周庭梁， 許 婧， 陳小紅， 趙時旻

(1.同濟大學(xué) 道路與交通工程教育部重點實驗室， 上海 201804；2.卡斯柯信號有限公司， 上海 200071;3.華東師范大學(xué) 上海市高可信計算重點實驗室, 上海 200062)

?

基于因果關(guān)系的列控系統(tǒng)模型約簡方法

周庭梁1,2， 許 婧2， 陳小紅3， 趙時旻1

(1.同濟大學(xué) 道路與交通工程教育部重點實驗室， 上海 201804；2.卡斯柯信號有限公司， 上海 200071;3.華東師范大學(xué) 上海市高可信計算重點實驗室, 上海 200062)

在基于安全需求對驗證問題進(jìn)行投影的方法基礎(chǔ)上，針對投影出的驗證子問題，提出了基于因果關(guān)系的變量約簡方法，定義了環(huán)境變量間的因果關(guān)系，歸納出基本的因果關(guān)系組合，并提煉出變量約簡規(guī)則，通過變量約減減少了驗證問題的狀態(tài)空間.采用國內(nèi)某地鐵線路的相關(guān)數(shù)據(jù)進(jìn)行建模和驗證，結(jié)果表明，該方法能夠有效降低系統(tǒng)驗證復(fù)雜度.

需求驗證； 變量約簡； 因果關(guān)系； 列車運行控制系統(tǒng)

作為一種安全攸關(guān)系統(tǒng)，列車運行控制系統(tǒng)(簡稱列控系統(tǒng))必須經(jīng)過驗證.目前列車運行控制系統(tǒng)的建模和驗證方法主要有以下3種：① 基于邏輯的方法.這類方法基于集合論和一階邏輯，采用邏輯推理或者定理證明的方式精化系統(tǒng)的功能，證明系統(tǒng)的正確性，典型代表是Z，VDM，B和Event-B方法[1]等，其中B方法已經(jīng)在法國巴黎RER線路所采用的SACEM系統(tǒng)[2]中得到成功應(yīng)用.② 基于進(jìn)程代數(shù)的方法.進(jìn)程代數(shù)關(guān)注并行行為，強調(diào)對不同模塊并發(fā)過程之間的交互進(jìn)行建模.例如，Zou等[3]調(diào)研了如何對CTCS-3(Chinese Train Control System 3)的系統(tǒng)需求規(guī)約(system requirement specification，SRS)進(jìn)行形式化的描述和驗證.③ 基于形式化模型與規(guī)約的方法.在列控系統(tǒng)的需求階段，多種類型的模型被用于系統(tǒng)建模和驗證過程中.例如，基于有色Petri網(wǎng)(coloured Petri nets，CPNs)，Horste等[4]對歐洲列控系統(tǒng)ETCS進(jìn)行了針對系統(tǒng)功能的形式化描述.

雖然現(xiàn)有的這些需求建模方法能有效避免二義性，并且能成功實現(xiàn)對需求規(guī)約的驗證，但是這些方法并沒有考慮到環(huán)境的影響.列控系統(tǒng)所處環(huán)境的復(fù)雜性以及環(huán)境自身的其他特性，會帶來系統(tǒng)模型驗證空間急劇爆炸的問題，導(dǎo)致在復(fù)雜環(huán)境中難以保證系統(tǒng)的可信度.因此，在需求模型的可信構(gòu)造和驗證過程中，需要研究如何對環(huán)境相關(guān)的約束進(jìn)行調(diào)整，從而提高復(fù)雜環(huán)境下列控系統(tǒng)模型的可驗證性.

為了解決這個問題，組合驗證方法應(yīng)運而生[5].組合驗證方法先將系統(tǒng)分解為子系統(tǒng)，然后分別驗證各子系統(tǒng)，最后分析集成的系統(tǒng).這類方法在很多大型系統(tǒng)中得到成功的應(yīng)用，例如McMillan[6-7]將該方法應(yīng)用于微處理器的亂序執(zhí)行單元和多處理機的緩存一致性協(xié)議.但是傳統(tǒng)的組合驗證的分解方法只能對系統(tǒng)進(jìn)行劃分，不允許子系統(tǒng)中存在重疊的部分.然而在列控系統(tǒng)中，由于環(huán)境共享，不可避免地存在子系統(tǒng)之間的部分重疊.基于問題框架方法的投影[8]是一種有效的處理有重疊部分的分解方法.它能夠?qū)?fù)雜的問題通過投影進(jìn)行分解，降低大型系統(tǒng)的復(fù)雜度.

