趙夢瑤 , 陳小紅 , 孫海英 , 劉 靜 , 陳良育 , 周庭梁

1(上海市高可信計算重點實驗室(華東師范大學(xué)),上海 200062)2(卡斯柯信號有限公司,上海 200071)

軌道交通聯(lián)鎖系統(tǒng)是以計算機(jī)、現(xiàn)代多媒體和通信網(wǎng)絡(luò)技術(shù)等技術(shù)為手段,以道岔機(jī)、信號機(jī)和軌道電路作為基礎(chǔ)設(shè)備,主要負(fù)責(zé)處理進(jìn)路內(nèi)的信號機(jī)、道岔、軌道電路之間的安全聯(lián)鎖關(guān)系[1].它包括實現(xiàn)聯(lián)鎖關(guān)系、建立進(jìn)路、控制道岔的轉(zhuǎn)換和信號燈的開放以及進(jìn)路解鎖,是軌道交通信號系統(tǒng)中不可或缺的核心部分,是保證列車行車安全的重要子系統(tǒng).它有歐盟安全完整性等級最高的SIL4 級安全需求[2]、復(fù)雜的邏輯和很高的實時性能,若發(fā)生故障,則能危害整列車的安全.因此,必須確保聯(lián)鎖系統(tǒng)的高安全性.

為了保證這樣的安全性,目前很多歐洲鐵路控制與防護(hù)標(biāo)準(zhǔn),如EN50128[2],EN50129[3]等強(qiáng)烈推薦在開發(fā)之前,使用形式化方法進(jìn)行建模和分析.形式化方法以嚴(yán)密的數(shù)學(xué)理論和相關(guān)推理為基礎(chǔ),有嚴(yán)格的語法規(guī)范和確定的語義定義,并且是自證正確的,因此非常適用于開發(fā)聯(lián)鎖系統(tǒng)這樣安全攸關(guān)的系統(tǒng).但是,形式化方法又有著固有的學(xué)習(xí)成本高、不易使用的缺點.一般來說,領(lǐng)域?qū)＜业男问交ｋx不開形式化專家的幫助,建模的主體依然是形式化的專家.在聯(lián)鎖系統(tǒng)這類領(lǐng)域知識特別復(fù)雜的系統(tǒng)中,領(lǐng)域?qū)＜倚枰焖贅?gòu)建模型并分析復(fù)雜業(yè)務(wù)邏輯,根據(jù)分析結(jié)果快速進(jìn)行錯誤定位與錯誤修正,建模與分析的主體應(yīng)該是領(lǐng)域?qū)＜?如何讓領(lǐng)域?qū)＜夷茏灾鳂?gòu)建形式化模型,是一個需要解決的問題.

現(xiàn)有的軌道交通領(lǐng)域的形式化建模工作主要分為3 類:基于自然語言的形式化方法、基于半形式化的方法和基于領(lǐng)域特定語言(DSL)的方法.基于自然語言的形式化建模[4-6]都是形式化專家根據(jù)領(lǐng)域?qū)＜业淖匀徽Z言描述直接建立形式化模型,并采用相應(yīng)的形式化驗證工具進(jìn)行性質(zhì)驗證,這類方法需要領(lǐng)域?qū)＜液托问交瘜＜业木o密合作,對于不具有形式化知識的領(lǐng)域?qū)＜襾碇v很難使用.基于半形式化的形式化建模與驗證中[7-11],先由領(lǐng)域?qū)＜沂褂冒胄问交Z言(例如UML)描述系統(tǒng),然后形式化專家再把半形式化模型轉(zhuǎn)換為形式化模型并進(jìn)行形式化分析.但這些半形式化語言都是軟件專業(yè)建模語言,不是領(lǐng)域?qū)＜宜瞄L的語言.基于領(lǐng)域特定語言的形式化建模與驗證中[12-15],首先由領(lǐng)域?qū)＜沂褂妙I(lǐng)域特定語言描述系統(tǒng),然后形式化專家再把領(lǐng)域特定語言模型轉(zhuǎn)換為形式化模型并進(jìn)行形式化分析.例如,Idani 等人[12]將圖形領(lǐng)域定制語言的模型轉(zhuǎn)換為形式化B 模型.這類方法允許領(lǐng)域?qū)＜抑灰鶕?jù)領(lǐng)域特定語言給出領(lǐng)域模型,就可以享受形式化方法帶來的好處,便于形式化專家和領(lǐng)域?qū)＜业暮献?也減少了人工建模出錯誤的可能性.

基于以上分析,我們認(rèn)為,基于領(lǐng)域特定語言的建模方法更方便領(lǐng)域?qū)＜沂褂?但現(xiàn)有的基于特定語言的方法并不能直接應(yīng)用于聯(lián)鎖系統(tǒng),原因如下:

(1) 使用的形式化模型,如文獻(xiàn)[12]使用的B 方法和文獻(xiàn)[13]使用的時間弧Petri 網(wǎng)等,并不能應(yīng)對聯(lián)鎖系統(tǒng)的故障隨機(jī)性和行為實時性的特點.聯(lián)鎖系統(tǒng)中,事故通常是由設(shè)備故障造成的,而設(shè)備故障通常具有隨機(jī)性的特點,例如由雷擊等意外事件導(dǎo)致軌道電路出現(xiàn)短路等故障.同時,聯(lián)鎖系統(tǒng)屬于典型的實時系統(tǒng),邏輯復(fù)雜且有較高的實時性要求[16];

(2) 可重用構(gòu)件多,需要多次重用列車、軌道等構(gòu)件.聯(lián)鎖系統(tǒng)在各個站的組成都類似,每個站的聯(lián)鎖系統(tǒng)都有著相同的構(gòu)件,如列車、軌道、道岔、信號燈、聯(lián)鎖表、控制器,它們的主要區(qū)別在于車站布局(車站站場圖)不同導(dǎo)致的實例個數(shù)不同.

因此,在前期工作基礎(chǔ)上[14,15],本文提出了基于模板的聯(lián)鎖系統(tǒng)模型生成方法,建立聯(lián)鎖系統(tǒng)的特定領(lǐng)域語言,通過模板重用,允許領(lǐng)域?qū)＜腋鶕?jù)實際需要自行構(gòu)建系統(tǒng)模型,而不必接受形式化方法的培訓(xùn).這種模板可以用能建模故障隨機(jī)性和實時性的隨機(jī)混成自動機(jī)[17]或價格時間自動機(jī)[18]進(jìn)行構(gòu)建.

本文首先由領(lǐng)域?qū)＜覍β?lián)鎖系統(tǒng)模型進(jìn)行分析,根據(jù)不同案例設(shè)計其領(lǐng)域特定語言;其次,由領(lǐng)域?qū)＜掖_定聯(lián)鎖系統(tǒng)模型的模板組成,并由形式化專家抽取系統(tǒng)模型的模板,舉例構(gòu)建其隨機(jī)混成自動機(jī)模板;然后,由領(lǐng)域?qū)＜彝ㄟ^領(lǐng)域特定語言輸入?yún)?shù)自動生成系統(tǒng)模型.本文以某站聯(lián)鎖系統(tǒng)為例,自動構(gòu)建了其系統(tǒng)的混成自動機(jī)模型,并在驗證平臺UPPAAL-SMC 上進(jìn)行事故預(yù)測分析,證明了本文方法的可行性和有效性.

