作者 |王依玲上?？匕部尚跑浖?chuàng)新研究院系統(tǒng)建模組
版塊 |鑒源論壇 · 觀模
社群 |添加微信號“TICPShanghai”加入“上?？匕?1fusa安全社區(qū)”
引言：前面幾期文章介紹了形式化方法的發(fā)展歷史和具體技術(shù)，并從整體的角度介紹了形式化方法的工程化。本文將聚焦于軌交領(lǐng)域，從領(lǐng)域?qū)Ｓ玫男枨笞珜懪c分析工具Prema入手，介紹形式化方法在工業(yè)中的實際應(yīng)用。
01
背 景
隨著城市日新月異的發(fā)展，軌道交通的建設(shè)與分布越來越成為城市交通便捷、經(jīng)濟發(fā)達的重要標志?！笆濉睍r期，城市軌道交通運營里程已達 6600 公里，預(yù)計到 2025 年，超大城市的軌道站點 800 米半徑覆蓋通勤比例將不小于 30%。軌道交通的控制軟件決定了系統(tǒng)運行的安全性，如果控制軟件沒有按照預(yù)期方式運行，則存在引發(fā)財產(chǎn)損失和人員傷亡的可能性。因此軌道交通控制軟件的質(zhì)量安全攸關(guān)，國家也對此出臺了嚴格的安全標準。
在軌道交通領(lǐng)域中，列車自動控制系統(tǒng) (Automatic Train Control,ATC)系統(tǒng)包括三部分，ATP(Automatic Train Protection，列車自動防護系統(tǒng))，ATO(Automatic Train Operation, 列車自動運行系統(tǒng))，和 ATS(Automatic Train Supervision，列車自動監(jiān)控系統(tǒng))，它通過自動地防止列車司機的失誤來提供高水平的列車安全。如圖1所示，ATO 是控制列車自動運行的系統(tǒng)，由車載設(shè)備和地面設(shè)備組成；ATP是為了確保列車一旦超過規(guī)定速度，立即施行制動的系統(tǒng)，它也是由車載設(shè)備和地面設(shè)備所組成；ATS 系統(tǒng)是為了完成對列車的自動監(jiān)控的系統(tǒng)，它由控制中心、車站、車場以及車載設(shè)備組成。三者的關(guān)系是，ATO 系統(tǒng)在 ATP 系統(tǒng)的保護下，根據(jù)ATS 的指令實現(xiàn)列車運行的自動駕駛、速度的自動調(diào)整和列車車門的自動控制。
圖1列車自動控制系統(tǒng)結(jié)構(gòu)
需求分析是軟件設(shè)計的基礎(chǔ)，是軟件開發(fā)活動中最為關(guān)鍵最早開始的環(huán)節(jié)。需求文檔中包含著列車控制系統(tǒng)的功能描述，可以通過對列車控制系統(tǒng)需求進行分析，發(fā)現(xiàn)需求中系統(tǒng)的功能描述錯誤。經(jīng)過長期的研究和實踐，學(xué)術(shù)界和工業(yè)界都意識到從需求階段開始對列車控制系統(tǒng)的功能需求進行檢查的必要性。然而目前的工業(yè)界中，人工檢查自然語言描述的列車控制系統(tǒng)需求不但低效，而且無法確保功能需求的正確性。
02
形式化建模方法概述
采用自然語言進行需求描述會存在二義性，所以某些對撰寫者來說清晰無誤的表述，完全可能被其他人理解成其他意思。導(dǎo)致不同的開發(fā)者對相同的需求和設(shè)計產(chǎn)生模棱兩可的理解，從而導(dǎo)致開發(fā)效率的降低。為了避免這種情況的發(fā)生，我們采用標準的形式來描述需求和設(shè)計。這種標準形式一般以數(shù)學(xué)語言為基礎(chǔ)。這種標準化的描述規(guī)范就構(gòu)成了形式化方法的基礎(chǔ)。
形式化方法是建立在數(shù)學(xué)基礎(chǔ)上的針對數(shù)字化系統(tǒng)進行規(guī)格說明撰寫、軟件開發(fā)、軟件驗證的技術(shù)。它的數(shù)學(xué)基礎(chǔ)包括形式邏輯，離散數(shù)學(xué)和機器可識別語言。形式化模型是一種無二義性的用數(shù)學(xué)語法和語義刻畫的模型，是一種對軟件諸多方面的抽象表達形式，用于后續(xù)的分析、仿真和代碼生成（在有些條件下，直接從模型生成代碼可能無法實現(xiàn)）。應(yīng)用形式化方法的基礎(chǔ)是對即將開發(fā)的軟件建立一個形式化模型。
形式化方法包含兩項主要分支，形式化規(guī)格說明技術(shù)和形式化驗證技術(shù)，而形式化驗證技術(shù)又分為定理證明和模型檢查兩個分支，如圖2所示。
圖2 形式方法的構(gòu)成
在學(xué)術(shù)界和工業(yè)界，學(xué)者和工程人員為了保證列車安全運行，主要有從以下方面對軌道交通控制系統(tǒng)的研究：形式化需求描述、建立模型和驗證、對系統(tǒng)進行仿真。這三者并不是孤立的，經(jīng)常結(jié)合在一起研究，如利用形式化方法對系統(tǒng)的需求進行描述，然后建立模型、分析驗證。
為了實現(xiàn)采用形式化方法保障軌道交通控制系統(tǒng)安全的目的，我們提出了一種針對軌道交通控制系統(tǒng)的需求建模形式化工程方法，并開發(fā)了一個集需求撰寫及分析功能于一體的工具Prema（Precise Requirements Editing, Modeling and Analysis 精確需求撰寫，建模與分析）用于輔助形式化工程方法的應(yīng)用。
03
軌交領(lǐng)域解決方案Prema
Prema對形式化技術(shù)的應(yīng)用主要包含兩個方面，形式化需求規(guī)格說明和模型檢查。為了可以對需求進行形式化描述，我們提出了適配軌道交通領(lǐng)域的CASDL語言。對形式化語言描述的系統(tǒng)需求進行需求建模后，可以在需求模型中驗證布爾表達式描述的約束性質(zhì)是否成立。
Prema工具界面運行主界面圖如下圖3所示，圖中主要分為左邊部分的編輯欄和右邊部分的展示欄。用戶可以在左邊撰寫需求，同時在右邊區(qū)域?qū)崟r顯示最終生成的文檔樣式，在編輯區(qū)域上方還有一些快捷工具以供用戶撰寫需求。
圖3 Prema工具界面
3.1 形式化需求規(guī)格說明
用戶在左側(cè)編輯欄用CASDL語言撰寫形式化需求，以下對CASDL語言規(guī)范進行簡單介紹。
由于軌道交通領(lǐng)域的控制系統(tǒng)通常周期性運行，CASDL中的cycle有著用于表示目前系統(tǒng)的運行進行到了哪一個周期的特殊含義，其語法可以表示為如下形式：
● 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個部分。Block部分描述的是系統(tǒng)狀態(tài)遷移情況，在Block里由唯一的identifier來對它進行標識，Precondition用于判斷系統(tǒng)狀態(tài)遷移的條件是否滿足，initial用于表示系統(tǒng)狀態(tài)遷移前的值，State中存儲了所有發(fā)生了狀態(tài)值改變的變量值，Transaction描述了狀態(tài)轉(zhuǎn)換的具體過程，描述該過程的結(jié)構(gòu)也在上述中被表述出來。其中，Source和Target分別代表狀態(tài)改變前的值和狀態(tài)改變后的值，Condition里記錄的是發(fā)生狀態(tài)遷移的需要滿足的條件集合，最后一項Action則記錄了該狀態(tài)轉(zhuǎn)換過程如何發(fā)生。
DefBlock描述的是計算模塊，它包含了模塊名稱name，唯一的標識identifier,以及由控制流組成的計算任務(wù)Tasks。
Dictionary里記錄了在需求文檔建模過程中出現(xiàn)的變量。
如圖4所示為用CASDL書寫的示例，該例子中紅色部分表示的是展示狀態(tài)遷移情況的Block部分，它沒有返回值，只更改狀態(tài)變量的取值，使系統(tǒng)所處的狀態(tài)發(fā)生改變，即狀態(tài)遷移。其中State后跟隨的（k-1）表示第k-1個周期。黃色部分展示的是描述計算任務(wù)的defBlock部分。
圖4 Block與DefBlock示例
CASDL同樣定義了一些表達式用于描述DefBlock中面向計算的任務(wù)的計算過程，表達式的語法如下所示：
● SExpr :: = Const | Var | f(n)(SExpr)
●BTerm :: = True | False | p(n)(SExpr)
● IExpr :: = (after | duration)(BTerm,SExpr)
●BExpr :: = BTerm | ?BExpr | BExpr∨BExpr | BExpr∧BExpr
其中，語句表達式由一個常量，一個變量或者多個語句表達式組成，布爾變量的取值為True或False或者從狀態(tài)表達式的值推導(dǎo)而來。間隔表達式主要用于描述與時間有關(guān)的需求片段，比如在某個時間段或者在某個時間段后值為布爾值或者是某個語句表達式的計算值。而布爾表達式則由布爾值，布爾值的非值，或值或者與值組成。
同時CASDL也定義了幾種語句結(jié)構(gòu)：
● stmts :: = pStmt | cStmt
●pStmt :: = aStmt | skip
●aStmt :: = x := SExpr
●cStmt :: = stmts | if BExpr then stmts else stmts
語句集合包含復(fù)合語句或者是單獨的語句，其中pStmt由賦值語句或者skip語句組成，賦值語句可以表示為一個變量被賦予了一個表達式的值，而復(fù)合語句由語句集合構(gòu)成或者由一個選擇語句結(jié)構(gòu)構(gòu)成。
總體來說，CASDL與工程師的使用習(xí)慣相符合，學(xué)習(xí)和理解成本很低， 這種類python的語言容易令人接受，不過其語義與python仍有不同，如k在CASDL中是一個特殊的字母，它代表了系統(tǒng)運行的周期。
3.2 模型檢查
在需求撰寫完成后，Prema工具提供靜態(tài)分析、狀態(tài)機模擬執(zhí)行、需求性質(zhì)驗證等功能用于驗證撰寫需求的正確性。需求性質(zhì)驗證即模型檢查。
需求性質(zhì)驗證是在需求檢查無語法錯誤后，對需求模型進行諸如不變式或者可達性之類的驗證。其主要目的在于分析有影響關(guān)系的某些變量之間發(fā)生了變化，是否一定會影響到相關(guān)變量的變化，這對于理解和分析需求邏輯關(guān)系有著至關(guān)重要的作用。性質(zhì)驗證的流程圖如圖5所示：
圖5 性質(zhì)驗證流程圖
Prema性質(zhì)驗證界面如圖6所示，用戶可選擇之前使用過的配置選項，也可以重新選擇。在該驗證界面中，用戶選擇需要驗證哪些需求條目，選擇完畢后，單擊Go按鈕會生成完整的驗證界面。
圖6 性質(zhì)驗證界面示意圖
工具會根據(jù)用戶所選擇的需求條目生成變量關(guān)系圖，提醒需求工程師該需求條目所描述的內(nèi)容，同時也避免錯誤地勾選了需求條目。在確定選取了正確的需求條目后，在性質(zhì)撰寫區(qū)撰寫所需要驗證的性質(zhì)，目前驗證的性質(zhì)僅支持布爾表達式。填寫完初始狀態(tài)（可以不填）和性質(zhì)后，可以點擊check按鈕來驗證所填寫的性質(zhì)是否是布爾表達式。
用戶選取了所要驗證的需求條目和性質(zhì)，單擊Verify按鈕后，界面展示驗證結(jié)果。需求工程師可根據(jù)反饋的信息查看需求是否滿足了性質(zhì)，如果沒有滿足性質(zhì)，則會給出不滿足該性質(zhì)時的反例。
通過使用Prema工具，能夠有效消除需求語句的模糊性和二義性，并保證需求的正確性。
04
總 結(jié)
近年來通過不斷地努力，形式化方法不僅僅在學(xué)術(shù)界取得很大的發(fā)展，同樣在工業(yè)界也已得到大量的應(yīng)用。形式化方法首先需要定義領(lǐng)域相關(guān)的需求描述語言，這種語言可以完全覆蓋該領(lǐng)域中的所有需求特征。其次通過建立的描述語言來刻畫和描述需求模型，并提供與之配套的算法來對需求模型進行分析與驗證。由于軌道交通領(lǐng)域?qū)τ诳刂葡到y(tǒng)有著嚴格要求，這為形式化方法的應(yīng)用提供了前提。在未來，形式化方法將更好地與工業(yè)實踐結(jié)合，為工業(yè)安全保駕護航。
主要參考文獻：
[1] 光明網(wǎng). 《“十四五”全國城市基礎(chǔ)設(shè)施建設(shè)規(guī)劃》印發(fā)[EB/OL].(2022-08-03)[2022-8-16].
[2] 王秀超.列車控制系統(tǒng)需求文檔的模型抽取與分析[D].貴陽:貴州大學(xué),2017
[3] 韋群,王鈺.軟件缺陷及其對軟件可靠性的影響分析[J].計算機應(yīng)用與軟件.2011, 28(1):145-149.
[4] 包丹珠.軌道交通系統(tǒng)需求分析與一致性測試[D].上海:華東師范大學(xué), 2016
[5] 劉陽.面向軌道交通控制系統(tǒng)的需求模型分析與驗證[D].上海:華東師范大學(xué),2017
[6] 鄭寒月.面向軌道交通控制領(lǐ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.
審核編輯 黃宇