屬性驅動的列車控制系統需求建模與驗證

何麗蕓，趙 林，程瑞軍

（北京交通大學 軌道交通控制與安全國家重點實驗室，北京 100044）

屬性驅動的列車控制系統需求建模與驗證

何麗蕓，趙 林，程瑞軍

（北京交通大學 軌道交通控制與安全國家重點實驗室，北京 100044）

形式化語言越來越多地用來描述列車控制系統需求規范，其精確的語法和語義一方面有助于創建精確的需求模型、消除理解差異，另一方面也為進一步分析驗證提供了基礎。通過提出一種基于屬性的需求分析方法，利用具體的形式化技術來分析需求。首先將由自然語言描述的需求規范轉換為屬性描述語言（PSL）形式化規范，并通過仿真和博弈分別進行語義檢查和可實現性驗證，最后通過斷言來檢驗形式化語言所刻畫的系統的精確性和完整性。該方法從自然語言形式的需求約束中直接提取相關需求規范，構造形式化模型并進行驗證，為需求的早期確認提供了一種新的實用途徑。并以CTCS-3級列控系統RBC切換場景為例，說明該方法的有效性。

需求規范；驗證；列車控制系統；仿真；可實現性

需求規范是系統開發重要的依據性規范標準。高質量的需求規范可以切斷需求階段的bug來源，如果需求規范的質量控制不到位，極有可能會產生最原始的bug，并將會貫穿到整個系統開發的始終，造成巨大的經濟損失。工業數據顯示大約50%的產品缺陷是由于需求的質量不到位造成的，大約80% 的返工工作量可以追溯到需求缺陷[1]，特別是對列車運行控制系統（以下簡稱“列控系統”）而言，其需求規范的缺陷往往造成不可估量的財產損失和人員傷亡。具體來說，列控系統需求規范大多都是依靠領域專家們的經驗而制定的，不可避免地存在某些漏洞或者安全隱患；另外，用自然語言刻畫的系統需求規范可能存在歧義。這都將會給系統的設計與開發帶來不利影響。因此，在列控系統開發的早期階段對需求進行形式化分析驗證以保證需求質量顯得十分必要。

列車運行控制系統是安全苛求系統。根據鐵路工業標準（CENELEC EN50128[2]）和國際通用的安全相關系統標準（IEC61508[3]），對高安全系統（安全完善度等級4級），強烈推薦使用形式化方法對系統需求進行分析驗證。形式化方法[4]是采用嚴格的數學語言、具有精確的數學語義的方法，適合于軟件和硬件系統的描述、開發和驗證。屬性描述語言（PSL）[5]作為一種形式化的屬性規范語言，易于讀寫、語法精簡、語義嚴格清晰。利用PSL語言表達需求，使得需求以唯一的方式被解釋，能夠排除由自然語言帶來地二義性，進而準確地表達需求。

因此，本文以PSL語言為基礎，提出了一種基于屬性的需求分析方法，該方法可以從自然語言形式的需求約束中直接提取和構造形式化模型，通過對形式化模型進行仿真（Simulation）、博弈（Game）、以及斷言（Assurance）來分析需求，確保形式化需求的語義正確性、完整性以及可實現性。其中，設計人員可以通過屬性仿真來構建具體的場景并檢驗某個屬性所刻畫的行為是否符合需求規范約束；通過博弈來對形式化模型進行可實現性驗證；通過屬性斷言從更全面整體的角度來分析形式化模型，驗證形式化屬性集是否一致，是否足夠完整地刻畫一個系統的行為。從而可以有效地解決需求規范的表意模糊和邏輯缺陷問題，并且能夠在系統開發的初期對規范中的漏洞進行排查，提高需求的質量。最后，本文以列控系統的無線閉塞中心（RBC）切換場景[6]為例來說明該方法的有效性。

1 基于屬性的需求分析方法

基于屬性的需求分析方法通過屬性仿真、屬性斷言和博弈來對系統需求的一致性、完整性以及可實現性進行驗證分析，是一個不斷迭代的過程。圖1描述了基于屬性的需求分析過程。