本文第1 節(jié)介紹隨機(jī)混成自動機(jī)概念和UPPAAL-SMC.第2 節(jié)給出自動生成聯(lián)鎖系統(tǒng)模型的方法框架.第3 節(jié)定義聯(lián)鎖領(lǐng)域特定語言IS-DSL.第4 節(jié)確定聯(lián)鎖系統(tǒng)的模板組成,并舉例用隨機(jī)混成自動機(jī)構(gòu)建模型模板.第5 節(jié)在模板基礎(chǔ)上,根據(jù)領(lǐng)域特定語言輸入?yún)?shù)自動生成具體的系統(tǒng)模型.第6 節(jié)針對某站的實際情況進(jìn)行系統(tǒng)的生成和事故預(yù)測分析,驗證了本文方法的可行性和有效性.第7 節(jié)介紹相關(guān)工作.最后,第8 節(jié)總結(jié)全文并給出進(jìn)一步的研究方向.

1 預(yù)備知識

本節(jié)主要介紹一些概念和知識,主要包括隨機(jī)混成自動機(jī)和UPPAAL-SMC[19]平臺.隨機(jī)混成自動機(jī)是一種被廣泛接受的混合系統(tǒng)模型,也是建模時間和隨機(jī)性的重要模型,已經(jīng)被廣泛應(yīng)用于計算機(jī)仿真、自動機(jī)及其他領(lǐng)域[20].隨機(jī)混成自動機(jī)包含了隨機(jī)特性,在引入隨機(jī)事件后,更適合于以故障診斷為目的的建模.與傳統(tǒng)時間自動機(jī)(time automata,簡稱TA)[21,22]不同,隨機(jī)混成自動機(jī)提供對離散行為、連續(xù)行為和隨機(jī)行為的描述,對存在隨機(jī)行為的混成系統(tǒng)能夠很好的建模.隨機(jī)混成自動機(jī)的定義是一個七元組H=(L,l0,X,Σ,E,F,I),其中,L是有限位置集合;l0∈L是開始位置集合;X是連續(xù)變量的有限集;Σ是動作的有限集;E是遷移的有限集,其中每條遷移邊可表示為(l,g,a,φ,l′),其中,l和l′表示位置,g為定義在Rx上的謂詞,動作標(biāo)簽a∈Σ,φ是定義在Rx上的二元關(guān)系;對于每一個位置l,F(l)是其時間延遲函數(shù),I(l)是其不變式.

通過廣播信道和共享變量,不同的隨機(jī)混成自動機(jī)之間相互通信,組成隨機(jī)混成自動機(jī)網(wǎng)絡(luò)(network of stochastic hybrid automata,簡稱NSHA).圖1 展示了一個由隨機(jī)混成自動機(jī)A和B組成的隨機(jī)混成自動機(jī)網(wǎng)絡(luò).A有5 個狀態(tài):A0～A4,有一個時鐘變量x.B有4 個狀態(tài):B0～B3,有一個時鐘變量y.在狀態(tài)A0 中,x′==0 表示x的值在狀態(tài)A0 處沒有改變.在狀態(tài)A1 中,標(biāo)志1 表示A在狀態(tài)A1 處的延遲遵循λ=1 的指數(shù)分布.在狀態(tài)A2 中,x≤1為不變式,在該狀態(tài),時鐘x始終滿足該不變式.實線箭頭表示狀態(tài)之間的轉(zhuǎn)換,在遷移上有“guard”,“update”和“sync”,分別表示遷移條件、變量更新和同步.在狀態(tài)A2 到A4 的遷移上,“guard”為x≥1,表示當(dāng)x≥1 時遷移才會發(fā)生,“update”為x:=0,表示更新x的值為0.

Fig.1 An example of NSHA圖1 隨機(jī)混成自動機(jī)網(wǎng)絡(luò)樣例

隨機(jī)混成自動機(jī)支持不確定性操作,例如A離開狀態(tài)A0 時有兩個目標(biāo)狀態(tài),A1 和A2.隨機(jī)混成自動機(jī)用帶有權(quán)重信息的虛線箭頭表示進(jìn)入目標(biāo)狀態(tài)的概率.例如,從狀態(tài)A0 到狀態(tài)A1 的概率為3/(3+7),從狀態(tài)A0 到狀態(tài)A2 的概率為7/(3+7).為了使在一個隨機(jī)混成自動機(jī)網(wǎng)絡(luò)中的兩個隨機(jī)混成自動機(jī)進(jìn)行同步,各隨機(jī)混成自動機(jī)通過廣播信道和共享變量相互進(jìn)行通信.例如在圖1 中,兩個隨機(jī)混成自動機(jī)通過廣播信道a進(jìn)行通信,a?表示廣播信道a接收消息,a!表示廣播信道a發(fā)送信息.在進(jìn)行發(fā)送和接收操作的同步之后,兩個隨機(jī)混成自動機(jī)同時進(jìn)入各自的下一狀態(tài),如圖1 中所示,狀態(tài)A2 轉(zhuǎn)換到狀態(tài)A4,狀態(tài)B0 轉(zhuǎn)換到狀態(tài)B1.

UPPAAL-SMC 是一個工具環(huán)境,支持隨機(jī)混成自動機(jī)的建模、仿真與驗證,它是UPPAAL[23]工具鏈中對統(tǒng)計模型檢驗(statistical model checking,簡稱SMC)[24]支持的擴(kuò)展.目前,UPPAAL-SMC 在各種研究領(lǐng)域中被廣泛接受,例如軌道交通領(lǐng)域和軟件工程領(lǐng)域等[25,26].UPPAAL-SMC 提供了許多時間自動機(jī)的隨機(jī)解釋的相關(guān)查詢,同時允許用戶可視化地模擬運行表達(dá)式的值.本文在UPPAAL-SMC 中用到查詢語法如下:

其中,N為自然數(shù),表示要進(jìn)行仿真的次數(shù);bound為仿真的時間限制;E1,…,Ek是k個表達(dá)式,可被監(jiān)控和可視化.

2 方法框架

為實現(xiàn)列車行車的安全性,聯(lián)鎖系統(tǒng)的首要目的是在允許列車移動的同時,控制道岔和信號燈以防止列車發(fā)生相撞或脫軌[27].其主要功能是通過軌道電路監(jiān)視相關(guān)軌道段的占用情況、控制道岔位置、發(fā)送信號給列車司機(jī),告知其是否能進(jìn)入軌道.其通常的工作流程如下:(1) 列車(train)向控制器(controller)發(fā)出請求申請進(jìn)路并等候回饋;(2) 控制器收到列車請求后,查詢聯(lián)鎖表(interlock table),聯(lián)鎖表將進(jìn)路結(jié)果返回給控制器;(3) 控制器檢查該進(jìn)路軌道占用情況,軌道(track)收到控制器指令后,檢查占用情況,并向控制器返回結(jié)果;(4) 控制器對軌道占用情況檢測完畢后鎖閉道岔(point)并命令道岔移動到相應(yīng)位置,道岔移動完成后向控制器反饋;(5) 控制器完成對道岔的控制后向信號燈(signal light)發(fā)送變綠信號,控制信號燈變綠;(6) 控制器在列車駛出軌道后解鎖相應(yīng)的道岔、控制相應(yīng)的信號燈變紅,整個流程結(jié)束.

