作者 |王依玲上?？匕部尚跑浖撔卵芯吭合到y建模組

版塊 |鑒源論壇 · 觀模

社群 |添加微信號“TICPShanghai”加入“上?？匕?1fusa安全社區”

引言：前面幾期文章介紹了形式化方法的發展歷史和具體技術，并從整體的角度介紹了形式化方法的工程化。本文將聚焦于軌交領域，從領域專用的需求撰寫與分析工具Prema入手，介紹形式化方法在工業中的實際應用。

01

背 景

隨著城市日新月異的發展，軌道交通的建設與分布越來越成為城市交通便捷、經濟發達的重要標志。“十三五”時期，城市軌道交通運營里程已達 6600 公里，預計到 2025 年，超大城市的軌道站點 800 米半徑覆蓋通勤比例將不小于 30%。軌道交通的控制軟件決定了系統運行的安全性，如果控制軟件沒有按照預期方式運行，則存在引發財產損失和人員傷亡的可能性。因此軌道交通控制軟件的質量安全攸關，國家也對此出臺了嚴格的安全標準。

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

圖1列車自動控制系統結構

需求分析是軟件設計的基礎，是軟件開發活動中最為關鍵最早開始的環節。需求文檔中包含著列車控制系統的功能描述，可以通過對列車控制系統需求進行分析，發現需求中系統的功能描述錯誤。經過長期的研究和實踐，學術界和工業界都意識到從需求階段開始對列車控制系統的功能需求進行檢查的必要性。然而目前的工業界中，人工檢查自然語言描述的列車控制系統需求不但低效，而且無法確保功能需求的正確性。

02

形式化建模方法概述

采用自然語言進行需求描述會存在二義性，所以某些對撰寫者來說清晰無誤的表述，完全可能被其他人理解成其他意思。導致不同的開發者對相同的需求和設計產生模棱兩可的理解，從而導致開發效率的降低。為了避免這種情況的發生，我們采用標準的形式來描述需求和設計。這種標準形式一般以數學語言為基礎。這種標準化的描述規范就構成了形式化方法的基礎。

形式化方法是建立在數學基礎上的針對數字化系統進行規格說明撰寫、軟件開發、軟件驗證的技術。它的數學基礎包括形式邏輯，離散數學和機器可識別語言。形式化模型是一種無二義性的用數學語法和語義刻畫的模型，是一種對軟件諸多方面的抽象表達形式，用于后續的分析、仿真和代碼生成（在有些條件下，直接從模型生成代碼可能無法實現）。應用形式化方法的基礎是對即將開發的軟件建立一個形式化模型。

形式化方法包含兩項主要分支，形式化規格說明技術和形式化驗證技術，而形式化驗證技術又分為定理證明和模型檢查兩個分支，如圖2所示。

圖2 形式方法的構成

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

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

03

軌交領域解決方案Prema

Prema對形式化技術的應用主要包含兩個方面，形式化需求規格說明和模型檢查。為了可以對需求進行形式化描述，我們提出了適配軌道交通領域的CASDL語言。對形式化語言描述的系統需求進行需求建模后，可以在需求模型中驗證布爾表達式描述的約束性質是否成立。

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

圖3 Prema工具界面

3.1 形式化需求規格說明

用戶在左側編輯欄用CASDL語言撰寫形式化需求，以下對CASDL語言規范進行簡單介紹。

由于軌道交通領域的控制系統通常周期性運行，CASDL中的cycle有著用于表示目前系統的運行進行到了哪一個周期的特殊含義，其語法可以表示為如下形式：

● 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部分描述的是系統狀態遷移情況，在Block里由唯一的identifier來對它進行標識，Precondition用于判斷系統狀態遷移的條件是否滿足，initial用于表示系統狀態遷移前的值，State中存儲了所有發生了狀態值改變的變量值，Transaction描述了狀態轉換的具體過程，描述該過程的結構也在上述中被表述出來。其中，Source和Target分別代表狀態改變前的值和狀態改變后的值，Condition里記錄的是發生狀態遷移的需要滿足的條件集合，最后一項Action則記錄了該狀態轉換過程如何發生。

DefBlock描述的是計算模塊，它包含了模塊名稱name，唯一的標識identifier,以及由控制流組成的計算任務Tasks。

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

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

圖4 Block與DefBlock示例

CASDL同樣定義了一些表達式用于描述DefBlock中面向計算的任務的計算過程，表達式的語法如下所示：

● 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或者從狀態表達式的值推導而來。間隔表達式主要用于描述與時間有關的需求片段，比如在某個時間段或者在某個時間段后值為布爾值或者是某個語句表達式的計算值。而布爾表達式則由布爾值，布爾值的非值，或值或者與值組成。

同時CASDL也定義了幾種語句結構：

● stmts :: = pStmt | cStmt

●pStmt :: = aStmt | skip

●aStmt :: = x := SExpr

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

語句集合包含復合語句或者是單獨的語句，其中pStmt由賦值語句或者skip語句組成，賦值語句可以表示為一個變量被賦予了一個表達式的值，而復合語句由語句集合構成或者由一個選擇語句結構構成。

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

3.2 模型檢查

在需求撰寫完成后，Prema工具提供靜態分析、狀態機模擬執行、需求性質驗證等功能用于驗證撰寫需求的正確性。需求性質驗證即模型檢查。

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

圖5 性質驗證流程圖

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

圖6 性質驗證界面示意圖

工具會根據用戶所選擇的需求條目生成變量關系圖，提醒需求工程師該需求條目所描述的內容，同時也避免錯誤地勾選了需求條目。在確定選取了正確的需求條目后，在性質撰寫區撰寫所需要驗證的性質，目前驗證的性質僅支持布爾表達式。填寫完初始狀態（可以不填）和性質后，可以點擊check按鈕來驗證所填寫的性質是否是布爾表達式。

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

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

04

總 結

近年來通過不斷地努力，形式化方法不僅僅在學術界取得很大的發展，同樣在工業界也已得到大量的應用。形式化方法首先需要定義領域相關的需求描述語言，這種語言可以完全覆蓋該領域中的所有需求特征。其次通過建立的描述語言來刻畫和描述需求模型，并提供與之配套的算法來對需求模型進行分析與驗證。由于軌道交通領域對于控制系統有著嚴格要求，這為形式化方法的應用提供了前提。在未來，形式化方法將更好地與工業實踐結合，為工業安全保駕護航。

主要參考文獻：

[1] 光明網. 《“十四五”全國城市基礎設施建設規劃》印發[EB/OL].(2022-08-03)[2022-8-16].

[2] 王秀超.列車控制系統需求文檔的模型抽取與分析[D].貴陽:貴州大學,2017

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

[4] 包丹珠.軌道交通系統需求分析與一致性測試[D].上海:華東師范大學, 2016

[5] 劉陽.面向軌道交通控制系統的需求模型分析與驗證[D].上海:華東師范大學,2017

[6] 鄭寒月.面向軌道交通控制領域的基于需求的測試用例自動生成方法研究[D].上海:華東師范大學,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.

審核編輯 黃宇