程瑞軍 趙 林 何麗蕓

程瑞軍:北京交通大學電子信息工程學院 碩士研究生 100044北京

趙 林:北京交通大學軌道交通控制與安全國家重點實驗室講師 100044北京

何麗蕓:北京交通大學電子信息工程學院 碩士研究生 100044北京

CTCS-3級列控系統(tǒng)需求規(guī)范，是CTCS-3級列控系統(tǒng)開發(fā)的起點和基礎，是確保列控系統(tǒng)高效安全運行的關鍵環(huán)節(jié)。列控系統(tǒng)是典型的復雜安全苛求系統(tǒng)，根據(jù)國際標準IEC61508-1，對高安全系統(tǒng) (安全完善度等級4級)強烈推薦使用形式化方法進行分析。

形式化方法采用嚴格的數(shù)學語言，具有精確的數(shù)學語義，適合于軟、硬件系統(tǒng)的描述、開發(fā)和驗證。國內外學者雖然提出了許多有用的形式化方法和模型檢驗工具，對列控領域的形式化方法進行歸納，然而對于工程人員來說，由于對大多數(shù)的形式化語言和驗證技術并不熟悉且難以理解，限制了形式化方法在工業(yè)界的廣泛應用。針對這一現(xiàn)狀，需要運用一種簡便的方法來對系統(tǒng)進行建模。UML是一種半形式化的建模語言，目前已被視為事實上的工業(yè)標準。同時，PSL(Property Specification Language)是一種易于讀寫、語法精簡、語義嚴格清晰的硬件設計屬性說明語言，為建立形式化模型提供了簡單的途徑，并可運用RATSY(Requirements Analysis Tool with Synthesis)對PSL模型進行形式化驗證。

因此，采用基于屬性的分析方法，不僅簡化了建模過程，而且在自然語言描述的規(guī)范與PSL模型之間建立了聯(lián)系，保證模型對需求規(guī)范的覆蓋能力。

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

基于屬性的分析方法是個不斷迭代的過程。圖1描述了基于屬性的分析方法流程。主要的分析步驟簡述如下。

第1步，建立規(guī)范中對應場景的UML模型。

第2步，根據(jù)轉換規(guī)則，將UML模型轉換為PSL形式化規(guī)范。該屬性規(guī)范是系統(tǒng)的抽象可執(zhí)行模型，允許在不考慮實現(xiàn)細節(jié)的情況下，使用該模型進行仿真、調試和驗證。

第3步，驗證該形式化模型是否能實現(xiàn)，即是否存在可實現(xiàn)的系統(tǒng)。如果是可實現(xiàn)的，則轉到第4步;若為不可實現(xiàn)，需運用RATSY工具調試并修改該PSL模型，通過反例對錯誤進行定位和修改，最終得到可實現(xiàn)的規(guī)范模型。

第4步，當需求可實現(xiàn)時，通過模型檢驗和仿真的方法進行驗證，驗證該模型是否具有某些屬性。若形式化需求不滿足某個屬性，就會得到一個反例。

運用上述分析方法，最終將得到PSL描述需求規(guī)范模型。系統(tǒng)可用一個四元組表示:

Y= ＜ S，E，A，G ＞。

其中，S和E是變量的2個不相交集，S代表系統(tǒng)變量 (受系統(tǒng)控制的變量)，E代表環(huán)境變量(受環(huán)境控制的變量)。需求分為保證需求和假定需求，保證需求用G表示，是關于系統(tǒng)變量的PSL屬性集;假定需求用A表示，是關于環(huán)境變量的PSL屬性集。

圖1 基于屬性的分析流程

RATSY是一種基于屬性的需求分析工具，為工程人員提供了仿真、驗證和調試的環(huán)境。以下舉例說明基于屬性的分析方法在列控領域中的應用。

2 基于屬性的分析方法在需求規(guī)范驗證中的應用

列車運行控制系統(tǒng)由地面設備和車載設備構成，用于控制列車運行速度，保證行車安全，提高運輸能力。由于包括有大量的子系統(tǒng)且功能復雜，正確地開發(fā)列控系統(tǒng)是很困難且容易出錯的。在開發(fā)過程中，正確理解并建立系統(tǒng)需求規(guī)范是首要問題。為了盡早發(fā)現(xiàn)規(guī)范中的漏洞，借助計算機輔助分析手段建立形式化的需求規(guī)范是一種有效途徑。以下運用UML和RATSY對CTCS-3列控系統(tǒng)需求規(guī)范中的模式轉換部分進行了建模和驗證。

2.1 模式轉換