從上述流程中可知:聯(lián)鎖系統(tǒng)的運行不僅僅只涉及控制器,還涉及列車、軌道、道岔、信號燈和聯(lián)鎖表.其中,列車包含其車載系統(tǒng),軌道分為多個區(qū)段,每個區(qū)段與一個軌道電路相關(guān)聯(lián),用以檢測軌道是否被列車占用.道岔是軌道的連接處,根據(jù)道岔的不同位置,列車可以駛?cè)氩煌倪M(jìn)路.道岔可以處于解鎖與鎖閉兩種狀態(tài),且若其處于解鎖狀態(tài),則表明該道岔未與岔口相連.當(dāng)?shù)啦硖幱阪i閉狀態(tài)時,列車才能通過該道岔.信號燈位于不同的軌道區(qū)段之間,其狀態(tài)為紅燈或者綠燈,表明列車應(yīng)該停止或允許前進(jìn).進(jìn)路由聯(lián)鎖表定義,一般在鐵路站場設(shè)計時被創(chuàng)建,每個進(jìn)路由按拓?fù)浣Y(jié)構(gòu)順序連接的軌道段組成,只有在進(jìn)路建立后,列車才能獲準(zhǔn)進(jìn)入該進(jìn)路.所有的這些一般都可以從一個站場圖中獲得,例如從圖2 可以看出,該站場包含2 個道岔(SW1,SW2)、9 個信號燈(S1～S9)與7 段軌道(T1～T7).

Fig.2 Track layout of a station圖2 某站的站場圖

要建立一個聯(lián)鎖系統(tǒng)的模型,不僅僅是要建?？刂破?還需要建模與其交互的環(huán)境,這些環(huán)境包括多輛列車、多段軌道、多個道岔、多盞信號燈和一個聯(lián)鎖表.在不同的車站,其站場圖不同,系統(tǒng)模型也會不同.也就是說,聯(lián)鎖系統(tǒng)在各個站的組成都類似,它們的主要區(qū)別在于車站站場圖不同導(dǎo)致的實例個數(shù)不同.從中也不難發(fā)現(xiàn),雖然構(gòu)件數(shù)量不同,但構(gòu)件類型是固定的,也就是說,每個聯(lián)鎖系統(tǒng)都會涉及控制器、列車、軌道、道岔、信號燈和聯(lián)鎖表.我們可以將每種類型的構(gòu)件抽取出來做成模板,進(jìn)行形式化建模.在模板的形式化建模中,適用的語言要可以應(yīng)對設(shè)備故障的隨機(jī)性以及較高的實時性要求,可以采用隨機(jī)混成自動機(jī)和價格時間自動機(jī)進(jìn)行建模.

各個聯(lián)鎖系統(tǒng)模型的不同,主要是構(gòu)件數(shù)量的不同,但后面我們也發(fā)現(xiàn)有其他的不同.比如,為了安全的目的,需要建模異常,包括設(shè)備故障的概率等等.可以將這些不同抽取出來,定義為領(lǐng)域特定語言,由領(lǐng)域?qū)＜疫M(jìn)行設(shè)定,然后可以跟構(gòu)件模板結(jié)合起來形成完整的系統(tǒng)模型,便于后續(xù)的安全分析.基于上述分析,我們設(shè)計了基于模板的聯(lián)鎖系統(tǒng)生成和應(yīng)用框架,如圖3 所示.

· 首先,由領(lǐng)域?qū)＜腋鶕?jù)領(lǐng)域特定語言提供模型參數(shù)列表;

· 然后,結(jié)合由形式化專家建立的系統(tǒng)模板進(jìn)行特定系統(tǒng)模型生成.系統(tǒng)模板由兩部分組成:環(huán)境模板和控制器模板.其中:環(huán)境模板包括了聯(lián)鎖系統(tǒng)的每個環(huán)境構(gòu)件的模型,包括火車、道岔、聯(lián)鎖表、信號燈和軌道;控制器模板定義了控制器的行為模式.在結(jié)合模板過程中,可以實例化系統(tǒng)中的各個模板,以便生成特定的系統(tǒng)模型;

· 最后在UPPAAL-SMC 平臺上模擬生成的系統(tǒng)模型,獲取仿真數(shù)據(jù),結(jié)合安全性質(zhì)進(jìn)行安全分析,以驗證系統(tǒng)的安全性.

Fig.3 Framework of our approach圖3 方法框架

3 聯(lián)鎖領(lǐng)域特定語言IS-DSL

根據(jù)上述分析,聯(lián)鎖系統(tǒng)的模型首先在構(gòu)件的數(shù)量上是不同的,也就是說,列車、道岔、信號燈和軌道實例化的個數(shù)隨案例變化.這些構(gòu)件的數(shù)量要成為語言的一部分.不僅如此,由于這些實體數(shù)量的變化,導(dǎo)致其進(jìn)路表是不同的.假設(shè)圖2 這樣的站場中包含3 條進(jìn)路,R1～R3,R1 由軌道段T1～T3,T6 和T7 組成,需要信號燈S1～S4和S9 為綠燈,道岔SW1 和SW2 向上打開;R2 由軌道段T1,T2,T4,T6 和T7 組成,需要信號燈S1,S2,S5,S6 和S9 為綠燈,道岔SW1 和SW2 向前打開;R3 由軌道段T1,T2,T5～T7 組成,需要信號燈S1,S2,S7～S9 為綠燈,道岔SW1 和SW2 向下打開.其進(jìn)路表見表1.

Table 1 Interlocking table of a station表1 某站的聯(lián)鎖表

這樣的一個聯(lián)鎖表的表示也應(yīng)該成為領(lǐng)域特定語言的一部分.我們發(fā)現(xiàn):一個聯(lián)鎖表是由進(jìn)路組成,每個進(jìn)路又包含一系列的軌道,軌道邊上又有信號燈和道岔,因此,可以將聯(lián)鎖表定義為一組進(jìn)路,每個進(jìn)路有自己的標(biāo)識(rid)和軌道序列,每段軌道使用軌道的標(biāo)識符(tr_id)、進(jìn)入該軌道所需的信號燈的標(biāo)識符(li_id)和道岔標(biāo)識符(p_id)及道岔方向組成,那么每個進(jìn)路可以表示為

以表1 中的R1 為例,表示為:R1:T1(S1)→T2(S2)→T3(S3;SW1:UP)→T6(S4;SW2:UP)→T7(S9).R1 包括T1～T3,T6,T7 這5 段軌道,其中,T3(S3;SW1:UP)表示進(jìn)入軌道T3 需要信號燈S3 為綠燈狀態(tài),道岔SW1 的方向向上.

除了數(shù)量之外,我們發(fā)現(xiàn)還有兩種類型的不同.一種是構(gòu)件發(fā)生故障的概率.這個是從安全角度考慮,不同的構(gòu)件由于購買時間、使用時間、放置的場景不同,其發(fā)生故障的概率是不同的.這個概率可能是一個具體的數(shù)字,比如超過5 年之后,信號燈壞的概率為30%,還有可能這個概率只是符合某一種分布,比如正態(tài)分布、均勻分布或者指數(shù)分布.故障發(fā)生概率這種類型跟安全關(guān)系很大,可以通過統(tǒng)計規(guī)律得到,屬于領(lǐng)域?qū)＜业募夹g(shù)范疇,因此我們也將它設(shè)計在聯(lián)鎖特定語言中.另一種是構(gòu)件的物理特性的不同.這些物理特性包括列車的最大允許速度、列車的最大加速度、軌道的長度、列車的發(fā)車間隔時間等.這些物理性質(zhì)因車而異、因軌道而異,但是跟安全又有著莫大的關(guān)系,是領(lǐng)域?qū)＜沂煜さ?因此也將它們設(shè)計在語言中.

