百度做的网站后台怎么更新,网站要学什么,瑞昌市环保局网站建设,设计交流网站作者 | 王依玲 上海控安可信软件创新研究院系统建模组
版块 | 鉴源论坛 观模
社群 | 添加微信号“TICPShanghai”加入“上海控安51fusa安全社区” 引言#xff1a;前面几期文章介绍了形式化方法的发展历史和具体技术#xff0c;并从整体的角度介绍了形式化方法的工程化。本…作者 | 王依玲 上海控安可信软件创新研究院系统建模组
版块 | 鉴源论坛 · 观模
社群 | 添加微信号“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 形式方法的构成
在学术界和工业界学者和工程人员为了保证列车安全运行主要有从以下方面对轨道交通控制系统的研究形式化需求描述、建立模型和验证、对系统进行仿真。这三者并不是孤立的经常结合在一起研究如利用形式化方法对系统的需求进行描述然后建立模型、分析验证。
为了实现采用形式化方法保障轨道交通控制系统安全的目的我们提出了一种针对轨道交通控制系统的需求建模形式化工程方法并开发了一个集需求撰写及分析功能于一体的工具PremaPrecise 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.
