張 恬
(中鐵第一勘察設計院集團有限公司,西安 710043)
計算機聯鎖(CBI,Computer Based Interlocking)系統通過技術手段建立信號機、軌道電路以及進路上道岔之間的相互制約關系[1]。隨著鐵路信號工程的集成化發展,CBI 系統接入和控制的設備種類不斷增加。目前,城市軌道交通的CBI 系統增加了屏蔽門、防淹門、車庫門等設備與接口,高速鐵路的CBI 系統增加了與列控中心(TCC)的接口[2],以及與相鄰車站CBI 系統[3]等的信息交互接口。不斷擴展的功能要求使得CBI 系統軟件復雜度日益增加,給CBI系統的軟件開發和維護帶來很大的壓力。
CBI 系統應工作可靠,符合故障-安全原則,滿足GB/T 28809-2012 規定的SIL4 安全等級要求[4];其安全性除了依靠采用冗余結構的系統硬件,還應注重其軟件的安全性[5]。
高安全性應用程序開發環境(SCADE,Safety Critical Application Development Environment)是由法國研制的一個高安全性應用程序開發環境,提供了一套由模型驅動的軟件開發工具包。目前,SCADE被廣泛應用于高安全性需求的應用領域,例如航空、軌道交通、核電等。近年來,SCADE 開始應用于國內鐵路行業信息系統開發。文獻[6] 對基于SCADE的安全軟件開發方法展開研究,文獻[7] 研究并實現了基于SCADE 的聯鎖列控一體化系統,文獻[8] 提出采用SCADE 實現閉塞分區邏輯功能的建模。
本文基于SCADE 的軟件開發流程,依據CBI 系統的軟件需求規約,研究利用SCADE 進行CBI 系統軟件的開發。
SCADE 是一種由模型驅動的軟件開發方法,軟件開發過程圍繞形式化模型展開。為保證模型滿足功能需求,在各個開發階段可對所建立的模型進行仿真和驗證,避免功能實現出現偏離。
基于SCADE 的軟件開發流程見圖1 所示。

圖1 基于SCADE 的軟件開發流程
SCADE 提供了一組支持工具,覆蓋從軟件需求分析到代碼實現、驗證測試全過程的軟件開發工作,方便開發人員驗證模型實現的正確性。其中,SCADE Architect 為系統建模與驗證工具,SCADE Suite 為基于模型的控制軟件建模、仿真、驗證和自動代碼生成工具,SCADE Test 為模型級自動化測試工具,SCADE Simulation MTC 為模型覆蓋率測試和分析工具。SCADE 可根據經過驗證的模型自動生成代碼,支持自動化單元測試。因此,在SCADE 環境下,軟件開發的核心工作是軟件需求規約和設計,軟件開發人員采用直觀的、易于理解的圖形化方式完成需求建模和軟件設計;此外,集成測試和系統測試是通過基于軟件結構的覆蓋率分析和嚴格的形式化驗證實現,可保證軟件實現的正確性。
CBI 系統的主要任務是監視和控制進路上相關設備按照一定約束和程序動作,進而自動完成進路控制。信號機、道岔、軌道電路是主要室外設備,室內設備主要包括人機交互層、聯鎖控制層及I/O 接口層[9]。CBI 通過車站室外現場設備、TCC 及調度集中(CTC)等其它子系統提供的信息進行邏輯運算,再向車站室外控制設備輸出控制指令,并將安全信息傳送給TCC 等其它子系統。CBI 系統軟件基礎功能描述見表1。

表1 CBI 系統軟件基礎功能
CBI 系統分為邏輯運算層、平臺層、子系統接口層,聯鎖軟件的開發主要是實現邏輯運算層。
對于具體的CBI 車站,車站配置的其它信號設備或有不同,如CTC、TCC、信號集中監測(CSM)系統等。為此,除了實現通用基礎功能的處理邏輯,還需定義其具體的外部系統接口邏輯,形成適用于本站工程環境的CBI 邏輯。CBI 系統的基本結構如圖2 所示。

圖2 CBI 系統基本結構示意
CBI 系統由室外現場設備的輸入驅動,且需要與CTC、TCC 進行實時通信,是一種典型的面向數據流和變化傳播的反應式系統。對于這樣的系統,系統建模不僅需要考慮系統各個狀態間的轉換關系,還需考慮在同一步驟中狀態與環境之間復雜的約束關系,CBI 系統的總體功能模型如圖3 所示。