總之,本文總結(jié)出3 種類型的不同案例的聯(lián)鎖系統(tǒng)模型的不同,包括構(gòu)件數(shù)量的不同、構(gòu)件發(fā)生故障的概率不同以及構(gòu)件物理特性的不同.分別將這3 種不同定義到聯(lián)鎖特定語言中,由此得到了聯(lián)鎖領(lǐng)域特定語言IS-DSL,如圖4 所示.

Fig.4 IS-DSL圖4 聯(lián)鎖系統(tǒng)領(lǐng)域特定語言

4 系統(tǒng)模型的模板

4.1 模板的基本組成

針對聯(lián)鎖系統(tǒng)的特性,結(jié)合我們之前的工作[14,15],本節(jié)設(shè)計模板的基本組成.首先,系統(tǒng)模板可以分為控制器模板和環(huán)境模板,其中,環(huán)境模板包含列車、軌道、道岔、信號燈和聯(lián)鎖表.根據(jù)聯(lián)鎖系統(tǒng)的處理流程,它們之間的交互如下:列車進(jìn)入軌道前向控制器發(fā)出請求進(jìn)路信號“request”,控制器收到請求后,向聯(lián)鎖表發(fā)送查詢信號“checkTable”,聯(lián)鎖表將結(jié)果“result”返回給控制器.控制器根據(jù)聯(lián)鎖表返回信息,向相應(yīng)軌道發(fā)送檢測占用狀態(tài)命令“checkOccupied”,軌道收到控制器命令后,向控制器返回占用狀態(tài)“occupied”或未占用狀態(tài)“allUnoccupied”.若軌道狀態(tài)為未被占用,則控制器向道岔發(fā)出道岔鎖閉信號“doLock”,收到道岔發(fā)出的鎖閉狀態(tài)信號“turnLock”后,向信號燈發(fā)出變綠信號“doGreen”,列車收到信號燈發(fā)出的綠燈信號“green”后,進(jìn)入軌道,發(fā)出駛?cè)胄盘枴皌rainEnter”,軌道設(shè)置狀態(tài)為占用狀態(tài).列車駛出軌道后,發(fā)出信號“trainLeave”,控制中心收到該信號后解鎖相應(yīng)的道岔、控制相應(yīng)的信號燈變紅,軌道收到該信號后設(shè)置狀態(tài)為未占用狀態(tài).

在這樣的交互過程中,由于軌道、道岔、信號燈以及列車的數(shù)量都不止一個,控制器作為處理所有的控制邏輯的單元,其控制邏輯非常復(fù)雜,不方便復(fù)用.因此,本文將控制器中將對列車的調(diào)度、軌道的檢測、道岔的處理以及信號燈的處理邏輯都分別拆分出來,將控制器分為5 部分:控制中心(center)、軌道檢測子模塊(CTrack)、道岔處理子模塊(CPoint)、信號燈處理子模塊(CSignalLight)以及列車調(diào)度器(dispatcher),即:

其中,控制中心負(fù)責(zé)控制所有的軌道、道岔、信號燈、列車、聯(lián)鎖表;列車調(diào)度器負(fù)責(zé)向不同的列車發(fā)送調(diào)度信號“send”,用以控制不同列車在不同的時刻進(jìn)入同一軌道;軌道檢測子模塊負(fù)責(zé)向每一條軌道發(fā)送“checkOccupied”消息,用以檢查每條軌道的占用情況;道岔處理子模塊向每個道岔發(fā)送“doLock”“doUnlock”消息,用以控制道岔狀態(tài)變化;信號燈處理子模塊向每個信號燈發(fā)送“doGreen”“doRed”消息,用以控制信號燈狀態(tài)變化.

在上述的所有模塊中,道岔處理子模塊和信號燈處理子模塊都涉及對多個道岔和信號燈的多種控制,包括“doLock”與“doUnlock”“doGreen”與“doRed”,為了方便,我們將其分解為對多個道岔和信號燈的單信號控制.以道岔處理子模型為例,將其分為兩部分:道岔鎖閉子模塊(ControlPointLock)負(fù)責(zé)控制每個道岔鎖閉,道岔解鎖子模塊(ControlPointUnlock)負(fù)責(zé)控制每個道岔解鎖.類似地,可以將信號燈處理子模塊(CSignalLight)分解為兩部分:綠燈控制子模塊(ControlLightGreen)負(fù)責(zé)控制每個信號燈變綠,紅燈控制子模塊(ControlLightRed)負(fù)責(zé)控制每個信號燈變紅.

站在環(huán)境的立場,Track 和SingalLight 兩種構(gòu)件均涉及設(shè)置狀態(tài)和查詢狀態(tài)兩種操作,為保證設(shè)置構(gòu)件狀態(tài)期間能正常查詢構(gòu)件的狀態(tài),我們將其拆分為設(shè)置子模塊和查詢子模塊.以軌道為例,我們將軌道涉及的操作分為兩部分:一部分為軌道設(shè)置(STrack),負(fù)責(zé)對軌道的狀態(tài)進(jìn)行設(shè)置;另一部分為軌道查詢(RTrack),負(fù)責(zé)對軌道的狀態(tài)進(jìn)行查詢,即Track=STrack||RTrack.類似地,我們將信號燈涉及的操作分為兩部分:一部分為信號燈設(shè)置(SSignalLight),負(fù)責(zé)對信號燈的狀態(tài)進(jìn)行設(shè)置;另一部分為信號燈查詢(RSignalLight),負(fù)責(zé)對信號燈的狀態(tài)進(jìn)行查詢,即SignalLight=SSignalLight||RSignalLight.

綜上所述,將系統(tǒng)模型的模板分為兩大部分,控制器與環(huán)境,而控制器又可以分為7 個子模塊,環(huán)境也分為7個子模塊,這些模塊之間相互發(fā)送消息,通過協(xié)作,共同完成控制器的功能,具體的分解和協(xié)作關(guān)系如圖5 所示.

Fig.5 Interlocking system template圖5 聯(lián)鎖系統(tǒng)模板

4.2 模板抽取舉例

對于圖5 中的每個模塊的模板,都需要構(gòu)建其形式化模型.本節(jié)以SHA 為例,說明如何構(gòu)建其模板.在所有的模板構(gòu)造中,我們發(fā)現(xiàn)有兩種類型的模板.一種是抽取后固定,形狀不再發(fā)生變化,要變化的只是參數(shù),這類模板包括列車模板、信號燈設(shè)置模板、軌道設(shè)置模板、道岔模板和控制中心模板;另一種是需要針對一組構(gòu)件進(jìn)行建模,其模板分為兩部分:先對一個構(gòu)件進(jìn)行建模,然后根據(jù)領(lǐng)域特定語言的參數(shù)進(jìn)行動態(tài)生成,我們給出具體的生成算法.這類模板叫組合模板,圖5 中的聯(lián)鎖表模板、信號燈查詢模板、軌道查詢模板、軌道檢測子模塊模板、道岔處理子模塊模板、信號燈處理子模塊模板與調(diào)度模板都是這種類型.

