軌道交通聯(lián)鎖領域特定語言的形式化*

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

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

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

為了保證這樣的安全性,目前很多歐洲鐵路控制與防護標準,如EN50128[2],EN50129[3]等強烈推薦在開發(fā)之前,使用形式化方法進行建模和分析.形式化方法以嚴密的數學理論和相關推理為基礎,有嚴格的語法規(guī)范和確定的語義定義,并且是自證正確的,因此非常適用于開發(fā)聯(lián)鎖系統(tǒng)這樣安全攸關的系統(tǒng).但是,形式化方法又有著固有的學習成本高、不易使用的缺點.一般來說,領域專家的形式化建模離不開形式化專家的幫助,建模的主體依然是形式化的專家.在聯(lián)鎖系統(tǒng)這類領域知識特別復雜的系統(tǒng)中,領域專家需要快速構建模型并分析復雜業(yè)務邏輯,根據分析結果快速進行錯誤定位與錯誤修正,建模與分析的主體應該是領域專家.如何讓領域專家能自主構建形式化模型,是一個需要解決的問題.

現(xiàn)有的軌道交通領域的形式化建模工作主要分為3 類:基于自然語言的形式化方法、基于半形式化的方法和基于領域特定語言(DSL)的方法.基于自然語言的形式化建模[4-6]都是形式化專家根據領域專家的自然語言描述直接建立形式化模型,并采用相應的形式化驗證工具進行性質驗證,這類方法需要領域專家和形式化專家的緊密合作,對于不具有形式化知識的領域專家來講很難使用.基于半形式化的形式化建模與驗證中[7-11],先由領域專家使用半形式化語言(例如UML)描述系統(tǒng),然后形式化專家再把半形式化模型轉換為形式化模型并進行形式化分析.但這些半形式化語言都是軟件專業(yè)建模語言,不是領域專家所擅長的語言.基于領域特定語言的形式化建模與驗證中[12-15],首先由領域專家使用領域特定語言描述系統(tǒng),然后形式化專家再把領域特定語言模型轉換為形式化模型并進行形式化分析.例如,Idani 等人[12]將圖形領域定制語言的模型轉換為形式化B 模型.這類方法允許領域專家只要根據領域特定語言給出領域模型,就可以享受形式化方法帶來的好處,便于形式化專家和領域專家的合作,也減少了人工建模出錯誤的可能性.

基于以上分析,我們認為,基于領域特定語言的建模方法更方便領域專家使用.但現(xiàn)有的基于特定語言的方法并不能直接應用于聯(lián)鎖系統(tǒng),原因如下:

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

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

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

本文首先由領域專家對聯(lián)鎖系統(tǒng)模型進行分析,根據不同案例設計其領域特定語言;其次,由領域專家確定聯(lián)鎖系統(tǒng)模型的模板組成,并由形式化專家抽取系統(tǒng)模型的模板,舉例構建其隨機混成自動機模板;然后,由領域專家通過領域特定語言輸入參數自動生成系統(tǒng)模型.本文以某站聯(lián)鎖系統(tǒng)為例,自動構建了其系統(tǒng)的混成自動機模型,并在驗證平臺UPPAAL-SMC 上進行事故預測分析,證明了本文方法的可行性和有效性.

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

1 預備知識

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

通過廣播信道和共享變量,不同的隨機混成自動機之間相互通信,組成隨機混成自動機網絡(network of stochastic hybrid automata,簡稱NSHA).圖1 展示了一個由隨機混成自動機A和B組成的隨機混成自動機網絡.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 中,標志1 表示A在狀態(tài)A1 處的延遲遵循λ=1 的指數分布.在狀態(tài)A2 中,x≤1為不變式,在該狀態(tài),時鐘x始終滿足該不變式.實線箭頭表示狀態(tài)之間的轉換,在遷移上有“guard”,“update”和“sync”,分別表示遷移條件、變量更新和同步.在狀態(tài)A2 到A4 的遷移上,“guard”為x≥1,表示當x≥1 時遷移才會發(fā)生,“update”為x:=0,表示更新x的值為0.

Fig.1 An example of NSHA圖1 隨機混成自動機網絡樣例

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

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

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

2 方法框架

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