如圖1所示，設計人員首先從自然語言描述的用戶需求或未經驗證完善的需求規范中提取和構建形式化模型，通過屬性仿真來探索和研究形式化屬性的語義，將屬性的形式化表達式逐級分解來使設計人員更好地理解表達式，也可以用來糾正PSL形式化屬性表達式的錯誤；通過博弈來分析所刻畫的系統是否存在，是否可實現；通過屬性斷言對形式化需求規范的一致性和完整性檢查。其主要步驟簡述如下：

圖1 基于屬性的需求分析過程

（1）從自然語言描述的用戶需求或未經驗證完善的需求規范約束中直接提取和構建形式化需求模型Γ，該形式化需求模型使用PSL表示。對需求模型Γ進行一致性檢查，保證需求模型中的需求之間不存在沖突。

（2）若需求一致，則通過仿真來逐條檢驗需求模型Γ的形式化表達是否正確，是否描述的是所期望的行為，從而糾正并探索PSL形式化屬性表達式的語義。

（3）檢查由需求模型Γ所刻畫的系統是否為可實現，即是否存在與之相一致的系統。需求模型Γ中的變量分為環境（不可控）變量和系統（可控）變量。需求包含假定（Assumptions）需求和保證（Guarantees）需求兩種類型，分別是對環境變φ量和系統變量的約束。當環境輸入變量滿足所有假定需求時，存在一組滿足所有保證需求的系統變量，則稱該規范是可實現的。否則，規范為不可實現，需進行調試并修改該需求集。

（4）若系統可實現，則對形式化模型進行基于斷言的驗證，即通過兩個屬性集：assertionsφA和possibilities φP分別進行驗證。assertions φA，驗證所構建的形式化模型是否一定滿足assertions屬性，通過assertions來檢查形式化模型是否約束不足。possibilities φP，驗證形式化模型是否存在滿足possibilities屬性的可能性，通過possibilities來檢查需求是否約束過強。

（5）如果不滿足φA，檢查需求模型Γ是否約束不足，是否需要增加系統行為約束。如果不滿足φP，檢查需求模型Γ是否約束過強，是否需要去除系統行為的某個約束。通過這種方法，對需求模型Γ檢查修改，保證形式化需求模型的正確性。

（6）通過對需求模型Γ的修改更新，使其均滿足φA和φP后，逐步增加兩個屬性集φA和φP中的屬性約束再進行驗證，轉到第一步，不斷迭代，從而豐富和完善對系統的屬性刻畫。

為了形象地說明基于屬性的需求分析，將其用一個三元組來表示：

其中：

Γ： 形式化需求模型，描述系統行為和環境行為。Γ=＜S,E,RG,RA＞，其中，S和E是變量的兩個不相交集，S代表系統變量（受系統控制的變量），E代表環境變量（受環境控制的變量）。需求分為Guarantee需求和Assumption需求。Guarantee需求用RG表示，是關于系統變量的PSL屬性集；Assumption需求用RA表示，是關于環境變量的PSL屬性集。

φA：assertions屬性集，用Γ來描述的系統行為必須保證滿足assertion屬性（系統屬性的所有路徑必須都滿足assertions屬性集），通過assertions來檢查需求是否約束不足。

φP：possibilities屬性集，用Γ來描述的系統行為允許possibilities屬性（系統屬性中存在一條路徑滿足possibilities屬性），通過possibilitie來檢查需求是否約束過強。

下面以仲裁器為例進行說明，仲裁器的部分需求表示如下：

其中，g1和g2是布爾型系統變量，表示總線授權給出響應。r1和r2是布爾型環境變量，表示對總線發送請求。RG1表示兩個請求信號不能同時得到響應，RG2表示有請求最終會有響應，當S滿足RG時，E滿足RA，則系統是可實現的。同時，通過φA和φP來檢驗需求模型是否正確完整。

RATSY（ Requirements Analysis Tool with Synthesis[7]）是一種基于屬性的需求分析工具，它為工程人員提供了仿真、斷言和可實現性驗證的環境。以PSL為輸入語言，避免了復雜的建模過程，對獲得正確的形式化需求規范起到重要作用。下面以RBC切換場景為例說明基于屬性的需求分析方法在列控領域中的應用。

