基于Event-B的聯(lián)鎖進(jìn)路控制建模驗(yàn)證方法研究

童湖東，寧 濱，王海峰

（1.北京交通大學(xué) 軌道交通控制與安全國(guó)家重點(diǎn)實(shí)驗(yàn)室， 北京 100044；2. 北京交通大學(xué) 軌道交通運(yùn)行控制系統(tǒng)國(guó)家工程研究中心， 北京 100044）

聯(lián)鎖系統(tǒng)是鐵路信號(hào)系統(tǒng)的重要組成部分，是安全苛求系統(tǒng)。傳統(tǒng)的聯(lián)鎖軟件開發(fā)采用軟件工程方法，采用自然語(yǔ)言定義需求，使用基于功能的方法進(jìn)行系統(tǒng)設(shè)計(jì)，通過仿真和測(cè)試來進(jìn)行系統(tǒng)的驗(yàn)證。此方法在系統(tǒng)需求描述上難以保證完整性和一致性，在功能上也很難進(jìn)行完整的安全性分析與設(shè)計(jì)，仿真測(cè)試也無法完全遍歷系統(tǒng)所有狀態(tài)，使得聯(lián)鎖軟件中的錯(cuò)誤和安全隱患隨應(yīng)用的復(fù)雜度增加而增加，難以有效控制。針對(duì)這一問題，近年來國(guó)內(nèi)外學(xué)者做了形式化方法運(yùn)用于聯(lián)鎖軟件定義、設(shè)計(jì)過程的研究，如使用命題邏輯[1]、形式化Z語(yǔ)言[2～3]來做聯(lián)鎖系統(tǒng)規(guī)格說明和安全需求定義，使用Petri網(wǎng)[4]等形式化工具對(duì)聯(lián)鎖設(shè)備和邏輯進(jìn)行形式化建模等，但較少考慮對(duì)實(shí)際軟件開發(fā)過程的支持，在應(yīng)用上受到一定限制。

本文選取Event-B形式化方法對(duì)聯(lián)鎖進(jìn)路控制過程相關(guān)功能需求和安全需求進(jìn)行形式化建模、精化，采用機(jī)器證明和交互式證明相結(jié)合的方法進(jìn)行驗(yàn)證，生成高可靠性的模型，為后續(xù)程序開發(fā)提供支撐。

1 Event-B簡(jiǎn)介

Event-B方法是一種基于模型的形式化建模驗(yàn)證方法，以集合論和一階謂詞邏輯作為數(shù)學(xué)基礎(chǔ)，使用抽象機(jī)符號(hào)體系（Abstract Machine Notion， AMN），其構(gòu)建系統(tǒng)模型的基本單元是描述系統(tǒng)靜態(tài)屬性的場(chǎng)景（context）和描述系統(tǒng)動(dòng)態(tài)行為的抽象機(jī)（machine）。場(chǎng)景包含了系統(tǒng)中的常量（constant）、常量集合（carrier sets）以及用于約束常量（集合）類型、屬性及相互關(guān)系的公理（axioms）和定理（theorems）；抽象機(jī)則包括了描述系統(tǒng)狀態(tài)的變量（variables）、刻畫狀態(tài)改變的事件（event）及系統(tǒng)演變即狀態(tài)變化過程中必須滿足的不變式（invariants）。衛(wèi)條件（guard）是事件發(fā)生的觸發(fā)條件。Event-B以精化的形式進(jìn)行模型的逐步擴(kuò)展、細(xì)化和完善。為確保模型的安全性、有效性和完備性以及模型精化過程中的一致性，公理、定理和不變式需要被證明，由此產(chǎn)生證明義務(wù)[5]。Event-B相對(duì)于其他形式化方法更注重面向?qū)嶋H系統(tǒng)開發(fā)，從模型建立、精化、自動(dòng)證明到代碼生成整個(gè)開發(fā)周期都擁有較豐富的商業(yè)和開源的工具集支持體系。

2 聯(lián)鎖系統(tǒng)進(jìn)路控制的Event-B模型

2.1 聯(lián)鎖靜態(tài)數(shù)據(jù)的初步建模