從上述流程中可知:聯(lián)鎖系統(tǒng)的運行不僅僅只涉及控制器,還涉及列車、軌道、道岔、信號燈和聯(lián)鎖表.其中,列車包含其車載系統(tǒng),軌道分為多個區(qū)段,每個區(qū)段與一個軌道電路相關聯(lián),用以檢測軌道是否被列車占用.道岔是軌道的連接處,根據道岔的不同位置,列車可以駛入不同的進路.道岔可以處于解鎖與鎖閉兩種狀態(tài),且若其處于解鎖狀態(tài),則表明該道岔未與岔口相連.當道岔處于鎖閉狀態(tài)時,列車才能通過該道岔.信號燈位于不同的軌道區(qū)段之間,其狀態(tài)為紅燈或者綠燈,表明列車應該停止或允許前進.進路由聯(lián)鎖表定義,一般在鐵路站場設計時被創(chuàng)建,每個進路由按拓撲結構順序連接的軌道段組成,只有在進路建立后,列車才能獲準進入該進路.所有的這些一般都可以從一個站場圖中獲得,例如從圖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ū)別在于車站站場圖不同導致的實例個數不同.從中也不難發(fā)現(xiàn),雖然構件數量不同,但構件類型是固定的,也就是說,每個聯(lián)鎖系統(tǒng)都會涉及控制器、列車、軌道、道岔、信號燈和聯(lián)鎖表.我們可以將每種類型的構件抽取出來做成模板,進行形式化建模.在模板的形式化建模中,適用的語言要可以應對設備故障的隨機性以及較高的實時性要求,可以采用隨機混成自動機和價格時間自動機進行建模.

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

· 首先,由領域專家根據領域特定語言提供模型參數列表;

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

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

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

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

根據上述分析,聯(lián)鎖系統(tǒng)的模型首先在構件的數量上是不同的,也就是說,列車、道岔、信號燈和軌道實例化的個數隨案例變化.這些構件的數量要成為語言的一部分.不僅如此,由于這些實體數量的變化,導致其進路表是不同的.假設圖2 這樣的站場中包含3 條進路,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 向下打開.其進路表見表1.

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

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

以表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)表示進入軌道T3 需要信號燈S3 為綠燈狀態(tài),道岔SW1 的方向向上.

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

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

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

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

4.1 模板的基本組成

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

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

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

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

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

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

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

4.2 模板抽取舉例

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

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

4.2.1 固定模板

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

下面選取信號燈設置模型SSignalLight 的模板抽取作為例子進行說明.

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

增加時間約束時,從領域知識中可獲知SSignalLight 的時間約束,即信號燈狀態(tài)變化有延遲.根據時間約束定義時鐘變量,定義局部時鐘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”.類似在時間自動機中定義時鐘變量b,由此得到SSignalLight 的隨機混成自動機如圖6(a)所示.

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

4.2.2 組合模板

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

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

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

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

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

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

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

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

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

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

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

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

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

6 案例研究

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

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

根據站場圖及聯(lián)鎖表分析,請領域專家填寫,可以得到領域特定語言的系統(tǒng)描述如下.

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

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

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

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

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

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

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

輸入性質驗證表達式simulate 1[≤500]{Train(0).p,Train(1).p},表示對兩列車的位置變量在500 個時間單位內進行1 次仿真.經過仿真,得到兩列車的位置數據結果.

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

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

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

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

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

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

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

Table 3 Comparation between Ref.[14] and this paper表3 本文方法與文獻[14]中預測結果對比

7 相關工作

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

在基于自然語言的形式化建模與驗證中,形式化專家根據領域專家的自然語言描述,直接建立形式化模型,并采用相應的形式化驗證工具進行性質驗證.例如,Hartig 等人[4]在對用自然語言描述的鐵道車輛的安全需求分析之后,使用ACSL 來將其形式化,然后通過FRAMA-C[4]對形式化模型進行演繹驗證.Zafar 等人[5]對自然語言描述的移動塊聯(lián)鎖的安全性進行了形式化分析,提出了一個使用圖論和Z 符號分析降低系統(tǒng)復雜性的安全性過程.Russo 等人[6]提出了基于形式化方法的軌道拓撲和列車運行條件驗證工具.并使用Event-B[29]對生成的屬性進行形式化、證明和驗證.上述建模與驗證方法對于不具有形式化知識的領域專家來講很難使用,而本文提出的方法是使用隨機混成自動機模板進行聯(lián)鎖系統(tǒng)的建模,建立模板后,領域專家只要輸入參數即可重用模板,相比來說會方便使用很多.

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

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

8 總結與展望

聯(lián)鎖系統(tǒng)的安全使得形式化的建模非常必要.本文提出了基于模板的聯(lián)鎖系統(tǒng)自動生成方法,在分析聯(lián)鎖系統(tǒng)的前提下,定義了領域特定語言,確定了系統(tǒng)的模板以便重用,使得領域專家可以輸入參數就可以生成基于隨機混成自動機等的系統(tǒng)模型,并在此基礎上進行分析.本文的主要工作包括:

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

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

(3) 定義了基于系統(tǒng)模板的自動生成方法,在環(huán)境構件模板和控制器模板的基礎上,通過讓領域專家輸入領域特定語言確定參數,生成具體的系統(tǒng)隨機混成自動機模型,能建模故障隨機性、行為實時性,其仿真驗證數據能用于后續(xù)的安全分析.

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

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