基于SCADE的城軌聯鎖軟件開發方法的研究

張 重，劉曉娟，李國瑞

（ 蘭州交通大學 電子與信息工程學院，蘭州 730070 ）

基于SCADE的城軌聯鎖軟件開發方法的研究

張 重，劉曉娟，李國瑞

（ 蘭州交通大學 電子與信息工程學院，蘭州 730070 ）

CBTC的計算機聯鎖（CBI）系統是一個復雜且安全性要求非常高的系統，若按照傳統的方法進行開發，很難達到其所需要的安全性和可靠性。本文提出基于高安全性應用程序開發環境（SCADE）開發城軌聯鎖系統軟件的方法，能有效解決上述問題。文章主要介紹基于SCADE開發CBI軟件的流程，建模方法，形式化驗證和代碼自動生成的方法。

城軌聯鎖；SCADE；形式化方法；建模

CBTC系統即基于通信的列車控制系統，主要包括車載列車自動防護（ATP）系統、區域控制器（ZC）、列車自動運行（ATO）系統、列車自動監控（ATS）系統和計算機聯鎖（CBI）系統。CBI比較復雜，安全要求為SIL4級，為達到所要求的安全級別，采用安全軟件開發方法是必要的[1]。本文提出利

用基于模型驅動安全軟件開發環境（SCADE）開發CBI軟件的方法，如圖1所示。使用這種方法既能保證所開發系統的安全性，又能降低開發的難度。

1 SCADE簡介

高安全性應用程序開發環境（SCADE，Safety Critical Application Development Environment)是一種基于模型驅動的軟件開發環境，具有嚴格的數學理論基礎。軟件開發的整個流程都可以在SCADE中進行。SCADE可以自動生成直接面向工程的標準C代碼，從而提高了軟件開發的效率。目前，SCADE在國外已廣泛應用于安全需求非常高的領域，如航空、核電、交通控制等[2]。

圖1 基于SCADE的軟件開發流程

1.1 SCADE軟件建模方法

在SCADE中，通過直觀的圖形符號進行建模,參與構建的圖形符號都可以準確地轉換為LUSTRE 語言。LUSTRE 語言是一種形式化語言，能夠確保所建模型的精確性和無二義性。在開發軟件時，只需掌握SCADE基本的圖形符號即可，并不需掌握LUSTRE 語言，這樣能有效降低開發的復雜度。在構建模型的過程中，既可以用圖形符號構建，構建完成后其自動轉換為LUSTRE語言，也可以用LUSTRE語言直接構建。

1.2 基于SCADE的圖形化建模

SCADE 提供2種方法進行圖形化建模：數據流圖和安全狀態機。

1.2.1 數據流圖

數據流圖能夠很好地對連續控制系統進行建模、數據采集、信號處理、計算等相關工作，數據流圖的功能節點即為軟件的功能單元，能夠構建多層次的功能節點來表示復雜的功能單元，數據流圖所采用的算符有算術算符、時序算符、邏輯算符等，這些算符在SCADE中都是以直觀的圖形化方式表現出來，用圖形化的方法構建軟件模型具有直觀、易于掌握等優點。

1.2.2 安全狀態機

在SCADE中描述離散狀態控制系統一般采用安全狀態機，安全狀態機主要用于描述外部中斷處理和內部事物的處理，安全狀態機也是用圖形化符號表示，其構建的模型的變化控制邏輯是用一系列的狀態符號、轉移和信號來表示。用從一個狀態到另一個狀態的轉移來表示系統的進展，用信號來觸發狀態的轉移。

2 基于SCADE的CBI系統的建模

CBI系統主要作用是通過技術方法使信號、道岔和進路按照一定的程序和滿足一定的條件才能動作或建立起來，從而使列車能安全高效地運行。根據CBI系統的功能需求將其分為幾個功能子模塊[3]，并根據它們之間的關系設計出功能模塊的組成結構。

2.1 CBI系統功能模塊

CBI系統功能模塊如表1。

2.2 CBI系統結構設計

CBI主要任務是通過現場設備和CBTC其他子系統提供的信息，控制現場設備，并且將安全信息傳送給CBTC其他子系統[4]。CBI通過以下流程完成其功能：

表1 CBI系統功能模塊

（1）CBI接收來至ATS發送來的進路命令信息。（2）根據ZC傳來的相關軌道空閑信息以及相關道岔信息，由進路控制模塊進行聯鎖邏輯判斷后進行相應處理，并由道岔控制模塊對相關道岔進行控制。（3）根據進路控制單元判定好的信息傳送給信號控制模塊，信號控制模塊將信息進行有效處理后向ZC發送行車許可。根據上述描述建立CBI系統的結構圖，如圖2所示。

圖2 CBI系統結構圖

2.3 基于SCADE的CBI系統總體模型

