形式化方法的工業(yè)應(yīng)用：軌交領(lǐng)域

作者 |王依玲上?？匕部尚跑浖?chuàng)新研究院系統(tǒng)建模組

版塊 |鑒源論壇 · 觀模

社群 |添加微信號(hào)“TICPShanghai”加入“上海控安51fusa安全社區(qū)”

引言：前面幾期文章介紹了形式化方法的發(fā)展歷史和具體技術(shù)，并從整體的角度介紹了形式化方法的工程化。本文將聚焦于軌交領(lǐng)域，從領(lǐng)域?qū)Ｓ玫男枨笞珜懪c分析工具Prema入手，介紹形式化方法在工業(yè)中的實(shí)際應(yīng)用。

01

背 景

隨著城市日新月異的發(fā)展，軌道交通的建設(shè)與分布越來越成為城市交通便捷、經(jīng)濟(jì)發(fā)達(dá)的重要標(biāo)志?！笆濉睍r(shí)期，城市軌道交通運(yùn)營(yíng)里程已達(dá) 6600 公里，預(yù)計(jì)到 2025 年，超大城市的軌道站點(diǎn) 800 米半徑覆蓋通勤比例將不小于 30%。軌道交通的控制軟件決定了系統(tǒng)運(yùn)行的安全性，如果控制軟件沒有按照預(yù)期方式運(yùn)行，則存在引發(fā)財(cái)產(chǎn)損失和人員傷亡的可能性。因此軌道交通控制軟件的質(zhì)量安全攸關(guān)，國(guó)家也對(duì)此出臺(tái)了嚴(yán)格的安全標(biāo)準(zhǔn)。

在軌道交通領(lǐng)域中，列車自動(dòng)控制系統(tǒng) (Automatic Train Control,ATC)系統(tǒng)包括三部分，ATP(Automatic Train Protection，列車自動(dòng)防護(hù)系統(tǒng))，ATO(Automatic Train Operation, 列車自動(dòng)運(yùn)行系統(tǒng))，和 ATS(Automatic Train Supervision，列車自動(dòng)監(jiān)控系統(tǒng))，它通過自動(dòng)地防止列車司機(jī)的失誤來提供高水平的列車安全。如圖1所示，ATO 是控制列車自動(dòng)運(yùn)行的系統(tǒng)，由車載設(shè)備和地面設(shè)備組成；ATP是為了確保列車一旦超過規(guī)定速度，立即施行制動(dòng)的系統(tǒng)，它也是由車載設(shè)備和地面設(shè)備所組成；ATS 系統(tǒng)是為了完成對(duì)列車的自動(dòng)監(jiān)控的系統(tǒng)，它由控制中心、車站、車場(chǎng)以及車載設(shè)備組成。三者的關(guān)系是，ATO 系統(tǒng)在 ATP 系統(tǒng)的保護(hù)下，根據(jù)ATS 的指令實(shí)現(xiàn)列車運(yùn)行的自動(dòng)駕駛、速度的自動(dòng)調(diào)整和列車車門的自動(dòng)控制。

圖1列車自動(dòng)控制系統(tǒng)結(jié)構(gòu)

需求分析是軟件設(shè)計(jì)的基礎(chǔ)，是軟件開發(fā)活動(dòng)中最為關(guān)鍵最早開始的環(huán)節(jié)。需求文檔中包含著列車控制系統(tǒng)的功能描述，可以通過對(duì)列車控制系統(tǒng)需求進(jìn)行分析，發(fā)現(xiàn)需求中系統(tǒng)的功能描述錯(cuò)誤。經(jīng)過長(zhǎng)期的研究和實(shí)踐，學(xué)術(shù)界和工業(yè)界都意識(shí)到從需求階段開始對(duì)列車控制系統(tǒng)的功能需求進(jìn)行檢查的必要性。然而目前的工業(yè)界中，人工檢查自然語(yǔ)言描述的列車控制系統(tǒng)需求不但低效，而且無法確保功能需求的正確性。

02

形式化建模方法概述