基于問題框架方法，本文作者提出了一種基于安全需求的驗證問題投影方法[9]，以列車控制驗證系統(tǒng)的安全子屬性作為投影維度，將列控系統(tǒng)驗證問題投影為若干子問題.該方法可以有效地降低復(fù)雜度，但還是不能完全避免驗證問題狀態(tài)空間過大的問題.在研究投影出的子問題時，發(fā)現(xiàn)在列控系統(tǒng)中，變量之間存在因果關(guān)系，而變量的減少可以有效減小狀態(tài)空間.因此，本文通過找出存在因果關(guān)系的變量，并根據(jù)不同的因果關(guān)系類型對這些變量進(jìn)行約簡，進(jìn)一步降低驗證系統(tǒng)的狀態(tài)空間.最后采用國內(nèi)某地鐵線路的相關(guān)數(shù)據(jù)進(jìn)行建模和驗證，結(jié)果表明，該方法可以有效地降低驗證系統(tǒng)的復(fù)雜度，降低形式化模型驗證中的狀態(tài)空間爆炸問題發(fā)生的可能性，并且提升了形式化驗證的效率.

1 列控系統(tǒng)的需求模型驗證問題及投影

IS=a∪b∪ca:E!{p11,p12,…,pnm}b:M!{q11,q12,…,qnm}c:VM!{true, false}

圖1 列控系統(tǒng)驗證問題

Fig.1 Verification problem of automatic train

control system

在這些元素中，環(huán)境(E)實際上是與列控系統(tǒng)進(jìn)行交互的設(shè)備集合，每個設(shè)備可以用一組變量描述.因此，本文將E定義為一組設(shè)備變量Di(0≤i≤n)的集合，而每個設(shè)備變量又有一組屬性變量Vij(0≤i≤n,0≤j≤m)表示，可形式化定義為E={D1,D2,…,Di,…,Dn}，其中，Di={Vi1,Vi2,…,Vij,…,Vim}.

E與M有共享的交互集合a和交互集合b，其中a為由E控制的交互pij(0≤i≤n,0≤j≤m)的集合，b為由M控制的交互qij(0≤i≤n,0≤j≤m)的集合.在列控系統(tǒng)問題中，因為E和M間共享的是設(shè)備的屬性變量，所有的交互都是值交互，所以可以將交互定義為由設(shè)備的屬性變量的取值所確定的函數(shù)值，因此將與設(shè)備Di的屬性變量有關(guān)的交互pij,qij定義為，pij=fij(Vi1,Vi2,…,Vim)，qij=gij(Vi1,Vi2,…,Vim).

安全需求(Req)描述了M需要滿足的條件.Req引用了交互b，這是一個約束引用，約束環(huán)境的行為必須按照安全需求所規(guī)定的方式改變.安全需求由一組安全屬性構(gòu)成，只有當(dāng)每個安全屬性Pi(0≤i≤n)都成立時，安全需求Req才能成立.安全需求定義為(其中∧表示與)：Req=P0∧P1∧…∧Pi∧…∧Pn.

在這些定義基礎(chǔ)上，提出了基于安全需求對列控系統(tǒng)的驗證問題進(jìn)行投影[9]，將原驗證問題投影成多個子問題進(jìn)行驗證，從而得到了新的子問題的驗證系統(tǒng)、驗證環(huán)境和驗證需求.由于安全需求Req與問題的5個描述元素都有關(guān)系，所以可將Req作為投影的維度.因此，可以基于安全子屬性對整個驗證問題進(jìn)行投影.采用關(guān)系代數(shù)類似的表達(dá)，問題投影的形式可以表示如下：

(1)

在這4個輔助算子的基礎(chǔ)上，結(jié)合系統(tǒng)M，可以定義列控系統(tǒng)形式化驗證問題的投影為