根據上述對功能節點的劃分，在SCADE的建模工具中定義對應的功能節點。按照圖2所示的系統結構，在SCADE環境中建立CBI系統的總體模型，如圖3所示。

圖3 基于SCADE的CBI系統總體功能模型

即用SCADE數據流圖的功能節點將CBI的各功能模塊刻畫出來。各個功能節點對應CBI各功能模塊。系統輸入為I-ATS和I-ZC,系統輸出為O-ZC。進路命令處理（Command Processing）模塊接收ATS出來的進路命令信息，經過此功能模塊處理，將相應的進路信息發送給進路控制（Route Control）模塊。軌道空閑處理(TVP)功能模塊接收I- ZC信息，并做相應處理傳送給進路控制模塊。進路控制模塊接收進路處理模塊、軌道空閑檢查模塊、信號控制（Signal Control）模塊、道岔控制（Switch control）模塊相應信息，處理后將信息輸出給道岔控制模塊和信號控制模塊。信號控制模塊接收進路控制模塊信息，做相應處理后將信息輸出給信號控制模塊。

3 基于SCADE的CBI模型的形式化驗證

在SCADE中可以對所建模型進行形式驗證，從而保證模型的正確性，它內置了ProverSL作為形式化驗證引擎，對所建模型進行形式驗證時，設計一個符合安全需求的特性觀察器，對模型進行形式驗證，如果驗證結果表明模型符合安全需求，系統會自動給出一個安全證明，如果驗證結果表明不符合安全需求，系統回給出一個反例，幫助進一步修正。這就能夠保證軟件的安全性并且提高驗證的自動化程度?；赟CADE的形式驗證大體分為4步，結合上述所建CBI模型的實例對其流程進行說明，如圖4所示。

圖4 CBI系統形式化驗證的SCADE實現

（1）提取所建模型的安全需求，并進行規范。（2）用數據流圖將提取出的CBI安全需求進行描述。（3）創建一個模型將CBI系統的安全性需求描述和軟件需求描述結合到一起。（4）用形式化驗證引擎對上述結合在一起的模型進行驗證，如果模型安全，系統會給一個安全證明，如果模型不安全，會給出一個反例。

4 代碼的自動生成與分析

4.1 代碼自動生成與集成

SCADE能夠自動生成面向工程的C代碼，SCADE代碼生成器滿足DO-178B航空A級標準。所生成的代碼集成方式為工程人員自定義一個結構體來調度自動生成功能函數塊的接口，功能函數塊為結構體的成員，編寫基層支持軟件并添加主函數，在主程序中調用主函數，并將所有代碼在VC++6.0環境下編譯集成。

4.2 代碼測試與分析

本文應用clock函數測量手寫代碼和自動生成代碼的執行時間。通過測試表明，自動生成的代碼執行效率高于手寫代碼, 如表2所示。

表2 執行時間的比較

5 結束語

研究表明，SCADE圖形化建模直觀、易于掌握、利于軟件開發和后期維護。SCADE可以對其所建模型進行形式驗證，保證軟件開發的安全性。SCADE可自動生成直接面向工程的高安全的C代碼，使用SCADE開發城軌聯鎖軟件不僅能提高軟件的開發效率，而且能有效保證其安全性，是開發城軌軟件比較好的方法。

[1] CENELEC.EN50129: Railway Application-Communication, Signalling, Processing Systems-Safey Related Electronic System for Signailing[S]. 2003.

[2] 張合軍.基于SCADE的無人機飛行控制系統軟件設計[D].南京：南京航空航天學，2007.

[3] 劉曉娟，張雁鵬，湯自安. 城市軌道交通智能控制系統[M].北京：中國鐵道出版社，2010.

[4] 王 鯤，龍廣錢，王 俊，等.關于城市軌道交通CBTC計算機聯鎖子系統的研究[J].現代城市軌道交通，2012（4）：1-3.

[5] 顏雯清. SCADE平臺下 C代碼的自動生成[J].計算機仿真，2009（10）：24-28.

責任編輯 楊利明

Research on method of software development based on SCADE for Urban Transit interlocking

ZHANG Zhong, LIU Xiaojuan, LI Guorui
（School of Electronocs and Information Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China）

Computer based Interlocking(CBI) was a complex system, also a safety critical system. It was diff i cult to reach the safety and reliability of software needs by the traditional software development process. This paper proposed a method of software development based on Safety-Critical Application Development Environment (SCADE) for Urban Transit interlocking which could effectively solve the above problems. This paper mainly introduced the process of CBI software development based on SCADE, the modeling method，the method of formal verif i cation and code automatically generated.

Urban Transit interlocking; SCADE; formal methods; modeling

U231.7∶TP39

A

1005-8451（2014）02-0014-03

2013-08-25

張 重，在讀碩士研究生；劉曉娟，教授。