由于模板很多,我們針對每種類型各舉一例,說明如何建立模板的模型.其他模板的抽取過程類似,可以參閱https://github.com/zmy3036190149/SHA.

4.2.1 固定模板

這種類型的模板抽取主要是首先根據(jù)系統(tǒng)的處理流程找到與構(gòu)件相關(guān)的過程描述,包括與構(gòu)件相關(guān)的所有行為,構(gòu)建其基本時間自動機(jī).每次構(gòu)件發(fā)送或接收消息(動作)時,構(gòu)件的自動機(jī)從一個狀態(tài)移動到另一個狀態(tài).每個構(gòu)件的動作被轉(zhuǎn)換為基本自動機(jī)中的狀態(tài)和轉(zhuǎn)換.在此基礎(chǔ)上進(jìn)行故障建模,異常事件可用概率進(jìn)行表示,故在上一步生成的時間自動機(jī)上增加隨機(jī)概率事件,用于表示構(gòu)件發(fā)生的異常事件,用不同概率模擬構(gòu)件發(fā)生不同事件的情況.最后增加時間約束,可以采用隨機(jī)混成自動機(jī)的狀態(tài)上的跳轉(zhuǎn)延遲來表示時間約束.若狀態(tài)跳轉(zhuǎn)延遲服從指數(shù)分布,在該狀態(tài)設(shè)置指數(shù)分布的參數(shù);若服從均勻分布,則定義相應(yīng)的時鐘變量x和常量T,表示一條遷移上的消息到另一條遷移上的消息之間的時間.在時間自動機(jī)中前一條遷移的“update”內(nèi)賦時鐘變量初值為0,在中間狀態(tài)將時鐘限制為x≤T,在后一條遷移的“guard”內(nèi)定義時鐘變量的不等式x>T.針對連續(xù)變量的時間約束,首先定義相應(yīng)的連續(xù)變量,然后在各遷移上添加連續(xù)變量的更新表達(dá)式及判斷條件,在各個狀態(tài)上添加連續(xù)變量的變化函數(shù).

下面選取信號燈設(shè)置模型SSignalLight 的模板抽取作為例子進(jìn)行說明.

在構(gòu)造基本時間自動機(jī)時,SSignalLight 接收變綠信號“doGreen”后發(fā)送綠燈信號“turnGreen”;接收變紅信號“doRed”后發(fā)送紅燈信號“turnRed”.根據(jù)該流程,獲得了SSignalLight 的基本自動機(jī).在此基礎(chǔ)上進(jìn)行故障建模,信號燈在由紅燈狀態(tài)到綠燈狀態(tài)和由綠燈狀態(tài)到紅燈狀態(tài)的變化過程中可能發(fā)生故障,即在收到“doGreen”消息到發(fā)出“turnGreen”消息之間和收到“doRed”消息到發(fā)出“turnRed”消息之間發(fā)生故障.故在時間自動機(jī)中增加一個錯誤狀態(tài)(error).消息為“doGreen”的遷移到錯誤狀態(tài)間有一條概率為m%的遷移,到消息為“turnGreen”的遷移間有一條概率為n%的遷移,其中,m+n=100.類似可以建模從綠燈狀態(tài)到紅燈狀態(tài)變化過程中信號燈出現(xiàn)故障的情況.

增加時間約束時,從領(lǐng)域知識中可獲知SSignalLight 的時間約束,即信號燈狀態(tài)變化有延遲.根據(jù)時間約束定義時鐘變量,定義局部時鐘a表示信號燈由紅燈狀態(tài)變?yōu)榫G燈狀態(tài)的變化延遲時間,局部時鐘b表示信號燈由綠燈狀態(tài)變?yōu)榧t燈狀態(tài)的變化延遲時間.時鐘a為信號燈由紅燈狀態(tài)變?yōu)榫G燈狀態(tài)的延遲時間,即從RED 狀態(tài)收到“doGreen”消息到下一狀態(tài)GREEN 的時間.故在遷移“dogreen”的“update”上將a賦值為0,并在中間狀態(tài)將a限制為“a≤T”,在下一條遷移的“guard”上定義a的不等式“a>T”.類似在時間自動機(jī)中定義時鐘變量b,由此得到SSignalLight 的隨機(jī)混成自動機(jī)如圖6(a)所示.

Fig.6 SHA template of signal light圖6 信號燈隨機(jī)混成自動機(jī)模板

4.2.2 組合模板

這類模板主要是針對一組構(gòu)件進(jìn)行建模.首先對一個構(gòu)件進(jìn)行建模.具體如何建模取決于這組構(gòu)件要做什么事情,這來自于系統(tǒng)的處理流程中與構(gòu)件相關(guān)的過程描述.在這個描述中,依然可以遵循“每次構(gòu)件發(fā)送或接收消息(動作)時,構(gòu)件的自動機(jī)從一個狀態(tài)移動到另一個狀態(tài)”的規(guī)律轉(zhuǎn)換.與構(gòu)建固定模板步驟相同,在構(gòu)建其基本自動機(jī)后,需進(jìn)行故障建模和增加時間約束.接下來,在一個構(gòu)件模型的基礎(chǔ)上對一組構(gòu)件進(jìn)行建模,假設(shè)該組構(gòu)件數(shù)量為n.遍歷一個構(gòu)件模型的所有遷移,若遷移的同步信息針對單個環(huán)境構(gòu)件分兩種情況處理:(1) 若遷移起始和終點是同一狀態(tài),則根據(jù)環(huán)境構(gòu)件數(shù)量n,增加n-1 條遷移,并修改遷移上的“guard”“sync”和“update”信息;(2) 若遷移起始和終點不是同一狀態(tài),則增加n-1 條遷移和n-1 個狀態(tài),并修改遷移和狀態(tài)相關(guān)信息.若遷移的判斷條件是針對單個環(huán)境構(gòu)件,則修改遷移條件為n個條件的組合.

下面我們以信號燈查詢模型RSignalLight 的模板抽取為例,說明這種模板抽取的過程.為了得到一組信號燈的情況,先對一個信號燈進(jìn)行建模.RSignalLight 接收到“turnGreen?”消息時,對綠燈標(biāo)識符(isLightgreen)賦值為真,當(dāng)isLightgreen 為true 時,發(fā)送消息”green!”,當(dāng)isLightred 為true 時,發(fā)送消息“red!”.根據(jù)該流程,獲得了RSignalLight-Single 的隨機(jī)混成自動機(jī)模板,如圖6(b)所示.

一組信號燈建模過程在一個信號燈的基礎(chǔ)上進(jìn)行,增加相應(yīng)的不同信號燈的綠燈標(biāo)識符和紅燈標(biāo)識符.對于n個信號燈,則應(yīng)有n個紅燈標(biāo)識符和n個綠燈標(biāo)識符,定義數(shù)組isLightgreen[n],isLightred[n].從初始狀態(tài)到初始狀態(tài),增加n條消息為“turnGreen[i]?”的遷移,對isLightgreen[i]賦值為真.消息為“green!”的遷移判斷條件通過函數(shù)isLightgreen(rid)確定,rid 為進(jìn)路ID,若進(jìn)路rid 上的信號燈均為綠燈狀態(tài),則返回true.類似得到消息為“red!”的遷移判斷條件.具體的生成算法見算法1.

算法1.RSignalLight 模板生成算法.

5 系統(tǒng)模型的自動生成