(2)

在對投影結(jié)果進(jìn)一步分析時發(fā)現(xiàn)，在對子問題的環(huán)境進(jìn)行投影時只是將與待驗證的安全需求無關(guān)的設(shè)備進(jìn)行約簡，保留下所有與待驗證的安全需求相關(guān)的設(shè)備參數(shù).因此，只要與待驗證的安全需求產(chǎn)生了交互，該設(shè)備的所有變量都會被加入到環(huán)境中，但并不是所有加入的變量都真正會對驗證結(jié)果產(chǎn)生影響.因此，本文提出基于因果關(guān)系的約簡方法，嘗試找出設(shè)備內(nèi)部的各個變量間可能存在的關(guān)系，并基于變量間的因果關(guān)系進(jìn)一步降低系統(tǒng)的復(fù)雜度，從而進(jìn)一步減小系統(tǒng)的狀態(tài)空間，提高系統(tǒng)的驗證效率.

2 基于因果關(guān)系的變量約簡

2.1 列控系統(tǒng)的變量因果關(guān)系分析

在對列控系統(tǒng)驗證問題進(jìn)行投影后，將原驗證問題投影成多個子問題進(jìn)行驗證，能有效地降低系統(tǒng)驗證復(fù)雜度[11].但在投影后，只要與驗證需求產(chǎn)生了交互，該設(shè)備的所有變量都會被加入到環(huán)境中.但事實上，并不是所有變量都會對驗證結(jié)果產(chǎn)生影響[12]，這為進(jìn)一步約簡驗證系統(tǒng)提供了可能.

在未對變量進(jìn)行任何約簡前，環(huán)境中所有設(shè)備的屬性變量都與驗證系統(tǒng)共享.分析各變量間的關(guān)系后可以發(fā)現(xiàn)，在某些設(shè)備內(nèi)部的變量之間存在直接的因果關(guān)系.

設(shè)C,R為E中的變量或者E中變量間任意的與、或組合.根據(jù)因果關(guān)系理論，因果關(guān)系共分為4種：①C→R；② ￢C→R；③C→￢R；④ ￢C→￢R.

在情況①中，即當(dāng)C存在時，R一定存在，且R可由C推導(dǎo)得出，因此可設(shè)R=S(C)，此時可直接用C來表示R.

例如，在描述列車車尾的位置時，有兩個變量：最大車尾MaxTrainTailPos和最小車尾MinTrainTailPos.最大車尾和最小車尾之間的距離固定為TailLength，所以有

MaxTrainTailPos=MinTrainTailPos+

TailLength

則MinTrainTailPos → MaxTrainTailPos可表示為MaxTrainTailPos = S(MinTrainTailPos).

此時，所有與MaxTrainTailPos相關(guān)的變量均可由S(MinTrainTailPos)替代.

在情況②中，當(dāng)C不存在時，R一定存在.在情況③中，當(dāng)C存在時，R一定不存在.在列控系統(tǒng)的環(huán)境中，設(shè)備的屬性變量很少出現(xiàn)互斥的關(guān)系，所以在列控系統(tǒng)中，這兩種因果關(guān)系很少存在.即使存在，在情況②中，由于C不存在，R無法由C推導(dǎo)得出，所以無法約簡.在情況③中，由于R本身就不存在，所以同樣無法約簡.在情況④中，當(dāng)C不存在時，R一定不存在.這種情況下，由于C，R都不存在，這種因果關(guān)系對約簡狀態(tài)空間沒有實際意義.

總結(jié)上述4種情況分析, 只有C→R這類因果關(guān)系會對列控系統(tǒng)驗證過程中的變量約簡產(chǎn)生直接影響.由于系統(tǒng)驗證時會對所有變量進(jìn)行全狀態(tài)空間的遍歷，可用R=S(C)替代R，在R的取值范圍較大的情況下可明顯減小狀態(tài)空間，提升系統(tǒng)的驗證效率.由于變量的因果關(guān)系不一定是一一對應(yīng)的，也可能存在多個變量之間的因果關(guān)系.設(shè)C,R為E中的變量或者E中變量間任意的與、或組合，由上文可知，只有C→R類因果關(guān)系能用于變量約簡.

