SCADE在城市軌道交通ATP軟件建模中的應(yīng)用

白 銳，康隨武

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

SCADE在城市軌道交通ATP軟件建模中的應(yīng)用

白 銳，康隨武

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

列車(chē)自動(dòng)防護(hù)（ATP）系統(tǒng)是基于通信列車(chē)控制 (CBTC) 系統(tǒng)的重要組成部分。車(chē)載ATP在列車(chē)運(yùn)行過(guò)程中擔(dān)負(fù)列車(chē)安全運(yùn)行的重要任務(wù)，是與安全直接相關(guān)的系統(tǒng)，需要高的安全性和可靠性。為了滿(mǎn)足車(chē)載ATP軟件對(duì)安全的需求，提出了基于模型的軟件開(kāi)發(fā)方法對(duì)ATP進(jìn)行建模。應(yīng)用SCADE作為開(kāi)發(fā)工具，建立了ATP系統(tǒng)部分功能的模型，說(shuō)明了SCADE在ATP軟件建模上的可行性。

列車(chē)自動(dòng)防護(hù)；安全相關(guān)；SCADE

列車(chē)自動(dòng)防護(hù)（ATP）系統(tǒng)是CBTC系統(tǒng)的子系統(tǒng)，它負(fù)責(zé)列車(chē)的安全運(yùn)行，并在緊急情況下采取措施來(lái)保證乘客的安全。ATP子系統(tǒng)連續(xù)檢測(cè)列車(chē)的位置，計(jì)算列車(chē)運(yùn)行的速度曲線(xiàn)和速度限制，提供給列車(chē)移動(dòng)授權(quán)，保證前后車(chē)的安全間距及超速防護(hù)，控制車(chē)門(mén)和站臺(tái)屏蔽門(mén)的開(kāi)關(guān)，確保旅客的上下車(chē)安全[1]。

SCADE[2]（Safety-Critical Application Development Environment）是高安全性應(yīng)用開(kāi)發(fā)環(huán)境，覆蓋了嵌入式開(kāi)發(fā)的整個(gè)流程，是一個(gè)以軟件模型設(shè)計(jì)為中心而非傳統(tǒng)的以程序代碼為中心的軟件開(kāi)發(fā)工具?；赟CADE的軟件開(kāi)發(fā)流程從需求出發(fā)，用圖形化建模的方式來(lái)實(shí)現(xiàn)概要設(shè)計(jì)和詳細(xì)設(shè)計(jì)，采用基于模型構(gòu)造系統(tǒng)的設(shè)計(jì)方法。利用SCADE提供的開(kāi)發(fā)工具，可以從模型自動(dòng)生成代碼，且不必對(duì)所生成代碼進(jìn)行單元測(cè)試，減少了手工編碼和測(cè)試工作量，在航空、航天、國(guó)防、核電等安全要求極高的領(lǐng)域應(yīng)用非常廣泛。

1 軟件開(kāi)發(fā)方法的比較

1.1 傳統(tǒng)的軟件開(kāi)發(fā)模式

傳統(tǒng)的軟件開(kāi)發(fā)流程是一個(gè)“V”型的開(kāi)發(fā)流程[3]，軟件開(kāi)發(fā)中所有的工作都是以手工編碼和以代碼為中心而開(kāi)展的。包括需求分析、概要設(shè)計(jì)、詳細(xì)設(shè)計(jì)、編碼、單元測(cè)試、集成測(cè)試、系統(tǒng)測(cè)試等7個(gè)進(jìn)程。整個(gè)軟件開(kāi)發(fā)流程的核心就是軟件編碼，設(shè)計(jì)過(guò)程中所做需求分析、概要設(shè)計(jì)、詳細(xì)設(shè)計(jì)都是為了下一步的編碼。而單元測(cè)試、集成測(cè)試、軟件產(chǎn)品確認(rèn)都是為了驗(yàn)證代碼的正確性，如圖1所示。

傳統(tǒng)的軟件開(kāi)發(fā)流程主要存在以下不足：

（1）概要設(shè)計(jì)、詳細(xì)設(shè)計(jì)以圖表、自然語(yǔ)言表達(dá)，存在歧義，無(wú)法模擬仿真，不能保證正確體現(xiàn)規(guī)范要求；

圖1 傳統(tǒng)的軟件“V”型開(kāi)發(fā)流程

圖2 基于模型的軟件開(kāi)發(fā)流程