根據(jù)UPPAAL-SMC 平臺中模型的運行,系統(tǒng)模型應(yīng)該包含模型聲明、環(huán)境模型和控制器模型以及環(huán)境與控制器的交互.全局變量以及交互經(jīng)常定義在聲明中.以圖5 中的環(huán)境模板、控制器模板和領(lǐng)域特定語言表示的案例為輸入,進(jìn)行系統(tǒng)模型的生成,需要理清楚這些聲明從哪里來,如何對環(huán)境模板進(jìn)行實例化,對控制器進(jìn)行實例化以及對交互進(jìn)行實例化.

在環(huán)境模板進(jìn)行實例化時,根據(jù)圖5 中模板的參數(shù)信息,基本上需要如下3 方面的信息:構(gòu)件的數(shù)量、構(gòu)件發(fā)生故障的概率以及構(gòu)件的物理特性,這些都可以從領(lǐng)域特定語言描述中得到.在環(huán)境模板中,對列車、信號燈、軌道、道岔的實例化個數(shù)進(jìn)行賦值(句式詳見表2);對列車模板中的時鐘變量x的邊界值常量賦值;分別對信號燈模板、軌道模板、道岔模板中的隨機(jī)概率的值m和n進(jìn)行賦值;對聯(lián)鎖表模板中查詢結(jié)果標(biāo)號r1,r2 和r3進(jìn)行賦值等等.對于固定的模板,這些參數(shù)的值輸進(jìn)去以后就直接實例化了;對于組合模板,則需要根據(jù)相應(yīng)的生成算法生成相應(yīng)的實例.例如,RSignalLight 的實例可以在RSignalLight-Single 的基礎(chǔ)上,根據(jù)輸入的信號燈的數(shù)量Nl和算法1 進(jìn)行生成,在一個信號燈的RSignalLight 基礎(chǔ)上增加Nl個綠燈狀態(tài)標(biāo)識符,Nl個紅燈狀態(tài)標(biāo)識符和Nl條消息為“turnGreen[i]?”的遷移,并修改消息為“green!”的遷移判斷函數(shù)isLightgreen(rid),當(dāng)進(jìn)路rid上的信號燈均為綠燈狀態(tài)時返回true,紅燈情況類似.

根據(jù)軌道的數(shù)量Nr修改RTrack 模型,修改方法與修改RSignalLight 的方法類似.

在進(jìn)行控制器的實例化時,圖5 中的控制中心(center)、軌道檢測子模塊(CTrack)、道岔處理子模塊(CPoint)、綠燈控制子模塊(ControlLightGreen)、紅燈控制子模塊(ControlLightRed)、列車調(diào)度器(dispatcher)模板、道岔鎖閉子模型(ControlPointLock)、道岔解鎖子模型(ControlPointUnlock)和列車、信號燈、軌道、道岔的實例化個數(shù)都是有關(guān)系的,可以根據(jù)領(lǐng)域語言給出的列車、信號燈、軌道、道岔的實例化個數(shù)修改控制器子模塊的模板,并進(jìn)行物理特性參數(shù)的賦值.

例如:在軌道控制子模塊CTrack 中增加Nr個狀態(tài)和Nr條消息為“checkoccupied[i]!”的遷移,各遷移上的消息按順序排列.道岔處理子模塊、信號燈處理子模塊和列車調(diào)度器的修改方法類似.

接下來需要定義系統(tǒng)中的交互.系統(tǒng)交互由系統(tǒng)上下文圖中各構(gòu)件之間的通信實現(xiàn),因此定義系統(tǒng)交互即是定義構(gòu)件間通信涉及的所有消息.通信在UPPAAL-SMC 中使用廣播信道,一般在全局聲明中定義所有消息.例如broadcast changreen[Nt*Nl],假設(shè)根據(jù)聯(lián)鎖表可知,共有Nl個信號燈.每輛列車都需要記錄其請求的進(jìn)路的信號燈狀態(tài),因此對于Nt輛列車需定義Nt*Nl個綠燈信號信道.類似可定義其他信道及廣播信道,消息具體聲明見表2.

最后,定義系統(tǒng)模型的聲明及全局變量.在模型聲明中聲明系統(tǒng)中的所有模型.由圖5 可以確定系統(tǒng)是由14個模型組成,其聲明詳見表2.系統(tǒng)所需的全局變量為模型之間的共享信息,應(yīng)該包括軌道占用標(biāo)識符和在全局聲明中每個構(gòu)件的實例化個數(shù).此外,控制中心所需函數(shù)的變量也需在全局聲明中聲明.

Table 2 Partial results generated by the system表2 系統(tǒng)生成部分結(jié)果

6 案例研究

本文以某站的聯(lián)鎖系統(tǒng)為案例,闡述如何按照本文方法根據(jù)具體的情況生成聯(lián)鎖系統(tǒng)的模型,并在此模型基礎(chǔ)上給出了事故的預(yù)測分析,以此證明生成模型的有效性.圖2 為其站場圖,包含7 條軌道段、9 個信號燈、2個道岔和3 條進(jìn)路,每條進(jìn)路包含5 條軌道段、5 個信號燈以及2 個道岔,具體進(jìn)路信息見表1.

6.1 某站的聯(lián)鎖系統(tǒng)描述及其系統(tǒng)模型的生成

根據(jù)站場圖及聯(lián)鎖表分析,請領(lǐng)域?qū)＜姨顚?可以得到領(lǐng)域特定語言的系統(tǒng)描述如下.

將這樣的描述導(dǎo)入,做系統(tǒng)模型生成.系統(tǒng)模型中的系統(tǒng)聲明、全局變量聲明以及交互信道直接帶入表2就可以直接生成,最重要的是環(huán)境模板的實例化和控制器模板的實例化.在環(huán)境模板進(jìn)行實例化時,對于列車模板、軌道設(shè)置模板、信號燈設(shè)置模板、道岔模板這些固定的模板,將參數(shù)的值輸進(jìn)去以后就是直接實例化了.例如列車模板中(圖7),要求初始速度V0、列車允許最大速度Vmax、列車允許最大加速度Amax,軌道長度Smax的參數(shù)值,從領(lǐng)域描述中獲取這些值以后,列車模型就直接實例化了.

Fig.7 SHA template of train in a station圖7 某站聯(lián)鎖系統(tǒng)的列車隨機(jī)混成自動機(jī)模型

對于信號燈查詢模板、軌道查詢模板、聯(lián)鎖表模板這些組合模板,則需要根據(jù)相應(yīng)的生成算法生成相應(yīng)的實例.例如,根據(jù)信號燈個數(shù)和軌道個數(shù)修改RSignalLight 模板和RTrack 模板的遷移數(shù)量和判斷條件.由于有7條軌道段,故有7 個軌道占用標(biāo)識符isTrackoc;有7 條消息為“occu?”和“unoc?”的遷移,在遷移上對相應(yīng)的標(biāo)識符賦值為真.消息“allunoccupied!”的遷移判斷條件為函數(shù)isTrackun(rid).該函數(shù)判斷進(jìn)路rid 上的軌道是否均未被占用,軌道占用遷移情況類似,故RTrack 模型如圖8 所示.其他控制器子模塊的構(gòu)建方法與RTrack 模型的構(gòu)建方法類似,限于篇幅,具體模型見https://github.com/zmy3036190149/SHA.