2.2 列控系統(tǒng)的因果關(guān)系定義

為了表達(dá)出所有能用于變量約簡的因果關(guān)系，基于巴克斯范式(Backus-Naur Form，BNF)[13]對比類因果關(guān)系進(jìn)行如下定義：

<因果關(guān)系> ::= <變量表達(dá)式> → <變量表達(dá)式>

<變量表達(dá)式> ::= <變量> | <變量表達(dá)式> <運算符> <變量表達(dá)式>

<運算符> ::= ∧ | ∨

<變量> ::=V1|V2|…|Vi| …|Vn

變量間的組合型因果關(guān)系有7種最基本的情況，設(shè)Vi,Vj,Vk,Vl∈E，這7種基本情況分別為

(3)

(1)Vi→Vl

由上文可知，這種情況下可以用Vl=S(Vi)替代Vl.

(2)Vi∧Vj→Vl

需要同時知道Vi和Vj，才能推導(dǎo)出Vl.這種情況下Vl可表示為Vl=S(Vi,Vj).

(3)Vi∨Vj→Vl

只需知道Vi和Vj中任意一個變量，就能推出Vl.這種情況下Vl可表示為Vl=S(Vi)或Vl=S(Vj)，從中任取一種即可.從變量約簡的角度看，替換Vl時選擇Vi和Vj沒有區(qū)別，所以可以比較Vl=S(Vi)和Vl=S(Vj)，從中選擇較為簡單的一種表示方法對Vl進(jìn)行替換.

這種情況下，需要知道Vi∧Vj或者Vl，就能推出Vl.則Vl可表示為Vl=S(Vi,Vj)或Vl=S(Vk)，從中任取一種即可.由于Vl=S(Vk)的表示方法更簡潔，用S(Vk)替換Vl會使之后的驗證過程更為簡單.

這種情況下，需要知道Vi∧Vk或者Vj∧Vk，才能推出Vl.所以Vl可表示為Vl=S(Vi,Vk)或Vl=S(Vj,Vk)，從中任取一種即可.

(6)Vi→Vj∧Vl

在這種情況下，只需知道Vi，就可以推出Vj和Vk，因此等價于Vi→Vj且Vi→Vk.

(7)Vi→Vj∨Vl

在這種情況下，因無法確定推出的結(jié)果是Vj還是Vk，所以無法進(jìn)行約簡.如果有其他信息能輔助判斷推出的結(jié)果具體為哪個變量，則可以將問題轉(zhuǎn)化為Vi→Vj或者Vi→Vk進(jìn)行處理.

2.3 變量表達(dá)式的約減規(guī)則

在提煉出的7種基本情況中，情況(1)是一對一的情況，即一種原因推出一個結(jié)果；情況(2)至(5)是多對一的情況，即多種原因可以推出一個結(jié)果.這5種情況中變量Vl都可以由其他變量推出，因此可以用其他變量進(jìn)行替代.情況(6)和(7)是一對多的情況，用一個變量能夠推導(dǎo)出多個結(jié)果，即變量Vj和Vk都可以用變量Vi推導(dǎo)得到，因此在變量約簡后，可以用更少的變量來定義交互，由此可以降低驗證復(fù)雜度.除了上述7種最基本的情況外，式(3)所定義的其他情況都是這7種情況的組合，并可以通過依次迭代最終化簡為這7種情況中的一種，再對變量進(jìn)行約簡.

設(shè)C,C1,C2,C3,R,R1,R2是式(3)所定義的變量表達(dá)式，通過對這7種最基本情況的分析，可以總結(jié)出4個約簡規(guī)則：

(4)

根據(jù)基本情況(3)可知，只需知道C1和C2中任意一個變量表達(dá)式，就能推出R，所以原因中的C1∨C2可以直接用C1或C2替換.

(5)

根據(jù)基本情況(6)可知，只需知道C，就可以推出R1和R2，因此等價于C→R1且C→R2，可以拆成這兩種情況分別進(jìn)行討論.

(6)

根據(jù)基本情況(4)可知，只需要知道C1∧C2或者C3，就能推出R.由于用C3推導(dǎo)R會更為簡潔，所以 (C1∧C2)∨C3直接用C3替換.