（2）軟件開(kāi)發(fā)完成之后難免會(huì)出現(xiàn)錯(cuò)誤，后期修改難度大；

（3）對(duì)代碼進(jìn)行單元測(cè)試的工作量大；

（4）手工編碼可靠性低；

（5）軟件開(kāi)發(fā)周期長(zhǎng)，開(kāi)發(fā)成本高。

1.2 SCADE基于模型的軟件開(kāi)發(fā)模式

基于模型的軟件開(kāi)發(fā)模式是一種面向模型的軟件設(shè)計(jì)方法，其基礎(chǔ)是模型和表達(dá)模型的語(yǔ)言。將目標(biāo)系統(tǒng)建立滿(mǎn)足需求的圖形化模型，實(shí)現(xiàn)了需求分析、概要設(shè)計(jì)和詳細(xì)設(shè)計(jì)。模型表達(dá)比傳統(tǒng)開(kāi)發(fā)模式采用的自然語(yǔ)言更能準(zhǔn)確地表明設(shè)計(jì)需求，保證了建立的模型與需求的一致性。并且可以直接對(duì)模型進(jìn)行早期模擬仿真和證明，在軟件開(kāi)發(fā)的早期階段發(fā)現(xiàn)錯(cuò)誤。SCADE軟件就是在這個(gè)理念上應(yīng)運(yùn)而生的。

根據(jù)需求所建立的SCADE 圖形化模型包含了軟件將實(shí)現(xiàn)的所有規(guī)范要求，可以將其視為SCADE 形式化功能規(guī)范。建模之后需要對(duì)模型進(jìn)行確認(rèn)，在SCADE 開(kāi)發(fā)環(huán)境下可以對(duì)模型自動(dòng)生成測(cè)試，在模型階段對(duì)建立的模型進(jìn)行單元測(cè)試和集成測(cè)試，確認(rèn)模型是否正確、完整地體現(xiàn)了其上層規(guī)范的需求。

在對(duì)模型進(jìn)行確認(rèn)后，使用SCADE 的代碼生成器，可以將所建立的模型自動(dòng)轉(zhuǎn)化為直接面向工程的ANSI C代碼，簡(jiǎn)化了開(kāi)發(fā)模式中的“編碼”過(guò)程，并且避免了傳統(tǒng)開(kāi)發(fā)模式中手工編寫(xiě)代碼引入的人工錯(cuò)誤，提高了軟件的可靠性。此外，無(wú)需對(duì)所生成的代碼進(jìn)行單元測(cè)試，節(jié)省了開(kāi)發(fā)時(shí)間，提高了開(kāi)發(fā)效率。因此，基于SCADE 進(jìn)行軟件開(kāi)發(fā)，使軟件開(kāi)發(fā)模式實(shí)現(xiàn)了從“V” 型到“Y” 型的轉(zhuǎn)化?；谀Ｐ偷能浖_(kāi)發(fā)模式如圖2所示。

2 基于SCADE的ATP系統(tǒng)設(shè)計(jì)

2.1 SCADESuite環(huán)境

LUSTRE是一種同步程序設(shè)計(jì)語(yǔ)言，是SCADE系統(tǒng)的核心部分。當(dāng)應(yīng)用SCADE開(kāi)發(fā)環(huán)境時(shí)，需要對(duì)系統(tǒng)進(jìn)行建模，再用設(shè)計(jì)時(shí)所用的圖形描述符轉(zhuǎn)化成LUSTRE語(yǔ)言，然后在此基礎(chǔ)上完成軟件設(shè)計(jì)過(guò)程中的靜態(tài)檢查、模擬仿真、形式驗(yàn)證、覆蓋率分析，最后生成滿(mǎn)足EN50128安全標(biāo)準(zhǔn)的C代碼。

2.2 SCADE的軟件建模方法

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

數(shù)據(jù)流圖從數(shù)據(jù)傳遞和加工的角度，以圖形方式表達(dá)系統(tǒng)的邏輯功能、數(shù)據(jù)在系統(tǒng)內(nèi)部的邏輯流向和邏輯變換過(guò)程，是結(jié)構(gòu)化系統(tǒng)分析方法的主要表達(dá)工具。適用于對(duì)系統(tǒng)的過(guò)程進(jìn)行描述，模型用系統(tǒng)的輸入輸出數(shù)據(jù)流和圖形化的操作符一起搭建模型。

2.2.2 有限狀態(tài)機(jī)