Fig.8 SHA template of RTrack in a station圖8 某站聯(lián)鎖系統(tǒng)的軌道設(shè)置隨機(jī)混成自動機(jī)模型

得到環(huán)境構(gòu)件模型后,對控制器模板進(jìn)行實例化.根據(jù)構(gòu)件個數(shù)修改子模板,構(gòu)建軌道檢測子模型、綠燈控制子模型、紅燈控制子模型、道岔處理子模型及列車調(diào)度器模型.以軌道檢測子模型為例,由于每個進(jìn)路有5條軌道,故有一條以初始狀態(tài)為始端的遷移,遷移消息為“checkTrack?”,有5 條消息為“checkOccupied!”的遷移,依次相接.最后一條帶“checkOccupied!”消息的遷移發(fā)出后,若收到軌道查詢子模塊發(fā)送的未占用信號“allUnoccupied?”,則向控制中心發(fā)送軌道未占用信號 “trackUnoc!”；若收到軌道占用信號“occupied?”,則向控制中心發(fā)送軌道占用信號“trackOccu!”.由此得到軌道檢測子模型如圖9 所示.其他子模型的構(gòu)建方法與軌道檢測子模型的構(gòu)建方法一致,最后重用控制中心模板,控制中心模板為固定模板,輸入?yún)?shù)后即可實例化,具體模型見https://github.com/zmy3036190149/SHA.

Fig.9 SHA template of CTrack in a station圖9 某站聯(lián)鎖系統(tǒng)的軌道檢測子模塊的隨機(jī)混成自動機(jī)模型

將這些所有的實例化了之后,就可以得到可以在UPPAAL-SMC 上運行的系統(tǒng)模型.由于模型為連續(xù)模型,可以對列車的位置、速度等進(jìn)行仿真,獲得仿真數(shù)據(jù).仿真環(huán)境如下:處理器:Intel(R)Core(TM) i5-4460 CPU@3.20GHz;內(nèi)存:8G;操作系統(tǒng):64 位Windows 10 家庭中文版;UPPAAL 版本:4.1.19.

輸入性質(zhì)驗證表達(dá)式simulate 1[≤500]{Train(0).p,Train(1).p},表示對兩列車的位置變量在500 個時間單位內(nèi)進(jìn)行1 次仿真.經(jīng)過仿真,得到兩列車的位置數(shù)據(jù)結(jié)果.

6.2 基于聯(lián)鎖系統(tǒng)模型的分析:事故預(yù)測

在聯(lián)鎖系統(tǒng)基礎(chǔ)上可以進(jìn)行各種安全分析,本節(jié)研究如何進(jìn)行事故的預(yù)測.由于聯(lián)鎖系統(tǒng)涉及大量變量,對該系統(tǒng)的驗證通常會引發(fā)狀態(tài)空間爆炸問題[28],本文采用基于仿真的方式分析.在分析時,首先要定義事故模型.本文僅考慮軌道交通系統(tǒng)風(fēng)險中的碰撞情況,基本想法是:當(dāng)列車進(jìn)入同一路線后,若列車之間的距離為0m,則兩車相撞.具體描述為:第1 列車駛?cè)肽骋贿M(jìn)路,行駛一段時間后,第2 列車進(jìn)入該進(jìn)路.在該過程中,第1 列車和第2 列車按照各自的速度及加速度行駛.若在某一時刻兩列列車的相對距離為零,則兩列列車發(fā)生碰撞.根據(jù)第3 節(jié)中Train 的定義,每個Train 的路程為p(這個p是離出發(fā)站的距離,不是位移),則兩列列車train1和train2之間的距離為:Distance=train1.p-train2.p.由此,我們定義一個事故模型:

定義1(基于距離的事故模型).假設(shè)有兩列列車train1和train2,兩列車進(jìn)入同一進(jìn)路后列車之間的距離為Distance,其中Distance=train1.p-train2.p.若Distance=0,則兩列車相撞.

基于第6.1 節(jié)中仿真得到的兩列車的位置數(shù)據(jù),可以定義當(dāng)其位置曲線相交時,兩輛列車即存在相撞的情況.圖10 中,train[0]和train[1]的位置曲線相交了,就可預(yù)測出兩列車存在相撞.

為了驗證本文方法生成模型的有效性,本文與文獻(xiàn)[14]中的工作進(jìn)行了對比實驗.文獻(xiàn)[14]中使用的隨機(jī)混成自動機(jī)離散模型,沒有速度、位置等連續(xù)概念.在同上的參數(shù)設(shè)置下,僅修改兩列車進(jìn)入軌道的時間,得到多條預(yù)測結(jié)果,見表3.

由表中可以看出:針對同一案例,盡管本文方法更耗時,在本文的預(yù)測模型預(yù)測出事故的情況下,文獻(xiàn)[14]的預(yù)測模型不一定能預(yù)測出事故;在文獻(xiàn)[14]預(yù)測出事故的情況下,本文的預(yù)測模型均能預(yù)測出事故.相較于文獻(xiàn)[14]中的離散模型,本文生成的混成模型更加精確.其實,第2 節(jié)中提出的框架也適用于文獻(xiàn)[14].

Fig.10 Verification results of expression simulate 1[≤500]{Train(0).p,Train(1).p}圖10 表達(dá)式simulate 1[≤500]{Train(0).p,Train(1).p}的驗證結(jié)果

Table 3 Comparation between Ref.[14] and this paper表3 本文方法與文獻(xiàn)[14]中預(yù)測結(jié)果對比

7 相關(guān)工作

本文研究軌道交通聯(lián)鎖系統(tǒng)的形式化模型的自動生成,相關(guān)的工作主要包括軌道交通系統(tǒng)的形式化建模與驗證.關(guān)于這方面的研究有很多.根據(jù)初步建模使用的語言,我們將這方面的工作分為3 類:基于自然語言的形式化方法、基于半形式化的形式化方法以及基于領(lǐng)域特定語言(DSL)的形式化方法.

在基于自然語言的形式化建模與驗證中,形式化專家根據(jù)領(lǐng)域?qū)＜业淖匀徽Z言描述,直接建立形式化模型,并采用相應(yīng)的形式化驗證工具進(jìn)行性質(zhì)驗證.例如,Hartig 等人[4]在對用自然語言描述的鐵道車輛的安全需求分析之后,使用ACSL 來將其形式化,然后通過FRAMA-C[4]對形式化模型進(jìn)行演繹驗證.Zafar 等人[5]對自然語言描述的移動塊聯(lián)鎖的安全性進(jìn)行了形式化分析,提出了一個使用圖論和Z 符號分析降低系統(tǒng)復(fù)雜性的安全性過程.Russo 等人[6]提出了基于形式化方法的軌道拓?fù)浜土熊囘\行條件驗證工具.并使用Event-B[29]對生成的屬性進(jìn)行形式化、證明和驗證.上述建模與驗證方法對于不具有形式化知識的領(lǐng)域?qū)＜襾碇v很難使用,而本文提出的方法是使用隨機(jī)混成自動機(jī)模板進(jìn)行聯(lián)鎖系統(tǒng)的建模,建立模板后,領(lǐng)域?qū)＜抑灰斎雲(yún)?shù)即可重用模板,相比來說會方便使用很多.

