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

張 重，劉曉娟，李國(guó)瑞

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

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

張 重，劉曉娟，李國(guó)瑞

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

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

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

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

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

1 SCADE簡(jiǎn)介

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

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

1.1 SCADE軟件建模方法

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

1.2 基于SCADE的圖形化建模

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

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

數(shù)據(jù)流圖能夠很好地對(duì)連續(xù)控制系統(tǒng)進(jìn)行建模、數(shù)據(jù)采集、信號(hào)處理、計(jì)算等相關(guān)工作，數(shù)據(jù)流圖的功能節(jié)點(diǎn)即為軟件的功能單元，能夠構(gòu)建多層次的功能節(jié)點(diǎn)來(lái)表示復(fù)雜的功能單元，數(shù)據(jù)流圖所采用的算符有算術(shù)算符、時(shí)序算符、邏輯算符等，這些算符在SCADE中都是以直觀的圖形化方式表現(xiàn)出來(lái)，用圖形化的方法構(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ī)也是用圖形化符號(hào)表示，其構(gòu)建的模型的變化控制邏輯是用一系列的狀態(tài)符號(hào)、轉(zhuǎn)移和信號(hào)來(lái)表示。用從一個(gè)狀態(tài)到另一個(gè)狀態(tài)的轉(zhuǎn)移來(lái)表示系統(tǒng)的進(jìn)展，用信號(hào)來(lái)觸發(fā)狀態(tài)的轉(zhuǎn)移。

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

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

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

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

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

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

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

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

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

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

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

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

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

3 基于SCADE的CBI模型的形式化驗(yàn)證

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

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

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

4 代碼的自動(dòng)生成與分析

4.1 代碼自動(dòng)生成與集成

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

4.2 代碼測(cè)試與分析

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

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

5 結(jié)束語(yǔ)

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

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

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

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

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

[5] 顏雯清. SCADE平臺(tái)下 C代碼的自動(dòng)生成[J].計(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

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