有限狀態(tài)機(jī)用來(lái)表示有限個(gè)狀態(tài)以及這些狀態(tài)之間的轉(zhuǎn)移和動(dòng)作行為的數(shù)學(xué)模型。

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

安全狀態(tài)機(jī)用豐富的形式化方法來(lái)處理復(fù)雜的結(jié)構(gòu)，適用于離散控制系統(tǒng)。它提供了順序、優(yōu)先級(jí)、層次、并行的狀態(tài)結(jié)構(gòu)。安全狀態(tài)機(jī)的圖形化方法可以很好的對(duì)反應(yīng)式系統(tǒng)建模，它用一系列的狀態(tài)、轉(zhuǎn)移和信號(hào)來(lái)表示反應(yīng)式系統(tǒng)的控制邏輯。系統(tǒng)的進(jìn)展用狀態(tài)和狀態(tài)之間的轉(zhuǎn)移來(lái)表示，轉(zhuǎn)移用信號(hào)來(lái)觸發(fā)。

2.3 基于SCADE的ATP功能建模

2.3.1 用數(shù)據(jù)流圖對(duì)列車(chē)間隔控制進(jìn)行建模

要測(cè)試列車(chē)的間隔距離是否在一個(gè)安全的范圍內(nèi)，ATP系統(tǒng)要計(jì)算列車(chē)的移動(dòng)授權(quán)（MA），當(dāng)列車(chē)匹配的進(jìn)路范圍內(nèi)有通信列車(chē)正在運(yùn)行時(shí)，前方列車(chē)將被視為障礙物，要確保在前行列車(chē)尾部的安全停車(chē)點(diǎn)前停車(chē)，保證系統(tǒng)內(nèi)所有列車(chē)之前的安全間隔。

計(jì)算列車(chē)的移動(dòng)授權(quán)，必須先確定列車(chē)移動(dòng)授權(quán)的計(jì)算范圍。移動(dòng)授權(quán)的起點(diǎn)為列車(chē)的車(chē)尾位置，移動(dòng)授權(quán)的終點(diǎn)是列車(chē)前方所有的可能進(jìn)路。MA首先要進(jìn)行初始化列車(chē)車(chē)尾到最遠(yuǎn)前方可能進(jìn)路的終點(diǎn)。

確定了列車(chē)的移動(dòng)授權(quán)范圍之后，遍歷前方列車(chē)，移動(dòng)授權(quán)的終點(diǎn)也即為前方列車(chē)的車(chē)尾。如果前方列車(chē)失去通信，移動(dòng)授權(quán)的終點(diǎn)要和前方列車(chē)所占用的計(jì)軸區(qū)段間隔至少一個(gè)區(qū)段。循環(huán)遍歷前車(chē)的SCADE數(shù)據(jù)流圖模型如圖3所示。輸入列車(chē)的信息I_TrainInfo、前車(chē)的信息I_FroTrainInfo，判斷前車(chē)是正常通信的列車(chē)Comm_Train或者失去通信的列車(chē)UnComm_Train計(jì)算MA，最后得出MA信息。

圖3 循環(huán)遍歷前車(chē)的SCADE數(shù)據(jù)流圖模型

列車(chē)移動(dòng)授權(quán)的信息數(shù)據(jù)都存儲(chǔ)在L_MAInfo1和L_MAInfo2中。輸出時(shí)，通過(guò)該結(jié)構(gòu)體構(gòu)造出移動(dòng)授權(quán)的具體通信幀。

2.3.2 用數(shù)據(jù)流圖對(duì)列車(chē)超速防護(hù)功能的建模

在列車(chē)的運(yùn)行過(guò)程中，車(chē)載ATP要連續(xù)檢測(cè)列車(chē)的位置和速度，一旦列車(chē)超速，ATP系統(tǒng)就要進(jìn)行報(bào)警處理，并且實(shí)施制動(dòng)，并記錄報(bào)警信息。這就要與區(qū)域控制器配合。區(qū)域控制器的主要任務(wù)是通過(guò)為其控制的列車(chē)提供移動(dòng)授權(quán)，保證列車(chē)在其區(qū)域內(nèi)不超速行駛，保證列車(chē)的安全。

超速防護(hù)功能的系統(tǒng)結(jié)構(gòu)如圖4所示。

圖4 超速防護(hù)功能結(jié)構(gòu)圖