(7)

根據(jù)基本情況(5)可知，只需要知道C1∧C3或者C2∧C3，就能推出R.所以(C1∨C2)∧C3可用C1∧C3或者C2∧C3替換.

在對列控系統(tǒng)的變量進(jìn)行分析時，如果變量之間存在可以用于約簡的因果關(guān)系，則一定在式(4)所定義的范圍內(nèi).而式(4)所定義的因果關(guān)系，又可以通過上述4個化簡規(guī)則轉(zhuǎn)化成最基本的7種變量間的組合型因果關(guān)系之一進(jìn)行處理，所以對所有可能情況都可以進(jìn)行相應(yīng)的變量約簡操作.在約簡的過程中，由于交互并未發(fā)生改變，但驗證過程中實際使用到的變量個數(shù)減少了，從而降低了系統(tǒng)驗證復(fù)雜度.

3 實例分析

以卡斯柯信號有限公司的軌旁列控系統(tǒng)區(qū)域控制器iZC為例，應(yīng)用基于因果關(guān)系的約簡方法，降低系統(tǒng)驗證的復(fù)雜度.與上一代列控系統(tǒng)有所不同，CBTC系統(tǒng)通過移動閉塞來追蹤并保護(hù)列車.iZC根據(jù)軌道上各列車的精確位置，來計算各列車之間的安全區(qū)間，并通過無線車地通信傳遞給列車.這些安全區(qū)間被稱為移動授權(quán)(MA).MA屬于列控系統(tǒng)的核心安全功能，其安全等級達(dá)到SIL4要求，必須通過形式化驗證來確保該功能的正確性及安全性.

iZC會在每個計算周期內(nèi)為其管轄范圍內(nèi)的所有列車計算移動授權(quán)MA的范圍，起點一般為列車的最小車頭，計算得到的終點稱之為EOA(end of authority).EOA是指授權(quán)列車移動的最大距離，EOA的計算依賴于列車自身的位置、速度，同時還依賴于軌道上的信號設(shè)備和特殊區(qū)段，例如包括信號機、緩沖區(qū)、重疊區(qū)等.

根據(jù)IEEE 1474.1標(biāo)準(zhǔn)[14]，當(dāng)遇到8種特殊情況時列車EOA計算將會終止，例如列車前方出現(xiàn)另外一輛CBTC列車、緩沖區(qū)、重疊區(qū)等等.這些情況可能導(dǎo)致列車運行發(fā)生事故，因此這些情況也被稱為非安全狀態(tài)點.根據(jù)這8種情況，本文將EOA分為8種類型.同時，在iZC發(fā)給列車的MA報文中，包含EOA_TYPE字段，主要描述選取當(dāng)前點作為EOA的原因.

3.1 EOA驗證問題描述

EOA模型的形式化驗證問題可以表示為:

ProblemEOA=

其中，EOA為待驗證的系統(tǒng)模型，共有8種類型，在驗證過程中為“黑盒”，不可更改.EnvEOA為問題所處的環(huán)境，包含車、閉塞、分支、信號機、BZ(buffer zone)、OL(overlap)、TD(traffic direction)等，即

EnvEOA=

VeriEOA為需要創(chuàng)建的EOA驗證系統(tǒng).IntEOA為EnvEOA與各問題領(lǐng)域交互的集合Int1∪Int2∪Int3.SafeR′為EOA的驗證需求，驗證EOA的安全需求SafeR=P0∧P1∧P2.

針對不同的EOA系統(tǒng)類型j，每個安全需求Pi僅需滿足對應(yīng)的安全子屬性Pij，因此有

SafeR=P01∧P02∧…∧P08∧P11∧…∧P18∧P21∧…∧P28

由于系統(tǒng)EOA不可變動，所以投影后結(jié)果不會變化.另外的4個元組可以借助投影算子分別進(jìn)行投影.下面以第8種類型EOA為例進(jìn)行投影，并對投影后的子問題進(jìn)行約簡.該類型EOA表示非安全狀態(tài)點為重疊區(qū)，即前方搜索到閉塞軌道邊界.根據(jù)文獻(xiàn)[9]中的投影方法，以安全子屬性SafeR8為投影維度，對 ProblemEOA進(jìn)行投影，投影結(jié)果為