基于半形式化的形式化建模與驗證中,首先由領(lǐng)域?qū)＜沂褂冒胄问交Z言(例如UML)描述聯(lián)鎖系統(tǒng),然后,形式化專家把半形式化模型轉(zhuǎn)換為形式化模型并進(jìn)行形式化分析.例如,Xu 等人[7]將使用UML 等建模語言指定的鐵路聯(lián)鎖模型轉(zhuǎn)換為形式化模型,并進(jìn)行數(shù)學(xué)分析,彌補(bǔ)半形式化語言和形式化語言之間的差距,從而促進(jìn)模型驅(qū)動工程(MDE)方面的安全關(guān)鍵系統(tǒng)的開發(fā).Hansen 等人[8]描述了xUML 子集到流程代數(shù)規(guī)范語言mCRL2 的轉(zhuǎn)換.黃友能等人[9]采用擴(kuò)展后的UML 對ZC 子系統(tǒng)的系統(tǒng)功能進(jìn)行半形式化建模,然后根據(jù)轉(zhuǎn)換規(guī)則將UML 模型轉(zhuǎn)換為線性混成自動機(jī)的形式化模型,使用BACH 軟件進(jìn)行驗證.Fotso 等人[10]使用SysML/KAOS[30]對系統(tǒng)需求、領(lǐng)域特性以及與混合ERTMS/ETCS 3 級標(biāo)準(zhǔn)[31]相關(guān)的安全不變量進(jìn)行半形式化建模,然后自動轉(zhuǎn)換為B 系統(tǒng)規(guī)范,以獲得形式化規(guī)范的體系結(jié)構(gòu),最后用Rodin 工具對其進(jìn)行驗證.楊璐等人[11]采用消息順序圖(message sequence chart,簡稱MSC)[32]對ZC 切換場景功能和受限活性,然后將MSC 模型轉(zhuǎn)換為形式化的時間自動機(jī),通過UPPAA 對其進(jìn)行建模和驗證.這些半形式化的方法,無論是UML 還是SysML,都其實還是軟件專業(yè)建模語言,領(lǐng)域?qū)＜覒?yīng)用起來還是比較吃力.而我們的方法是專門為領(lǐng)域?qū)＜以O(shè)計.

基于DSL 的形式化建模與驗證中,首先由領(lǐng)域?qū)＜沂褂妙I(lǐng)域特定語言描述聯(lián)鎖系統(tǒng),然后,形式化專家再把DSL 模型轉(zhuǎn)換為形式化模型并進(jìn)行形式化分析.這類做的比較好的工作是Idani 等人[12]在2019 年發(fā)表的工作,他們將模型驅(qū)動工程(MDE)范式與形式化方法相結(jié)合,首先使用MDE 工具定義圖形DSL 的一個示例,然后使用形式化B 方法定義其底層操作語義,并確保模型行為相對于其安全屬性的正確性.他們利用Meedus 工具對域模型的執(zhí)行場景進(jìn)行動畫和可視化.從DSL 工具中設(shè)計的給定模型開始,Meedus 要求prob 對B 操作進(jìn)行動畫處理,并通過B 變量估值獲得達(dá)到的狀態(tài).然后,它將這些估值轉(zhuǎn)換回初始DSL,從而自動修改域模型.這種方法允許比當(dāng)前的視覺動畫技術(shù)更務(wù)實的、以領(lǐng)域為中心的動畫,因為最終的DSL 工具允許領(lǐng)域?qū)＜易孕性O(shè)計和驗證各種領(lǐng)域模型,而這些專家不必接受形式化方法的培訓(xùn).Kaymak?? 等人[13]的工作其實也跟這個類似,他們采用時間弧Petri 網(wǎng)的構(gòu)建聯(lián)鎖系統(tǒng)形式化模型的模板,開發(fā)了一個可視化的工具來自動生成聯(lián)鎖系統(tǒng)的形式化TAPN 模型,然后將安全需求描述為CTL 公式,在TAPAAL 上進(jìn)行驗證.這個可視化的工具實際上就是用來給出站場圖,這跟本文的思路其實很相似,只要領(lǐng)域?qū)＜医o出相應(yīng)的參數(shù),形式化模型就構(gòu)建好了.從另一個方面講,也減少了人工建模出錯誤的可能性.我們的方法其實也屬于這一類,與它們相比,我們的方法以隨機(jī)混成自動機(jī)作為形式化手段,既考慮了聯(lián)鎖系統(tǒng)的實時性,又能兼顧故障隨機(jī)性,更加適合作為聯(lián)鎖系統(tǒng)的建模語言.不僅如此,本文還充分利用了聯(lián)鎖系統(tǒng)中構(gòu)件可重用的特點,利用模板進(jìn)行形式化方法的重用.另外,我們之前的工作[14]使用的是隨機(jī)混成自動機(jī)模型,但是文獻(xiàn)[14]中的模型是離散模型,沒有速度、位置等連續(xù)概念.從這個角度來說,本文的模型比文獻(xiàn)[14]中的模型更適合聯(lián)鎖系統(tǒng).

8 總結(jié)與展望

聯(lián)鎖系統(tǒng)的安全使得形式化的建模非常必要.本文提出了基于模板的聯(lián)鎖系統(tǒng)自動生成方法,在分析聯(lián)鎖系統(tǒng)的前提下,定義了領(lǐng)域特定語言,確定了系統(tǒng)的模板以便重用,使得領(lǐng)域?qū)＜铱梢暂斎雲(yún)?shù)就可以生成基于隨機(jī)混成自動機(jī)等的系統(tǒng)模型,并在此基礎(chǔ)上進(jìn)行分析.本文的主要工作包括:

(1) 定義了聯(lián)鎖領(lǐng)域特定語言,針對構(gòu)件數(shù)量、構(gòu)件發(fā)生故障的概率及構(gòu)件的物理特性分別進(jìn)行了設(shè)計;

(2) 確定了聯(lián)鎖領(lǐng)域的模板,包括環(huán)境構(gòu)件模板和控制器模板,對模板進(jìn)行了固定模板和組合模板的分類,根據(jù)分類,制定了模板的隨機(jī)混成自動機(jī)模型;

(3) 定義了基于系統(tǒng)模板的自動生成方法,在環(huán)境構(gòu)件模板和控制器模板的基礎(chǔ)上,通過讓領(lǐng)域?qū)＜逸斎腩I(lǐng)域特定語言確定參數(shù),生成具體的系統(tǒng)隨機(jī)混成自動機(jī)模型,能建模故障隨機(jī)性、行為實時性,其仿真驗證數(shù)據(jù)能用于后續(xù)的安全分析.

在案例研究中,以一個具體車站的聯(lián)鎖系統(tǒng)為例,根據(jù)系統(tǒng)模型自動生成方法生成了具體模型,還基于此模型進(jìn)行了事故預(yù)測分析,與現(xiàn)有方法的事故預(yù)測相比具有好的效果,也驗證了本文方法模型生成的有效性.

本文工作尚有不足之處:文中的模板只考慮了列車行駛故障、信號燈故障、道岔故障、軌道故障等硬件故障,還未考慮聯(lián)鎖系統(tǒng)中軟件故障以及更多的復(fù)雜的現(xiàn)實因素.未來工作中,將在模板中注入這些故障,讓故障出現(xiàn)的時機(jī)等更接近現(xiàn)實,使得生成的形式化模型更真實,能驗證出更多的現(xiàn)實錯誤.另外,還需要設(shè)計算法能快速地在仿真驗證中發(fā)現(xiàn)錯誤.