作者 | 王依玲 上海控安可信软件创新研究院系统建模组
版块 | 鉴源论坛 · 观模
社群 | 添加微信号“TICPShanghai”加入“上海控安51fusa安全社区”
引言：前面几期文章介绍了形式化方法的发展历史和具体技术，并从整体的角度介绍了形式化方法的工程化。本文将聚焦于轨交领域，从领域专用的需求撰写与分析工具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].https://m.gmw.cn/baijia/2022-08/03/35929147.html.
[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.
