程瑞軍 趙 林 何麗蕓

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

趙 林:北京交通大學(xué)軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室講師 100044北京

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

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

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

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

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

基于屬性的分析方法是個(gè)不斷迭代的過(guò)程。圖1描述了基于屬性的分析方法流程。主要的分析步驟簡(jiǎn)述如下。

第1步，建立規(guī)范中對(duì)應(yīng)場(chǎng)景的UML模型。

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

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

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

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

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

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

圖1 基于屬性的分析流程

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

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

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

2.1 模式轉(zhuǎn)換

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

2.2 模式轉(zhuǎn)換的PSL建模過(guò)程

2.2.1 建立模式轉(zhuǎn)換的UML模型

模式轉(zhuǎn)換中，車載設(shè)備需同無(wú)線閉塞中心、列車、應(yīng)答器等進(jìn)行信息交互。采用面向?qū)ο蟮姆椒▽TCS-3級(jí)列控系統(tǒng)中的實(shí)體抽象為幾個(gè)相互關(guān)聯(lián)的類，分別為車載設(shè)備類 (OBE)、司機(jī)類(Driver)、列車類 (Train)、無(wú)線閉塞中心類(RBC)和應(yīng)答器類 (Balise)。由于人機(jī)界面只起接口作用，與模式轉(zhuǎn)換的切換過(guò)程無(wú)關(guān)，在此不作考慮。

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

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

圖2 模式轉(zhuǎn)換的類圖

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

表1 圖2中類屬性和操作與規(guī)范對(duì)應(yīng)關(guān)系表

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

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

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

A1:T_stop＆＆ OBE_awake＆＆ !Iso_brake

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

3．約束環(huán)境事件和系統(tǒng)變量。對(duì)互斥的事件進(jìn)行約束，如隔離制動(dòng)和恢復(fù)制動(dòng)的操作不能同時(shí)發(fā)生，由PSL定義為A2:never(Iso_brake＆＆Recover_brake)。對(duì)車載工作狀態(tài)進(jìn)行約束，如不考慮故障情況，車載設(shè)備工作在CTCS-3級(jí)時(shí)，共有9個(gè)工作模式，在某一時(shí)刻CTCS-3級(jí)列控系統(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)圖，將模式轉(zhuǎn)換過(guò)程轉(zhuǎn)換為PSL描述，并作為約束集S的組成部分。例如，由隔離模式轉(zhuǎn)換到待機(jī)模式:

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

5．待驗(yàn)證性質(zhì)。由PSL描述系統(tǒng)待驗(yàn)證的屬性。如車載設(shè)備從待機(jī)模式 (SB)到調(diào)車模式(SH)的轉(zhuǎn)移特性，由PSL描述為:

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

2.2.3 建立PSL模型

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

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 對(duì)PSL形式化規(guī)范進(jìn)行調(diào)試和驗(yàn)證

2.3.1 對(duì)PSL模型進(jìn)行調(diào)試

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

圖4 GAME中的反例

2.3.2 模式轉(zhuǎn)換特性的驗(yàn)證

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

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

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

圖5 驗(yàn)證eventually!(SB＆＆next(SH))的仿真結(jié)果

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

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

圖6 編輯Büchi自動(dòng)機(jī)作為新需求

［1］ 中華人民共和國(guó)鐵道部．CTCS-3級(jí)列控系統(tǒng)系統(tǒng)需求規(guī)范(SRS)［M］ ．北京:中國(guó)鐵道出版社，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］ 曹源，唐濤，徐田華，等．形式化方法在列車運(yùn)行控制系統(tǒng)中的應(yīng)用［J］ ．交通運(yùn)輸工程學(xué)報(bào)，2010，10(1):112－126．