SProblemEOA8是由原問題ProblemEOA投影出的子問題.安全需求SafeR8是原問題安全需求SafeR的子集，驗證時可直接跳過與當(dāng)前類型無關(guān)的安全需求的驗證過程，因此，根據(jù)投影后的安全需求設(shè)計出的驗證系統(tǒng)的規(guī)模也相應(yīng)減小.

3.2 EOA驗證變量約簡

列控系統(tǒng)一般采用兩種坐標(biāo)定位方式.一種是基于閉塞(block)的，例如一組道岔的位置可以表示為一個二元組(Block_Index, OffsetOnBlock)，其中Block_Index表示道岔所處的閉塞索引，OffsetOnBlock表示精確的位置偏移.另外一種是基于分支(branch)的，分支是一組閉塞連接而成的連續(xù)軌道，一組道岔的位置可以表示為一個二元組(Branch_Index, OffsetOnBranch)，其中Branch_Index表示道岔所在的分支索引，OffsetOnBranch表示在該分支上的精確的位置偏移.因此，所有的基于閉塞的位置坐標(biāo)都可以轉(zhuǎn)化為基于分支的位置坐標(biāo).

以列車內(nèi)部變量關(guān)系為例，列車位置由4個坐標(biāo)決定：最大(MaxTrainHeadPos)/最小(Min-TrainHeadPos)車頭位置和最大(MaxTrain-TailPos)/最小(MinTrainTailPos)車尾位置.值域[MinTrainHeadPos, MaxTrainHeadPos]代表列車車頭的可能位置.值域[MinTrainTailPos, Max-TrainTailPos]代表列車車尾的可能位置.同時，每輛列車被一個列車在軌道上的虛擬占用區(qū)域(VTP)包絡(luò).iZC系統(tǒng)被設(shè)計用于計算VTP的碰撞概率，并防止這些VTP發(fā)生碰撞.由于VTP的位置與列車的位置相互關(guān)聯(lián)，VTP的位置變量與列車的位置變量會相互影響.VTP位置也由4個坐標(biāo)決定：最大(MaxVTPHeadPos)/最小(MinVTPHeadPos)VTP頭位置和最大(MaxVTPTailPos)/最小(MinVTP-TailPos)VTP尾位置，如圖2所示.

圖2 列車定位相關(guān)坐標(biāo)點

另外還有1個列車狀態(tài)變量(TrainMonitor-Modes)用來表示列車當(dāng)前的運行模式.由此可知，

Train={MinVTPTailPos, MaxVTPTailPos,

MinVTPHeadPos, MaxVTPHeadPos,

MinTrainTailPos, MaxTrainTailPos,

MinTrainHeadPos, MaxTrainHeadPos,

TrainLength, TrainMonitorModes}

在問題投影過后生成的子問題SProblemEOA8中，列車的位置坐標(biāo)點全部隨機，即它們可能為任意一個block中的任意一個點.但實際情況中，車的位置坐標(biāo)之間存在幾組等價關(guān)系，由圖2可以推導(dǎo)出：

(1) 最小VTP尾與最小車尾間距離為固定值MinTailLength，所以

MinTrainTailPos → MinVTPTailPos

(2) 最小車尾與最小車頭之間距離為固定長度，所以

MinTrainTailPos∧MinTrainHeadPos→

TrainLength

(3) 最小車頭與最小VTP頭的位置一致，所以

MinTrainHeadPos → MinVTPHeadPos

(4) 最大VTP頭與最小VTP頭間距離為固定值MaxHeadLength，所以

MinVTPHeadPos→MaxVTPHeadPos

又因為MinTrainHeadPos→

MinVTPHeadPos

所以

MinTrainHeadPos→MaxVTPHeadPos

(5) 最大車尾與最小車尾間距離為固定值TailLength，所以

MinTrainTailPos → MaxTrainTailPos

(6) 最大車尾與最大車頭間距離為車長，所以

MaxTrainTailPos∧TainLength→

MaxTrainHeadPos