根據(jù)上述對(duì)功能節(jié)點(diǎn)的劃分，在SCADE建模工具中定義對(duì)應(yīng)的功能節(jié)點(diǎn)，按照上述的系統(tǒng)結(jié)構(gòu)，建立超速防護(hù)功能的總體SCADE模型，如圖5所示。

圖5 超速防護(hù)總體SCADE模型

2.3.3 用有限狀態(tài)機(jī)對(duì)列車(chē)行為模型的建模

列車(chē)的行為模型是ATP系統(tǒng)設(shè)計(jì)中非常重要的部分，列車(chē)的行為是一種有限狀態(tài)的過(guò)程。初始狀態(tài)是第一個(gè)激活狀態(tài)。標(biāo)記選擇性的附加到轉(zhuǎn)移和狀態(tài)上。在ATP系統(tǒng)中，列車(chē)的行為是一系列連續(xù)的邏輯動(dòng)作，包括列車(chē)的登錄狀態(tài)、正常運(yùn)行狀態(tài)、列車(chē)的折返狀態(tài)、列車(chē)的接管狀態(tài)、列車(chē)的注銷(xiāo)狀態(tài)等。

根據(jù)ATP功能的需求，定義一個(gè)有限狀態(tài)機(jī)，命名為T(mén)rain_Status。對(duì)列車(chē)的每個(gè)狀態(tài)定義了一個(gè)變量，分別是S_Init，S_Moving，S_Reverse，S_Takeover，S_Handover和S_Cancel。如圖6所示，詳細(xì)描述了列車(chē)的行為模型。

圖6 列車(chē)的行為模型

2.3.4 用安全狀態(tài)機(jī)對(duì)列車(chē)的車(chē)門(mén)控制功能進(jìn)行建模

在列車(chē)運(yùn)行或者列車(chē)停車(chē)時(shí)，ATP系統(tǒng)要監(jiān)控列車(chē)車(chē)門(mén)的狀態(tài)。只有在確保安全的情況下，列車(chē)的車(chē)門(mén)才得以開(kāi)啟。車(chē)載ATP監(jiān)視列車(chē)的速度為零時(shí)，才能進(jìn)行乘客的上下車(chē)。并且在車(chē)門(mén)開(kāi)啟或者鎖閉之前，車(chē)載ATP要禁止列車(chē)行駛。

列車(chē)車(chē)門(mén)控制的安全狀態(tài)機(jī)模型如圖7所示。

圖7 列車(chē)車(chē)門(mén)控制的安全狀態(tài)機(jī)模型

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

目前，SCADE模型開(kāi)發(fā)工具還沒(méi)有專(zhuān)門(mén)針對(duì)軌道交通的開(kāi)發(fā)工具包。本文采用SCADE工具對(duì)城市軌道交通CBTC系統(tǒng)中ATP系統(tǒng)的部分功能進(jìn)行建模，對(duì)SCADE的軟件開(kāi)發(fā)方法和流程進(jìn)行了介紹。下一步研究的重點(diǎn)是對(duì)ATP系統(tǒng)的每一項(xiàng)功能選取合理的建模方式并對(duì)其進(jìn)行仿真。

[1]董凱霞，劉曉娟，朱耘燕.城市軌道交通CBTC系統(tǒng)車(chē)載ATP仿真研究[J].鐵道通信信號(hào)，2011，47（4）：12-15.

[2]Esterel Technology. SCADE Usage in Railways and Subways [R]. 2011（2）.

[3]王群偉，吳成富，陳懷民，徐 克. 基于SCADE的無(wú)人機(jī)三余度飛控系統(tǒng)設(shè)計(jì)及實(shí)現(xiàn)[J].測(cè)控技術(shù)，2007，26（4）：52-54.

責(zé)任編輯 方 圓

Application of SCADE in ATP software modeling for Urban Transit

BAI Rui, KANG Suiwu

( College of Electronic and Information Engineering, Lanzhou Jiaotong University, Lanzhou 730070, China )

Automatic Train Protection(ATP) System was an important part of Communication Based Train Control(CBTC) System. Car borne ATP bearded the important task of train safe movement, was directly related to security of the System, required high level safety and reliability. To satisfy the safety requirements of the car borne ATP software, model based software development method was proposed in this paper. It was used SCADE suite as the development tool, established ATP system function model, and showed the feasibility of SCADE on ATP software modeling.

ATP; safety-related; SCADE

U284∶TP39

A

2013-06-07

白 銳，在讀碩士研究生；康隨武，在讀碩士研究生。

1005-8451（2014）01-0037-04