聯(lián)鎖系統(tǒng)中靜態(tài)數(shù)據(jù)的主要內(nèi)容是信號(hào)機(jī)、道岔、軌道區(qū)段等物理實(shí)體的靜態(tài)屬性（如名稱、位置）和構(gòu)建于軌道區(qū)段之上的進(jìn)路的靜態(tài)屬性（如性質(zhì)、方向、范圍）以及它們之間的制約關(guān)系。以圖1所示站場(chǎng)圖（部分）為例，1股道下行接車進(jìn)路按方向依次包括軌道區(qū)段1DG、1G，Ⅱ股道下行接車進(jìn)路則依次包括軌道區(qū)段1DG、ⅡG。

圖1 站場(chǎng)示意圖

Event-B中的笛卡爾積、關(guān)系、函數(shù)能很好地描述靜態(tài)數(shù)據(jù)相關(guān)屬性。在Event-B中，有如下定義：

定義1 笛卡爾積：對(duì)任意集合S、T，笛卡爾積S×T表示所有這樣的有序?qū)Φ募希河行驅(qū)χ幸粋€(gè)元素屬于S,另一個(gè)元素屬于T。即：S×T={a?b|a∈S∧b∈T}。

定義2 關(guān)系：對(duì)任意集合S、T，關(guān)系S?T表示S與T笛卡爾積的冪集，即：S?T=?(S×T)，是一個(gè)S到T的多對(duì)多映射，其中?代表冪集。關(guān)系的定義域（dom）定義為：?r·r∈S?T? dom(r)={x·(?y·x?y ∈ r)}；值域（ran）則定義為：?r·r∈S?T ? ran(r)={y·(?x·x?y∈r)}。定義域限制定義為：S?r={x?y∣x?y∈r∧x∈S}；定義域縮減 ：S?r={x?y∣x?y∈r∧x?S}。值域限制和縮減的定義類似。

定義3 函數(shù)：函數(shù)是一種特殊的關(guān)系，是一種多對(duì)一的映射。本文主要用到的Event-B函數(shù)定義如下，對(duì)任意集合S、T：

偏函數(shù)：S■T={r·r∈S?T∧r～° r?T?id}，其中r～是關(guān)系r的共軛關(guān)系，r～° r表示r～與r的復(fù)合；

全函數(shù)：S→T={f·f∈S■T∧dom(f)=S}；

偏內(nèi)射：S■T={f·f∈S■T∧f～∈T■S}；

偏滿射：S■T={f·f∈S■T∧ran(f)=T}。

在進(jìn)路控制初步模型中，將軌道區(qū)段和進(jìn)路以常量集的形式引入場(chǎng)景中，分別為集合BLOCK和ROUTE，以圖1所示為例，BLOCK中的元素有 1DG， Ⅱ G，2DG和 1G；ROUTE則 包 含 了 1股道下行接車進(jìn)路和Ⅱ股道下行接車進(jìn)路。

為描述軌道區(qū)段間的拓?fù)溥B接關(guān)系以及軌道區(qū)段和進(jìn)路之間的從屬關(guān)系，引入以下常量：全關(guān)系adjc，描述軌道區(qū)段間的鄰接關(guān)系；全滿關(guān)系rbl，描述軌道區(qū)段與進(jìn)路間的從屬關(guān)系；全函數(shù)fbl和lbl，分別表示進(jìn)路中第一個(gè)和最后一個(gè)軌道區(qū)段。軌道區(qū)段和進(jìn)路的靜態(tài)安全屬性主要有以下幾點(diǎn)：（1）進(jìn)路內(nèi)的軌道區(qū)段具有拓?fù)溥B續(xù)性。（2）不存在環(huán)形進(jìn)路，即進(jìn)路內(nèi)的軌道區(qū)段不能首尾相接。（3）2條進(jìn)路若有共用軌道區(qū)段，則共用部分必須是從第一區(qū)段開始或以最后一個(gè)區(qū)段結(jié)束的連續(xù)區(qū)段。初步模型中，靜態(tài)安全屬性用模型的場(chǎng)景部分的公理來描述。初步模型的場(chǎng)景結(jié)構(gòu)如圖2所示。其中am_nocircle、am_successive、am_nobreak1和am_nobreak2分別描述了上述的3條安全屬性。