又因為MinTrainTailPos → MaxTrainTailPos

MinTrainTailPos∧MinTrainHeadPos→

TainLength

所以

MinTrainTailPos∧MinTrainHeadPos→

MaxTrainHeadPos

(7) 最大車尾與最大VTP尾間距離為固定值MaxTailLength，所以

MaxTrainTailPos → MaxVTPTailPos

又因為MinTrainTailPos → MaxTrainTailPos

所以

MinTrainTailPos → MaxVTPHeadPos

由此，一旦確定了最小車尾和最小車頭的具體坐標(biāo)，就能得到車長，另外6個列車的相關(guān)坐標(biāo)點位置也能相應(yīng)固定.所以Train可以約簡為

Train′={MinTrainTailPos,

MinTrainHeadPos, TrainMonitorModes}

此時，Train中的10個變量可約簡為Train’中的3個變量，系統(tǒng)驗證狀態(tài)空間得到了極大的約簡，有效降低了驗證復(fù)雜度.

3.3 EOA驗證實驗及分析

以圖3所示的國內(nèi)某地鐵線路數(shù)據(jù)作為環(huán)境，線路中共有6個block，并涵蓋2個道岔.在此環(huán)境下，基于SCADE工具直接對iZC系統(tǒng)模型進(jìn)行驗證.

圖3 驗證環(huán)境

按照文獻(xiàn)[5]中的投影方法，基于安全需求對驗證問題進(jìn)行投影后， iZC系統(tǒng)順利通過了形式化驗證.圖4展示了投影生成的SProblemEOA8的驗證結(jié)果.由圖4的結(jié)果可以看出，復(fù)雜環(huán)境下系統(tǒng)驗證狀態(tài)空間仍然較大，形式化驗證耗時較長.

圖4 投影后系統(tǒng)的驗證結(jié)果

按照第2節(jié)中的約簡方法，基于因果關(guān)系對變量進(jìn)行約簡后，環(huán)境輸出的變量減少，系統(tǒng)的復(fù)雜度進(jìn)一步降低，狀態(tài)空間進(jìn)一步縮小，形式化驗證的效率得到提高.由于消耗時間可能與工具運行狀態(tài)有關(guān)，可能存在一定的隨機性，所以每種類型在約簡前后均多次驗證，最終結(jié)果取多次驗證所耗時間的平均值進(jìn)行分析.變量約簡前后每種類型的待驗證系統(tǒng)進(jìn)行驗證所耗的時間如圖5所示.

圖5 變量約減前后驗證效率對比

由實驗結(jié)果可知，對于系統(tǒng)過于復(fù)雜，驗證時間較長的iZC系統(tǒng)，在對每種類型的驗證子系統(tǒng)分別進(jìn)行驗證時，基于因果關(guān)系對變量進(jìn)行約簡，使驗證所需的時間縮短，驗證效率得到了有效提高.由此在對整個iZC系統(tǒng)進(jìn)行驗證時，所需的總體時間明顯縮短，驗證效率顯著提升.

4 結(jié)論

本文針對列控系統(tǒng)的特點，在對列控系統(tǒng)進(jìn)行形式化驗證的過程中，提出可以利用列控系統(tǒng)各設(shè)備變量間的因果關(guān)系對驗證系統(tǒng)進(jìn)行化簡，形成基于因果關(guān)系的列車運行控制系統(tǒng)模型約簡方法.通過分析變量間的因果關(guān)系，在基于安全需求的列控系統(tǒng)投影方法的基礎(chǔ)上，針對投影得到的子系統(tǒng)，根據(jù)設(shè)備內(nèi)各變量之間存在的因果關(guān)系進(jìn)一步對環(huán)境的輸出變量進(jìn)行了約簡，從而減少了驗證系統(tǒng)的狀態(tài)空間.

本文以軌旁列控系統(tǒng)iZC的安全功能EOA為例，進(jìn)行EOA形式化驗證問題的投影及變量約減，并對8種EOA類型的驗證子系統(tǒng)分別進(jìn)行驗證.實驗結(jié)果表明，采用基于因果關(guān)系的列控系統(tǒng)模型約簡方法，能夠有效地提高形式化驗證的效率.