2 基于屬性的需求分析方法在列控系統需求規范中的應用

CTCS-3級列控系統是基于全球鐵路移動通信系統（GSM-R）的列車運行控制系統,通過車-地信息的雙向傳輸實現列車的閉環控制, 有效地提高列車的運營效率。由于包含有大量的子系統且功能復雜，在開發過程中，正確地理解并建立系統需求規范是首要問題。盡管工業數據顯示大約50%的產品缺陷是由于需求的質量不到位造成的，大約80%的返工工作量可以追溯到需求缺陷，但是對需求的分析手段卻很缺乏，而借助計算機輔助分析手段建立形式化的需求規范是一種有效的途徑。下面以RBC切換場景為例進行說明。

2.1 形式化需求模型的建立

場景可以用作分析與驗證需求的有效工具，可以通過選擇一組具有代表性的場景實例來對屬性需求進行檢驗，以發現需求中存在的缺陷。一組具有代表性的場景實例應該既包含描述一些系統期望行為的場景，即期望場景，也包含描述一些系統不希望發生行為的場景，即異常場景。使用場景實例對需求進行驗證和校驗，期望場景可以驗證需求的完整性，異常場景可以驗證需求的正確性。

CTCS-3級列控系統主要運營場景包括注冊與啟動、注銷、進出動車段、等級轉換、行車許可、RBC切換、自動過分相、重聯和摘解、臨時限速、降級情況、災害防護、調車作業、人工解鎖進路、特殊進路共14個場景文件，其中RBC場景是CTCS-3級列控系統中最為重要和最具代表性的流程之一，

現對該場景需求進行分析研究。場景中表示的屬性含義參見表1。

表1 場景中各屬性的含義

為了敘述簡單清晰，根據CTCS-3級列控需求規范，提取RBC切換運營場景的部分片段（兩部電臺都能進行正常的RBC切換）進行分析，以車載設備為系統，其他均看作環境。構建一個初步的形式化需求模型，該模型用形式化語言PSL表述如下：

RG1：允許車載設備與RBC 通信中斷的時間為7 s～20 s，當超過這段時間則降級處理。always(CommunicationInterrupt=1&&C3=1-＞next (C2=1))

RG2：如果車載設備的版本與RBC的版本不兼容，則觸發車載設備降級運行。

always(ID_RBCincompatible=1&&C3=1-＞next(C2=1))

RG3：當列車運行速度超過最大速度曲線規定的速度時，C3控制單元應能通過安全數字接口實現安全防護（超速時應能實現安全防護）。

always(OverSpeed=1-＞next(SafetyProtection=1))

RG4：當車載設備(OBE)正常運行無故障時，應能實現通信、安全防護、監控、制動和計算的功能。

always(OBE_faultFree＜_＞(!CommunicationIn terrupt&&SafetyProtection&&Supervision&&Brak e&&

Compute))

RG5：車載設備應處于CTCS-2或CTCS-3級運行，同時CTCS-2和CTCS-3級互斥。

always((C3=1&&C2=0)||(C3=0&&C2=1))

RG6：如果通信不中斷且列車處于CTCS-3級運行，則繼續以CTCS-3級運行。

always(CommunicationInterrupt=0&&C3=1-＞next (C3=1))

RA1：預告點（LTA）到切換點（RN）應滿足列車不小于40 s的運行距離。

always(LTA=1_＞next[40](RN=1))

RA2：當列車前端通過RN時，“移交RBC”停止對列車的控制，切換到“接收RBC”進行控制。

always(RN=1_＞next(HandoverRBC_MA=0& &AcceptRBC_MA=1))

RA3：列車不能同時使用“移交RBC”發送的行車許可和“接收RBC”發送的行車許可。

never(HandoverRBC_MA&&AcceptRBC_MA)

RA4：為消除RBC切換對列車正常運行的影響，車載設備應設置兩部獨立GSM-R通信電臺（GSM-R1和GSM-R2），車載設備通過GSM-R1接收“移交RBC” 發送的MA，通過GSM-R2呼叫“接收RBC”。

(always(HandoverRBC_MA＜-＞GSMR1))&&(always(AcceptRBC_MA＜-＞GSM-R2))