圖3 CBI 系統總體功能模型
總體功能采用層次化結構設計,按照基礎功能可劃分為進路控制模塊、信號控制模塊、道岔控制模塊,各個子功能模塊間相互獨立。邏輯處理模塊通過對子功能模塊接口函數的調用來完成各模塊的輸入、輸出和邏輯處理,實現聯鎖基礎邏輯功能。
SCADE 提供數據流圖和安全狀態機2 種圖形化建模方法[9-10]。其中,數據流圖是一種基于LUSTRE語言的建模語言,以圖形化方式展現數據在系統中的流動和處理過程,主要用于連續性系統的建模。安全狀態機是一種基于同步假設的可視化建模語言,能直觀的描述系統控制流和邏輯判定功能,主要用于離散系統的建模。
以進路鎖閉模塊為例,在SCADE 中建立其對應的數據流圖模型,包括“鎖閉檢查”和“鎖閉執行”2 部分。其中,進路鎖閉檢查數據流見圖4。

圖4 進路鎖閉檢查數據流
在鎖閉條件檢查階段,重復檢查進路上各個控制對象的狀態,要求軌道電路區段處于空閑狀態、所有道岔位置正確、本咽喉區沒有建立敵對進路,且另一咽喉區也沒有建立迎面敵對進路。在圖4 中,輸入的現場道岔、敵對信號、道岔及照查數據,分別 由CheckSecZy、Check Opp Signal Open、Check Switch Position 完成邏輯運算后,輸出結果Lock Con;若Lock Con=ture,表示滿足進路鎖閉條件;反之,表示進路鎖閉條件不滿足。
鎖閉執行功能的狀態圖如圖5 所示,包含初始狀態(init)、進路鎖閉成功(RouteLockSucc)、進路鎖閉失敗(RouteLockfail)3 個狀態。

圖5 進路鎖閉執行功能的狀態
當進路鎖閉條件滿足,轉移到RouteLockSucc 狀態,同時將進路標志設置為信號開放(opening),并將信號機、道岔、區段鎖閉到規定位置,發送進路鎖閉成功命令(LockSuccess);當進路鎖閉條件不滿足(LockCon==false),則轉移到RouteLockfail狀態,發送進路鎖閉失敗命令。
SCADE Simulation MTC 可檢查和分析狀態圖和數據流圖模型具體實現的需求以及未覆蓋的需求。以聯鎖邏輯模型中的任意節點為例,對該節點進行MTC 覆蓋率分析。當節點插裝完畢后,運行一個周期,得到該節點初始測試用例結果的MTC 覆蓋率分析情況。按照MC/DC 覆蓋準則,需增加7 個輸入條件分別有且僅有一個為假的情況,依據提示信息增加或修改測試案例,最終使得覆蓋率達到100%。測試結果如圖6 所示。

圖6 SCADE Suite 測試結果
SCADE Suite 中KCG 工具能夠自動生成聯鎖系統工程的C 語言代碼,如圖7 所示。C 語言代碼覆蓋系統模型的所有輸入、輸出和功能邏輯,保證模型與代碼的一致性。

圖7 SCADE Suite 中KCG 工具自動生成的C 語言代碼文件
傳統的CBI 軟件開發方法中,需求規約、概要設計與詳細設計多為自然語言描述,易出現定義模糊和二義性問題,且軟件開發以耗時費力的代碼編寫和測試為主,代碼的準確性和可讀性難以保證,加重后期維護的難度。此外,單元測試和集成測試需要借助第三方驗證工具和編寫大量測試用例,工作量大,存在驗證不充分的問題。
SCADE 提供的開發工具涵蓋需求管理、模型建立、模型驗證、代碼生成、驗證測試全過程,開發過程清晰、直觀、連貫;利用SCADE 開發軟件,開發工作的重點集中在前期階段,且確認工作與開發過程能夠同步進行,支持V 模型軟件快速開發模式,幫助開發人員有效管控軟件開發風險;SCADE 代碼生成器可快速產生面向工程的C 語言代碼,自動生成的代碼規范、可讀性好,且可追溯。
經過初步測試驗證,利用SCADE 工具開發的CBI 系統軟件功能符合預期,可大幅縮短開發時間。