2.2 進(jìn)路控制過程的初步建模

聯(lián)鎖軟件進(jìn)路控制過程總體上可劃分為進(jìn)路建立和進(jìn)路解鎖2個(gè)階段[6]。本文用抽象機(jī)為進(jìn)路控制過程建模，初步模型中主要考慮進(jìn)路建立和進(jìn)路解鎖相關(guān)功能和安全需求的定義。在初步模型的抽象機(jī)interlocking_m_0中，引入4個(gè)模型變量表達(dá)系統(tǒng)狀態(tài)：被選出的進(jìn)路集合srt，被鎖閉的進(jìn)路集合lkrt，被征用的軌道區(qū)段集合sbl，以及被占用的軌道區(qū)段集合ocub。系統(tǒng)的安全需求分為2類：（1）狀態(tài)固有屬性的要求，即狀態(tài)的歸屬和范圍（用不變式1～5建模，如圖3所示）；（2）系統(tǒng)演變中的狀態(tài)遷移必須滿足的規(guī)律，例如軌道區(qū)段狀態(tài)只能是空閑→征用→鎖閉→占用而不能反轉(zhuǎn)（用不變式6～8建模，如圖3所示）。對(duì)應(yīng)于進(jìn)路控制過程的功能需求，引入3個(gè)基本事件：進(jìn)路選擇route_select、進(jìn)路鎖閉route_lock和進(jìn)路解鎖route_unlock。相應(yīng)的安全規(guī)則由事件的衛(wèi)條件來描述，如進(jìn)路鎖閉的判斷檢查條件：（1）進(jìn)路空閑；（2）相關(guān)道岔位置正確；（3）敵對(duì)進(jìn)路未建立。對(duì)應(yīng)圖1站場(chǎng)圖中，如要鎖閉1股道上行接車進(jìn)路，則必須要求1DG、1G空閑，道岔1處于反位鎖閉狀態(tài)。

圖2 進(jìn)路控制初步模型的場(chǎng)景結(jié)構(gòu)

圖3 進(jìn)路選擇、進(jìn)路鎖閉事件在初始模型抽象機(jī)中的結(jié)構(gòu)

進(jìn)路解鎖與進(jìn)路建立相對(duì)應(yīng)，初步模型中考慮正常解鎖，即在軌道電路檢測(cè)條件下的自動(dòng)解鎖，且以3點(diǎn)檢查方式作為安全性判斷條件，即第一階段檢查是否前一區(qū)段已解鎖和本區(qū)段有車占用，第二階段檢查本區(qū)段空閑和下一區(qū)段占用。

對(duì)應(yīng)圖1中，如要解鎖1股道上行接車進(jìn)路中的區(qū)段1G，則要求在緊鄰的上一周期1DG處于解鎖狀態(tài)且1G占用，本周期1G空閑且2DG占用。3點(diǎn)檢查解鎖條件作為系統(tǒng)的安全需求以衛(wèi)條件的形式引入事件的模型結(jié)構(gòu)。進(jìn)路解鎖事件的模型結(jié)構(gòu)如圖4所示。

2.3 模型的精化

對(duì)于本文聯(lián)鎖系統(tǒng)的Event-B模型，精化的過程主要是將站場(chǎng)元素逐步完善、聯(lián)鎖功能需求和安全需求逐步納入。本文采用了3步精化的策略，生成最終的進(jìn)路控制模型，詳細(xì)的精化策略如表1所示。

表1 進(jìn)路控制Event-B模型的精化策略

圖4 進(jìn)路解鎖事件的結(jié)構(gòu)

在精化策略的框架下，通過對(duì)模型的場(chǎng)景加強(qiáng)、事件擴(kuò)充和抽象機(jī)的細(xì)化分解，最終得到了較成熟的進(jìn)路控制Event-B模型，整個(gè)模型的層次化繼承結(jié)構(gòu)如圖5所示。

圖5 進(jìn)路控制Event-B模型的層次化繼承結(jié)構(gòu)

3 模型的形式化驗(yàn)證