RBC切換描述了在不同RBC邊界處，實現列車在兩個RBC間行車許可控制的安全切換過程。通過上述的轉化，初步得到一個形式化的需求規范如下：

PARBCTransition=＜Γ,φA,φP＞

其中，

S ={C3, C2, Speed_c2, Speed_c3,

OverSpeed, SafetyProtection, OBE_faultFree, SafetyProtection, Supervision, Brake, Compute }

E={CommunicationInterrupt, ID_RBCincompatible, LTA, RN, HandoverRBC _MA,AcceptRBC_MA, GSM-R1, GSM-R2 }

2.2 形式化模型的仿真、可實現性驗證及斷言

2.2.1 形式化需求的仿真

利用形式化屬性成功地刻畫系統的一個先決條件是對屬性語言要有一個正確的理解。RATSY提供的屬性仿真環境使得工程人員可以逐條對屬性約束的正確性進行確認，從而判斷該屬性所描述的行為是不是我們所期望。例如，對屬性RA2: always(RN-＞next(!HandoverRBC_MA&&AcceptRBC_MA))進行語義檢驗。仿真結果如圖2所示，給出正例（RA2所描述的需求成立）和反例（RA2所描述的需求不成立），更好地理解滿足屬性RA2或違反屬性RA2的情況。

圖2 屬性仿真

2.2.2 形式化需求模型的可實現性驗證