采用自然語(yǔ)言進(jìn)行需求描述會(huì)存在二義性，所以某些對(duì)撰寫者來說清晰無誤的表述，完全可能被其他人理解成其他意思。導(dǎo)致不同的開發(fā)者對(duì)相同的需求和設(shè)計(jì)產(chǎn)生模棱兩可的理解，從而導(dǎo)致開發(fā)效率的降低。為了避免這種情況的發(fā)生，我們采用標(biāo)準(zhǔn)的形式來描述需求和設(shè)計(jì)。這種標(biāo)準(zhǔn)形式一般以數(shù)學(xué)語(yǔ)言為基礎(chǔ)。這種標(biāo)準(zhǔn)化的描述規(guī)范就構(gòu)成了形式化方法的基礎(chǔ)。

形式化方法是建立在數(shù)學(xué)基礎(chǔ)上的針對(duì)數(shù)字化系統(tǒng)進(jìn)行規(guī)格說明撰寫、軟件開發(fā)、軟件驗(yàn)證的技術(shù)。它的數(shù)學(xué)基礎(chǔ)包括形式邏輯，離散數(shù)學(xué)和機(jī)器可識(shí)別語(yǔ)言。形式化模型是一種無二義性的用數(shù)學(xué)語(yǔ)法和語(yǔ)義刻畫的模型，是一種對(duì)軟件諸多方面的抽象表達(dá)形式，用于后續(xù)的分析、仿真和代碼生成（在有些條件下，直接從模型生成代碼可能無法實(shí)現(xiàn)）。應(yīng)用形式化方法的基礎(chǔ)是對(duì)即將開發(fā)的軟件建立一個(gè)形式化模型。

形式化方法包含兩項(xiàng)主要分支，形式化規(guī)格說明技術(shù)和形式化驗(yàn)證技術(shù)，而形式化驗(yàn)證技術(shù)又分為定理證明和模型檢查兩個(gè)分支，如圖2所示。

圖2 形式方法的構(gòu)成

在學(xué)術(shù)界和工業(yè)界，學(xué)者和工程人員為了保證列車安全運(yùn)行，主要有從以下方面對(duì)軌道交通控制系統(tǒng)的研究：形式化需求描述、建立模型和驗(yàn)證、對(duì)系統(tǒng)進(jìn)行仿真。這三者并不是孤立的，經(jīng)常結(jié)合在一起研究，如利用形式化方法對(duì)系統(tǒng)的需求進(jìn)行描述，然后建立模型、分析驗(yàn)證。

為了實(shí)現(xiàn)采用形式化方法保障軌道交通控制系統(tǒng)安全的目的，我們提出了一種針對(duì)軌道交通控制系統(tǒng)的需求建模形式化工程方法，并開發(fā)了一個(gè)集需求撰寫及分析功能于一體的工具Prema（Precise Requirements Editing, Modeling and Analysis 精確需求撰寫，建模與分析）用于輔助形式化工程方法的應(yīng)用。

03

軌交領(lǐng)域解決方案Prema

Prema對(duì)形式化技術(shù)的應(yīng)用主要包含兩個(gè)方面，形式化需求規(guī)格說明和模型檢查。為了可以對(duì)需求進(jìn)行形式化描述，我們提出了適配軌道交通領(lǐng)域的CASDL語(yǔ)言。對(duì)形式化語(yǔ)言描述的系統(tǒng)需求進(jìn)行需求建模后，可以在需求模型中驗(yàn)證布爾表達(dá)式描述的約束性質(zhì)是否成立。

Prema工具界面運(yùn)行主界面圖如下圖3所示，圖中主要分為左邊部分的編輯欄和右邊部分的展示欄。用戶可以在左邊撰寫需求，同時(shí)在右邊區(qū)域?qū)崟r(shí)顯示最終生成的文檔樣式，在編輯區(qū)域上方還有一些快捷工具以供用戶撰寫需求。

圖3 Prema工具界面

3.1 形式化需求規(guī)格說明

用戶在左側(cè)編輯欄用CASDL語(yǔ)言撰寫形式化需求，以下對(duì)CASDL語(yǔ)言規(guī)范進(jìn)行簡(jiǎn)單介紹。

由于軌道交通領(lǐng)域的控制系統(tǒng)通常周期性運(yùn)行，CASDL中的cycle有著用于表示目前系統(tǒng)的運(yùn)行進(jìn)行到了哪一個(gè)周期的特殊含義，其語(yǔ)法可以表示為如下形式：

● md :: = (cycle, Block, DefBlock, DataDictionary)

● Block :: = (identifier, Precondition, initial, State, Transition)

● DefBlock :: = (name, identifier, Tasks)

