張 重，劉曉娟，李國瑞

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

基于SCADE的城軌聯(lián)鎖軟件開發(fā)方法的研究

張 重，劉曉娟，李國瑞

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

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

城軌聯(lián)鎖；SCADE；形式化方法；建模

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

用基于模型驅(qū)動安全軟件開發(fā)環(huán)境（SCADE）開發(fā)CBI軟件的方法，如圖1所示。使用這種方法既能保證所開發(fā)系統(tǒng)的安全性，又能降低開發(fā)的難度。

1 SCADE簡介

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

圖1 基于SCADE的軟件開發(fā)流程

1.1 SCADE軟件建模方法

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

1.2 基于SCADE的圖形化建模

SCADE 提供2種方法進(jìn)行圖形化建模：數(shù)據(jù)流圖和安全狀態(tài)機(jī)。

1.2.1 數(shù)據(jù)流圖

數(shù)據(jù)流圖能夠很好地對連續(xù)控制系統(tǒng)進(jìn)行建模、數(shù)據(jù)采集、信號處理、計算等相關(guān)工作，數(shù)據(jù)流圖的功能節(jié)點(diǎn)即為軟件的功能單元，能夠構(gòu)建多層次的功能節(jié)點(diǎn)來表示復(fù)雜的功能單元，數(shù)據(jù)流圖所采用的算符有算術(shù)算符、時序算符、邏輯算符等，這些算符在SCADE中都是以直觀的圖形化方式表現(xiàn)出來，用圖形化的方法構(gòu)建軟件模型具有直觀、易于掌握等優(yōu)點(diǎn)。

1.2.2 安全狀態(tài)機(jī)

在SCADE中描述離散狀態(tài)控制系統(tǒng)一般采用安全狀態(tài)機(jī)，安全狀態(tài)機(jī)主要用于描述外部中斷處理和內(nèi)部事物的處理，安全狀態(tài)機(jī)也是用圖形化符號表示，其構(gòu)建的模型的變化控制邏輯是用一系列的狀態(tài)符號、轉(zhuǎn)移和信號來表示。用從一個狀態(tài)到另一個狀態(tài)的轉(zhuǎn)移來表示系統(tǒng)的進(jìn)展，用信號來觸發(fā)狀態(tài)的轉(zhuǎn)移。

2 基于SCADE的CBI系統(tǒng)的建模

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

2.1 CBI系統(tǒng)功能模塊

CBI系統(tǒng)功能模塊如表1。

2.2 CBI系統(tǒng)結(jié)構(gòu)設(shè)計

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

表1 CBI系統(tǒng)功能模塊

（1）CBI接收來至ATS發(fā)送來的進(jìn)路命令信息。（2）根據(jù)ZC傳來的相關(guān)軌道空閑信息以及相關(guān)道岔信息，由進(jìn)路控制模塊進(jìn)行聯(lián)鎖邏輯判斷后進(jìn)行相應(yīng)處理，并由道岔控制模塊對相關(guān)道岔進(jìn)行控制。（3）根據(jù)進(jìn)路控制單元判定好的信息傳送給信號控制模塊，信號控制模塊將信息進(jìn)行有效處理后向ZC發(fā)送行車許可。根據(jù)上述描述建立CBI系統(tǒng)的結(jié)構(gòu)圖，如圖2所示。

圖2 CBI系統(tǒng)結(jié)構(gòu)圖

2.3 基于SCADE的CBI系統(tǒng)總體模型

根據(jù)上述對功能節(jié)點(diǎn)的劃分，在SCADE的建模工具中定義對應(yīng)的功能節(jié)點(diǎn)。按照圖2所示的系統(tǒng)結(jié)構(gòu)，在SCADE環(huán)境中建立CBI系統(tǒng)的總體模型，如圖3所示。

圖3 基于SCADE的CBI系統(tǒng)總體功能模型

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

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

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

圖4 CBI系統(tǒng)形式化驗證的SCADE實(shí)現(xiàn)

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

4 代碼的自動生成與分析

4.1 代碼自動生成與集成

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

4.2 代碼測試與分析

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

表2 執(zhí)行時間的比較

5 結(jié)束語

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

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

[2] 張合軍.基于SCADE的無人機(jī)飛行控制系統(tǒng)軟件設(shè)計[D].南京：南京航空航天學(xué)，2007.

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

[4] 王 鯤，龍廣錢，王 俊，等.關(guān)于城市軌道交通CBTC計算機(jī)聯(lián)鎖子系統(tǒng)的研究[J].現(xiàn)代城市軌道交通，2012（4）：1-3.

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

責(zé)任編輯 楊利明

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

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