在保證需求模型中的每條需求約束都正確后，開始從整體上對形式化模型進行可實現性驗證。也就是說，當所有的環境變量滿足Assumption需求時，所有的系統變量也滿足Guarantee需求。只有保證需求模型是可實現的，后面的斷言驗證才有意義。通過驗證，上面的需求是不可實現的。為了更加方便快速地找到需求不可實現的原因，工具為工程人員提供了診斷信息并且將與該系統不可實現有關的需求做標記。如圖3所示，需求RG1、需求RG2、需求RG3、需求RG4以及需求RG6與系統的不可實現有關。RG6表示如果通信不中斷且列車處于C3級運行，則繼續以C3級運行，而RG2表示如果車載設備的版本與RBC的版本不兼容，則觸發車載設備降級運行?？梢妰烧叽嬖诿埽瑧谕ㄐ挪恢袛嗖⑶臆囕d設備的版本與RBC的版本兼容時，系統才可能以C3級正常運行。因此，對RG6進一步約束為：always(CommunicationInte rrupt=0&&C3=1&&ID_RBCincompatible=0_＞next( C3=1))。驗證修正后的需求模型是可實現的?；趯傩缘男枨蠓治龇椒槲覀儾檎译[藏在需求中的可實現性問題提供了一種快捷而有效的手段。

圖3 GAME窗口

2.2.3 形式化需求模型基于斷言的驗證

雖然我們保證了需求集的可實現性和屬性語義正確性，但是這對于刻畫一個完整而正確的系統是遠遠不夠的，通過基于斷言的驗證來保證需求的完整性以及需求約束程度的合理性，約束不能過強或者不足。

前面所給的形式化模型中φA為空集，現在假定φA={a1, a2}并進行驗證，其中：

a1：當車載設備通過兩部電臺與RBC1和RBC2同時進行連接通信時，如果司機關閉了駕駛臺，車載設備將對RBC1和RBC2都執行終止任務程序。

always(DeskClosed=1-＞next(Handover-RBC_MA=0&&AcceptRBC_MA=0))

a2：如果列車位置信息無效，則降級，列車繼續保持與RBC的通信會話

always(TrainLocation=0-＞next(C2=1))

驗證結果如圖4所示，需求集Γ=＜S,E,A,G＞不能滿足φA屬性，說明需求Γ約束不夠，將a1和a2分別加入需求集Γ中，從而更新了需求集合，增強了對系統屬性的約束，使得系統屬性表示更加準確。

圖4 驗證結果

對φP集驗證的意義不同于φA的驗證，φA所描述的屬性需求集Γ的所有路徑必須都滿足。而φP中的屬性需求集Γ只要存在一條路徑滿足即可，保證了需求集約束的精確程度，不會因為約束過緊或約束不夠而影響所刻畫系統的準確性。在這里，φP={p1 },其中：

p1: 當列車RBC切換點時，通信中斷，列車不能得到移交RBC和接收RBC的行車許可。

always(RN=1&&CommunicationInterrupt=0_＞next(HandoverRBC_MA=0&&AcceptRBC_MA= 0))。

驗證結果表明，需求模型所刻畫的系統滿足p1屬性，與我們的設計意圖相符，說明需求約束并不存在過強的問題。

運用上面的方法進行不斷迭代，發現列控需求規范中的缺陷和漏洞，例如某條需求可能存在約束不夠或約束過強的問題，從而獲得高質量的需求，也保證了生命財產的安全。

3 結束語

本文所提出的基于屬性的需求分析方法通過驗證需求的正確性、完整性以及可實現性，可以有效地解決需求規范的表意模糊和邏輯缺陷問題，并且能夠在系統開發的初期對規范中的漏洞進行排查，提高需求的質量。采用該方法將PSL與可視化界面工具RATSY相結合，對高安全要求的列控系統需求規范進行分析驗證，通過反例對錯誤進行定位和修改。驗證過程表明，基于屬性的需求分析方法適用于CTCS-3級列控系統需求規范的分析驗證。該方法簡便易行，避免了復雜的建模和轉換過程。對于初步編寫規范及對原有系統規范進行更新升級的工作具有重要的意義。

[1] 常云麗,鄔欣明,鄭 威.軍用軟件需求分析研究[J].火力與指揮控制，2013，38（1）.

[2] CELENEC EN 50128: Railway Applications - Communications, signaling and processing systems- Software for railway control and protection systems[S]. 2001.

[3] International Standard IEC 61508: Functional Safety of Elec

trical/Electronic/Programmable Electronic SafetyRelated Sys

tems. International Electrotechnical Commission[S]. 2000. [4] 包麗梅,張玉春,張世錚.關于形式化方法與軟件可靠性的研究[J].內蒙古民族大學學報：自然科學版，2010（2）：166-167.

[5] Accellera. Property specif i cation language reference manual version 1.1[EB/OL]. (2004-06-09)[2008-03-02]. http://www. eda.org/vfv/docs/PSL-v1.1.pdf．

[6] 中華人民共和國鐵道部. CTCS-3級列控系統系統需求規范(SRS)[M]. 北京：中國鐵道出版社，2009.

[7] Bloem R, Cavada R, Cimatti A ,et al. RATSY-A new Requirements Analysis Tool withSynthesis[C].Computer Aided Veri-f i cation, 22nd International Conference. Berlin:Springer-Verlag, 2010: 425-429.

責任編輯 楊利明

Property-driven modeling and verif i cation for requirements of Train Control System

HE Liyun, ZHAO Lin, CHENG Ruijun
( State Key Laboratory of Rail Traff i c Control and Safety, Beijing Jiaotong University, Beijing 100044, China )

Formal languages were increasingly used to describe the requirements specif i cation of Train Control System, the precise syntax and semantics on the one hand, helped to create accurate demand model, eliminated understanding differences, on the other hand also provided a basis for further analysis of the validation. This paper presented a property based requirements analysis approach which analyzed requirement by the application of specialized formal analysis techniques. Firstly, requirements described by natural language were transformed into formal requirements described by PSL (Property Specification Language). Secondly, the semantics were checked by simulation and the realizability of the System was verif i ed by the game. Finally, the correctness and completeness of the System were validated by assurance. This method directly extracted the relative requirements specif i cation from requirement constraints described by natural language and formalized the structures model to verify, also provided a new practical way for the early validation of the requirements. By using some requirement fragments from RBC Handover scenarios of CTCS-3 Train Control System as a realistic example, it was demonstrated the effectiveness of this approach.

requirements specif i cation; verif i cation; Train Control System; simulation; realizability

U284.4∶TP39

A

1005-8451（2014）02-0001-06

2013-11-06

國家國際科技合作專項項目（2012DFG81600）；北京交通大學軌道交通控制與安全國家重點實驗室自主課題項目（No.RCS2012ZT006）。

何麗蕓，在讀碩士研究生；趙 林，講師。