● Tasks :: = CFG

● Transition ::= (Source, Target, Condition, Action)

● DataDictionary ::= (V)

CASDL包含4個(gè)部分。Block部分描述的是系統(tǒng)狀態(tài)遷移情況，在Block里由唯一的identifier來對(duì)它進(jìn)行標(biāo)識(shí)，Precondition用于判斷系統(tǒng)狀態(tài)遷移的條件是否滿足，initial用于表示系統(tǒng)狀態(tài)遷移前的值，State中存儲(chǔ)了所有發(fā)生了狀態(tài)值改變的變量值，Transaction描述了狀態(tài)轉(zhuǎn)換的具體過程，描述該過程的結(jié)構(gòu)也在上述中被表述出來。其中，Source和Target分別代表狀態(tài)改變前的值和狀態(tài)改變后的值，Condition里記錄的是發(fā)生狀態(tài)遷移的需要滿足的條件集合，最后一項(xiàng)Action則記錄了該狀態(tài)轉(zhuǎn)換過程如何發(fā)生。

DefBlock描述的是計(jì)算模塊，它包含了模塊名稱name，唯一的標(biāo)識(shí)identifier,以及由控制流組成的計(jì)算任務(wù)Tasks。

Dictionary里記錄了在需求文檔建模過程中出現(xiàn)的變量。

如圖4所示為用CASDL書寫的示例，該例子中紅色部分表示的是展示狀態(tài)遷移情況的Block部分，它沒有返回值，只更改狀態(tài)變量的取值，使系統(tǒng)所處的狀態(tài)發(fā)生改變，即狀態(tài)遷移。其中State后跟隨的（k-1）表示第k-1個(gè)周期。黃色部分展示的是描述計(jì)算任務(wù)的defBlock部分。

圖4 Block與DefBlock示例

CASDL同樣定義了一些表達(dá)式用于描述DefBlock中面向計(jì)算的任務(wù)的計(jì)算過程，表達(dá)式的語(yǔ)法如下所示：

● SExpr :: = Const | Var | f(n)(SExpr)

●BTerm :: = True | False | p(n)(SExpr)

● IExpr :: = (after | duration)(BTerm,SExpr)

●BExpr :: = BTerm | ?BExpr | BExpr∨BExpr | BExpr∧BExpr

其中，語(yǔ)句表達(dá)式由一個(gè)常量，一個(gè)變量或者多個(gè)語(yǔ)句表達(dá)式組成，布爾變量的取值為True或False或者從狀態(tài)表達(dá)式的值推導(dǎo)而來。間隔表達(dá)式主要用于描述與時(shí)間有關(guān)的需求片段，比如在某個(gè)時(shí)間段或者在某個(gè)時(shí)間段后值為布爾值或者是某個(gè)語(yǔ)句表達(dá)式的計(jì)算值。而布爾表達(dá)式則由布爾值，布爾值的非值，或值或者與值組成。

同時(shí)CASDL也定義了幾種語(yǔ)句結(jié)構(gòu)：

● stmts :: = pStmt | cStmt

●pStmt :: = aStmt | skip

●aStmt :: = x := SExpr

●cStmt :: = stmts | if BExpr then stmts else stmts

語(yǔ)句集合包含復(fù)合語(yǔ)句或者是單獨(dú)的語(yǔ)句，其中pStmt由賦值語(yǔ)句或者skip語(yǔ)句組成，賦值語(yǔ)句可以表示為一個(gè)變量被賦予了一個(gè)表達(dá)式的值，而復(fù)合語(yǔ)句由語(yǔ)句集合構(gòu)成或者由一個(gè)選擇語(yǔ)句結(jié)構(gòu)構(gòu)成。

總體來說，CASDL與工程師的使用習(xí)慣相符合，學(xué)習(xí)和理解成本很低， 這種類python的語(yǔ)言容易令人接受，不過其語(yǔ)義與python仍有不同，如k在CASDL中是一個(gè)特殊的字母，它代表了系統(tǒng)運(yùn)行的周期。

3.2 模型檢查

在需求撰寫完成后，Prema工具提供靜態(tài)分析、狀態(tài)機(jī)模擬執(zhí)行、需求性質(zhì)驗(yàn)證等功能用于驗(yàn)證撰寫需求的正確性。需求性質(zhì)驗(yàn)證即模型檢查。