模式轉換部分的規(guī)范描述了CTCS-3級列控系統(tǒng)的車載設備在不同工作環(huán)境下的工作模式及轉換過程。在配置有CTCS-3級基礎設備的區(qū)段，且不考慮故障的情況下，車載設備共有9種工作模式，分別為完全監(jiān)控模式 (Full Supervision，F(xiàn)S)、目視行車模式 (On Sight，OS)、引導模式 (Call On，CO)、調車模式 (Shunting，SH)、隔離模式(Isolation，IS)、待機模式 (Stand By，SB)、休眠模式 (Sleeping，SL)、冒進防護模式 (Trip，TR)和冒進后防護模式 (Post Trip，PT)。各模式的具體使用環(huán)境及主要功能參考文獻。

2.2 模式轉換的PSL建模過程

2.2.1 建立模式轉換的UML模型

模式轉換中，車載設備需同無線閉塞中心、列車、應答器等進行信息交互。采用面向對象的方法將CTCS-3級列控系統(tǒng)中的實體抽象為幾個相互關聯(lián)的類，分別為車載設備類 (OBE)、司機類(Driver)、列車類 (Train)、無線閉塞中心類(RBC)和應答器類 (Balise)。由于人機界面只起接口作用，與模式轉換的切換過程無關，在此不作考慮。

圖2給出了模式轉換的類圖，并對每個類的屬性、操作進行了舉例說明。圖2中關聯(lián)線所標示的數(shù)字表明關聯(lián)中的數(shù)量關系，例如，一列車上裝有2個車載設備。圖2中屬性和操作與規(guī)范的對應關系見表1。

根據(jù)需求規(guī)范的內容，將車載設備的工作模式表示為工作狀態(tài)。建立模式轉換的UML狀態(tài)轉移圖，如圖3所示。圖3表示了列控系統(tǒng)車載設備工作狀態(tài)的切換過程。狀態(tài)遷移條件使用不同的標號進行表示，例如，P2t20，P1t1等。其中P2，P1等表示該轉移條件的優(yōu)先級，數(shù)字越小則遷移優(yōu)先級越高。t20，t1等表示遷移條件的名稱，條件的具體內容可以參見文獻，在此不再贅述。

圖2 模式轉換的類圖

圖3 模式轉換部分的狀態(tài)遷移圖

表1 圖2中類屬性和操作與規(guī)范對應關系表

2.2.2 定義由UML模型到PSL模型的轉換規(guī)則

1．定義模式轉換場景涉及的環(huán)境變量和系統(tǒng)變量。由于模式轉換可研究車載設備的各工作模式的切換過程，因此以車載設備的工作模式為系統(tǒng)變量，輸入車載的信息及操作為環(huán)境變量建立模型。根據(jù)PSL的特點，引入消息機制，使用布爾型數(shù)據(jù)代替整型及字符串型數(shù)據(jù)。以變量BaliseID(應答器號)為例，需求規(guī)范驗證過程關注的是應答器號是否在列車的應答器列表中，而該變量的具體取值對驗證結果并不產生影響。因此使用事件 IN_ListOfBalises進行替換。IN_ListOfBalises的值為0，表示該應答器不在列車的應答器列表中;值為1，表示在列車的應答器列表中。對類的操作進行類似變換，如 IsolateBrake()，引入布爾型的事件Iso_Brake。

2．定義系統(tǒng)的初始工作狀態(tài)。車載設備上電后應進行自檢和外部設備測試，自檢和測試通過后自動進入待機模式。

A1:T_stop＆＆ OBE_awake＆＆ !Iso_brake

G1:SB＆＆!SH ＆＆!FS＆＆!OS＆＆!CO＆＆!SL＆＆!TR＆＆!PT＆＆!IS

3．約束環(huán)境事件和系統(tǒng)變量。對互斥的事件進行約束，如隔離制動和恢復制動的操作不能同時發(fā)生，由PSL定義為A2:never(Iso_brake＆＆Recover_brake)。對車載工作狀態(tài)進行約束，如不考慮故障情況，車載設備工作在CTCS-3級時，共有9個工作模式，在某一時刻CTCS-3級列控系統(tǒng)只能處于一種工作模式。

PSL描述為:

G2:(always(SB＜－＞!(SH||FS||OS||CO||SL||TR||PT||IS)))

G3:(always(SH＜－＞!(SB||FS||OS||CO||SL||TR||PT||IS)))等。

4．定義狀態(tài)遷移。根據(jù)UML狀態(tài)圖，將模式轉換過程轉換為PSL描述，并作為約束集S的組成部分。例如，由隔離模式轉換到待機模式:

G4:always(T_stop＆＆Recover_brake＆＆OBE_awake＆＆IS－ ＞next(SB))

5．待驗證性質。由PSL描述系統(tǒng)待驗證的屬性。如車載設備從待機模式 (SB)到調車模式(SH)的轉移特性，由PSL描述為:

P1:eventually!(SB＆＆next(SH))。

2.2.3 建立PSL模型

根據(jù)2.2.2的轉換規(guī)則，初步得到一個交互式的可執(zhí)行模型Y=＜S，E，A，G ＞，其中各集合對應的含義為:

S={SB，SH，F(xiàn)S，OS，……:boolean};

E={Iso_brake，T_stop，……:boolean};

A={A1，A2，……};

G={G1，G2，G3，G4，……}。

2.3 對PSL形式化規(guī)范進行調試和驗證

2.3.1 對PSL模型進行調試

RATSY工具封裝了NuSMV，以便對可實現(xiàn)的PSL模型進行驗證，對不可實現(xiàn)的PSL模型進行調試。以一個反例來介紹調試過程。根據(jù)實現(xiàn)性的概念，RATSY僅保留集合A和S中與可實現(xiàn)相關的約束集G2、G3、G5、G6等，并給出了反例 (如圖4)。在step1，系統(tǒng)初始化工作模式為待機模式(SB);在step2，E_Brake(車載接收到緊急停車信息)、Iso_brake(隔離車載制動功能)和T_stop(列車停車)同時滿足，根據(jù)G5車載設備應切換至調車模式SH，根據(jù)G6車載設備應切換至完全監(jiān)控模式FS。但由G2、G3等約束知車載設備只能處于一種工作模式，故G2、G5和G6規(guī)范之間存在沖突?？紤]到實際情況，當車載設備處于待機模式時，RBC不能既給車載發(fā)送行車許可MA，同時又允許車載進入調車模式。因此需加入對環(huán)境變量的約束A3:never(RBC_per_SH＆＆Tdata_MA)。驗證修正后的規(guī)范是可實現(xiàn)的。最后需在需求規(guī)范中寫入該條信息，即RBC不能同時給車載發(fā)送行車許可和允許調車命令。

圖4 GAME中的反例

2.3.2 模式轉換特性的驗證

對CTCS-3級列控系統(tǒng)需求規(guī)范進行驗證，驗證所建立的模型是否具有某些屬性。對于斷言類的屬性 (用As標記)，若不滿足會給出反例;對于可能性屬性 (用P標記)，若滿足則給出仿真結果。由于涉及系統(tǒng)的所有模式，驗證內容較多，因此僅對驗證過程舉例介紹。

1．可達性驗證。例如，P1:eventually!(SH)，該屬性表示系統(tǒng)可以從其他狀態(tài)到達調車模式 (SH)狀態(tài)。驗證結果為真，存在一條到達調車模式的路徑，調車模式 (SH)可達。

2．轉移性驗證。例如，P2:eventually!(SB＆＆next(SH))，表示車載設備從待機模式(SB)可以經過1個轉換步驟切換至調車模式(SH)狀態(tài)。驗證結果為真，并得到一條滿足該屬性的路徑 (如圖5所示)，其中Step1為初始化狀態(tài)，系統(tǒng)從Step2開始運行，經過一個轉換步驟到SH模式。因此，系統(tǒng)由SB模式到SH模式具有轉移性。

圖5 驗證eventually!(SB＆＆next(SH))的仿真結果

3．死鎖性驗證。例如，As1:never(eventually!(always(SH)))，該屬性表示系統(tǒng)不會在很長一段時間內停留在調車模式。驗證結果為假，表明系統(tǒng)可能在很長一段時間內處于調車模式，會出現(xiàn)死鎖，需要添加新的需求。車載工作于調車模式且列車在停車狀態(tài)下，司機可通過再次按壓調車鍵退出調車模式轉入SB模式。編輯該需求的Büchi自動機 (如圖6所示，其中Init為Büchi自動機的初始狀態(tài))，并通過RATSY轉換成PSL公式，添加到原PSL模型中。重新進行驗證，驗證結果滿足As1屬性的要求。

本文運用基于屬性的需求分析方法，對CTCS-3級列控系統(tǒng)需求規(guī)范中的模式轉換部分進行形式化驗證。采用UML與PSL相結合的方法，利用RATSY對PSL模型進行相關屬性的驗證，通過反例對錯誤進行定位和修改。驗證過程表明基于屬性的分析方法適用于CTCS-3級列控系統(tǒng)需求規(guī)范的驗證。該方法簡便易行，對于初步編寫規(guī)范及對原有系統(tǒng)規(guī)范進行更新升級的工作具有重要的意義。

圖6 編輯Büchi自動機作為新需求

［1］ 中華人民共和國鐵道部．CTCS-3級列控系統(tǒng)系統(tǒng)需求規(guī)范(SRS)［M］ ．北京:中國鐵道出版社，2009．

［2］ BOWEN J P．Formal Methods in Safety－Critical Standards［C］ //Software Engineering Standards Symposium．Brighton:IEEE Computer Society Press，1993:168－177．

［3］ 古天龍．軟件開發(fā)的形式化方法［M］ ．北京:高等教育出版社，2005:15－20．

［4］ 曹源，唐濤，徐田華，等．形式化方法在列車運行控制系統(tǒng)中的應用［J］ ．交通運輸工程學報，2010，10(1):112－126．