[1] Abrial J R. Modeling in Event-B: system and software engineering[M]. New York: Cambridge University Press, 2010.

[2] DaSilva C, Dehbonei B, Mejia F. Formal specification in the development of industrial applications: subway speed control system[C]//Proceedings 5th IFIP Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE’92). North-Holland: Perros-Guirec, 1993:199-213.

[3] Zou L, Lv J, Wang S,etal. Verifying Chinese control system under a combined scenario by theorem proving [C]//International Conference on Verified Software: Theories, Tools, Experiments (VSTTE). Berlin: Springer-Verlag, 2013: 262-280.

[4] Horste M, Hungar A, Schnieder E. Modelling functionality of train control systems using petri nets[R]. Madrid: FM-RAIL-BOK Workshop, 2013.

[5] Giannakopoulou D. Model checking for concurrent software architectures[D]. London: University of London, 1999.

[6] McMillan K L. Microarchitecture verification by compositional model checking[C/CD]∥Proceedings of the 13th International Conference Computer-aided Verification. Livingston: Springer-Verlag, 2011.

[7] McMillan K L. Parameterized verification of the FLASH cache coherence protocol by compositional model checking[C/CD]∥Correct Hardware Design and Verification Methods. Lecture Notes in Computer Science. Livingston: Springer-Verlag, 2001.

[8] JIN Zhi, CHEN Xiaohong, Zowghi Didar. Performing projection in problem frames using scenarios[C]//16th Asia-Pacific Software Engineering Conference. Piscataway: IEEE, 2009: 252-256.

[9] XU Jing, CHEN Xiaohong, ZHOU Tingliang, et al. Decomposing automatic train control verification system with projection[C]//22th Asia-Pacific Software Engineering Conference. Los Alamitos: IEEE Computer Society, 2015: 301-308.

[10] 陳小紅，尹斌，金芝. 基于問題框架方法的需求建模：一個本體制導(dǎo)的方法[J]. 軟件學(xué)報，2011, 22(2): 177.

CHEN Xiaohong, YIN Bin, JIN Zhi. Ontology-guided requirements modeling based on problem frames approach [J]. Journal of Software, 2011, 22(2): 177.

[11] Sanaz Yeganefard, Michael Butler. Problem decomposition and sub-model reconciliation of control systems in Event-B[C]//IEEE 14th International Conference on Information Reuse & Integration (IRI). Piscataway: IEEE, 2013: 528-535.

[12] Alebrahim Azadeh, Faβbender Stephan. Problem-based requirements interaction analysis[C]//20th International Working Conference. Cham: Springer International Publishing, 2014: 200-215.

[13] Backus J W. The syntax and semantics of the proposed international algebraic language of the Zurich ACM-GAMM Conference[C]//Proceedings of the International Conference on Information Processing. Paris: UNESCO, 1959: 125-132.

[14] IEEE. IEEE Std 1474.1 Standard for communications-based train control (CBTC) performance and functional requirements[S]. [S.l.]: IEEE, 2004.

Automatic Train Control System Model Reduction Based on Causal Relation

ZHOU Tingliang1,2, XU Jing2, CHEN Xiaohong3,ZHAO Shimin1

(1.Key Laboratory of Road and Traffic Engineering of the Ministry of Education, Tongji University,Shanghai 201804, China; 2.CASCO Signal Ltd., Shanghai 200071, China; 3. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai 200062, China)

Based on the previous work about verification problem projection according to the safety requirements, a variable reduction approach was proposed based on causal relation for the projected sub-problems. First, the causal relations among the environment variables of the projected sub-problems were defined. Then, the basic causal relation combination of variables and the reduction rules were concluded. Through variable reduction, the state space of the verification problem was reduced. Finally, with configuration of a domestic metro line, an experiment of modeling and verification was demonstrated to show that the variable reduction approach efficiently reduces the verification complexity.

requirement verification; variable reduction; causal relation; automatic train control system

2016-03-29

國家自然科學(xué)基金(91418203)

周庭梁(1980—)，男，博士生，主要研究方向為軌道交通列車列控系統(tǒng)研制、測試及安全評估.E-mail:Leon_ztl@163.com

TP311

A