需求性質(zhì)驗(yàn)證是在需求檢查無語(yǔ)法錯(cuò)誤后，對(duì)需求模型進(jìn)行諸如不變式或者可達(dá)性之類的驗(yàn)證。其主要目的在于分析有影響關(guān)系的某些變量之間發(fā)生了變化，是否一定會(huì)影響到相關(guān)變量的變化，這對(duì)于理解和分析需求邏輯關(guān)系有著至關(guān)重要的作用。性質(zhì)驗(yàn)證的流程圖如圖5所示：

圖5 性質(zhì)驗(yàn)證流程圖

Prema性質(zhì)驗(yàn)證界面如圖6所示，用戶可選擇之前使用過的配置選項(xiàng)，也可以重新選擇。在該驗(yàn)證界面中，用戶選擇需要驗(yàn)證哪些需求條目，選擇完畢后，單擊Go按鈕會(huì)生成完整的驗(yàn)證界面。

圖6 性質(zhì)驗(yàn)證界面示意圖

工具會(huì)根據(jù)用戶所選擇的需求條目生成變量關(guān)系圖，提醒需求工程師該需求條目所描述的內(nèi)容，同時(shí)也避免錯(cuò)誤地勾選了需求條目。在確定選取了正確的需求條目后，在性質(zhì)撰寫區(qū)撰寫所需要驗(yàn)證的性質(zhì)，目前驗(yàn)證的性質(zhì)僅支持布爾表達(dá)式。填寫完初始狀態(tài)（可以不填）和性質(zhì)后，可以點(diǎn)擊check按鈕來驗(yàn)證所填寫的性質(zhì)是否是布爾表達(dá)式。

用戶選取了所要驗(yàn)證的需求條目和性質(zhì)，單擊Verify按鈕后，界面展示驗(yàn)證結(jié)果。需求工程師可根據(jù)反饋的信息查看需求是否滿足了性質(zhì)，如果沒有滿足性質(zhì)，則會(huì)給出不滿足該性質(zhì)時(shí)的反例。

通過使用Prema工具，能夠有效消除需求語(yǔ)句的模糊性和二義性，并保證需求的正確性。

04

總 結(jié)

近年來通過不斷地努力，形式化方法不僅僅在學(xué)術(shù)界取得很大的發(fā)展，同樣在工業(yè)界也已得到大量的應(yīng)用。形式化方法首先需要定義領(lǐng)域相關(guān)的需求描述語(yǔ)言，這種語(yǔ)言可以完全覆蓋該領(lǐng)域中的所有需求特征。其次通過建立的描述語(yǔ)言來刻畫和描述需求模型，并提供與之配套的算法來對(duì)需求模型進(jìn)行分析與驗(yàn)證。由于軌道交通領(lǐng)域?qū)τ诳刂葡到y(tǒng)有著嚴(yán)格要求，這為形式化方法的應(yīng)用提供了前提。在未來，形式化方法將更好地與工業(yè)實(shí)踐結(jié)合，為工業(yè)安全保駕護(hù)航。

主要參考文獻(xiàn)：

[1] 光明網(wǎng). 《“十四五”全國(guó)城市基礎(chǔ)設(shè)施建設(shè)規(guī)劃》印發(fā)[EB/OL].(2022-08-03)[2022-8-16].

[2] 王秀超.列車控制系統(tǒng)需求文檔的模型抽取與分析[D].貴陽(yáng):貴州大學(xué),2017

[3] 韋群,王鈺.軟件缺陷及其對(duì)軟件可靠性的影響分析[J].計(jì)算機(jī)應(yīng)用與軟件.2011, 28(1):145-149.

[4] 包丹珠.軌道交通系統(tǒng)需求分析與一致性測(cè)試[D].上海:華東師范大學(xué), 2016

[5] 劉陽(yáng).面向軌道交通控制系統(tǒng)的需求模型分析與驗(yàn)證[D].上海:華東師范大學(xué),2017

[6] 鄭寒月.面向軌道交通控制領(lǐng)域的基于需求的測(cè)試用例自動(dòng)生成方法研究[D].上海:華東師范大學(xué),2021

[7] Huang Y , Feng J , Zheng H ,et al.Prema: A Tool for Precise Requirements Editing, Modeling and Analysis[J]. 2019.DOI:10.1109/ASE.2019.00128.

審核編輯 黃宇