Event-B采用基于定理證明的演繹驗(yàn)證的方式進(jìn)行形式化驗(yàn)證，本文利用Rodin工具平臺(tái)對(duì)設(shè)計(jì)的進(jìn)路控制Event-B模型進(jìn)行驗(yàn)證，Rodin能自動(dòng)生成證明義務(wù)，并由自帶的證明器獨(dú)立自動(dòng)證明部分證明義務(wù)。本文模型各精化層次的證明義務(wù)和自動(dòng)證明數(shù)目見表2。

表2 各精化層次模型的證明義務(wù)數(shù)目和自動(dòng)證明數(shù)目

對(duì)于未能被自動(dòng)證明的證明義務(wù)，則通過Rodin提供的推導(dǎo)規(guī)則庫(kù)機(jī)制、證明策略及相關(guān)工具，人為的增加一些假設(shè)條件和規(guī)則，進(jìn)行人工引導(dǎo)下的交互式證明。

圖6 證明義務(wù)route_select/inv8/INV的交互式證明過程

如圖6所示，給出了抽象機(jī)rtcontrol_m_0中證明義務(wù)route_select/inv8/INV的交互式證明主要過程，該證明義務(wù)描述了事件route_select是否滿足不變式inv_8。自動(dòng)證明器通過引入自由變量r0進(jìn)行證明，實(shí)際上要證明相繼式1。該過程中需要手動(dòng)加入待證明的假設(shè)(rbl?{r})～[{r0}]=?，證明器利用已有假設(shè)對(duì)該假設(shè)做出證明后，整個(gè)證明義務(wù)的推導(dǎo)證明就會(huì)由證明器繼續(xù)往前推進(jìn)。

經(jīng)過上述步驟，對(duì)整個(gè)模型的證明義務(wù)進(jìn)行了完全的證明，模型的安全性和正確性得到保證，為后續(xù)利用Event-B模型到代碼轉(zhuǎn)化相關(guān)工具生成高可靠性的進(jìn)路控制程序打下了基礎(chǔ)。

4 結(jié)束語(yǔ)

聯(lián)鎖系統(tǒng)具有邏輯上的復(fù)雜性和安全苛求特性，本文針對(duì)傳統(tǒng)開發(fā)方法存在的需求定義不精確，軟件安全隱患不易排除等缺點(diǎn)，探索了利用Event-B形式化方法對(duì)聯(lián)鎖軟件的核心部分—進(jìn)路控制過程進(jìn)行建模和驗(yàn)證的方法：利用形式化Event-B語(yǔ)言嚴(yán)格描述系統(tǒng)安全需求和功能需求，通過逐步精化來構(gòu)建系統(tǒng)模型，并通過基于定理證明的驗(yàn)證方式進(jìn)行模型驗(yàn)證以保證模型的安全性和一致性。結(jié)果表明，Event-B方法能較好運(yùn)用于聯(lián)鎖軟件開發(fā)過程，彌補(bǔ)傳統(tǒng)開發(fā)方法的不足。

[1]Eugenio Roanes-Lozano, Antonio Hernando, Jose Antonio Alonso, Luis M. Laita. A logic approach to decision taking in a railway interlocking system using Maple[J]. Mathematics and Computers in Simulation, Volume 82, Issue 1, September 2011, Pages 15-28.

[2]Khan, S.A.; Zafar, N.A.Towards the formalization of railway interlocking system using Z-notations[C]. 2nd In-ternational Conference on Computer, Control and Communication, vol.,no., pp.1-6, 17-18 Feb. 2009.

[3]王鐵江，酈 萌. 計(jì)算機(jī)聯(lián)鎖軟件的Z規(guī)格說明[J]. 鐵道學(xué)報(bào)，2003，25（4）：62-66.

[4]陳邦興，吳芳美. 鐵路信號(hào)聯(lián)鎖邏輯形式化建模研究[J].鐵道學(xué)報(bào)，2002，24（6）：50-54.

[5]Jean-Raymond Abrial. Modeling in Event-B[C]. Cambridge University Press，2010.

[6]趙志熙. 車站計(jì)算機(jī)聯(lián)鎖ABC[M]. 北京：中國(guó)鐵道出版社，2007.