安全功能建模与仿真——模型与代码联动
在2021年的一篇文章中，我们介绍了通过功能建模与仿真进行动态、可视化的安全分析实践（《安全功能建模与仿真——让安全分析动起来》）。依靠功能建模与仿真，可以通过大量随机变量组合验证更多场景，也可以一键运行复杂逻辑模拟系统反应，让安全分析动起来。
但是，由于此前的安全功能模型是基于需求建立的，并不能反应最终软件或产品的行为。所以该如何验证软件实现是否和模型一致？尤其是如何确保软件贯彻了模型中定义的安全功能？今天这篇文章将给出答案——模型与代码联动。下面就来看一下怎样让代码参与到模型中、实现需求与代码联动。
我们使用的建模工具支持多种形式的外部系统导入，其中最直接的方式便是将代码编译为DLL格式导入到功能模型中，与需求一起联合仿真测试。整体结构如下：
◈ 场景输入模块：借助工具中提供的逻辑语句、状态机及随机变量等编写场景输入模块，为后续需求模型和DLL模块提供相同的输入变量组合，每一种输入变量组合都可以对应系统的特定场景
◈ 需求模型：可以是一个完整的系统功能，也可以是其中一个模块，由功能建模得到
◈ DLL模块：由与需求模型相对应的代码编译得到
◈ “观察者”模式：将DLL模块的输出连接到需求模块输入，需求模型运行模式选择为“观察者”，需求模型的输出变量即为期望测试结果，一旦DLL模块的输出变量与期望结果不符，工具将报错。
需求与代码联动
在上一篇文章中，我们对区域控制器的主备切换功能进行了建模，分析了多种场景下的双机切换。需求与代码联动的尝试就是在这个模型中进行的。
功能建模
既有的功能模型基于完整的主备切换功能搭建，此次我们选取了其中的核心功能模块即“冗余状态判定”进行代码联动测试。在既有模型的基础上，将“冗余状态判定”相关需求进一步模块化，调整输入变量接口，并定义和DLL的接口。既有模型包含两个冗余的控制器，我们选取其中的A机进行需求和代码的联合仿真。
双机切换仿真环境
在A机的模型中，将“冗余状态判定”相关需求封装为需求模块，与将要导入的DLL模块具有相同的输入变量。这些输入变量表示了测试场景，将由之后的测试模块提供。
A机模型
DLL生成
作为功能强大、逻辑复杂的安全攸关控制系统，区域控制器软件体量非常庞大。为了适配模型中的“冗余状态判定”这个单一功能，首先需要将相关测试代码抽出，定义模型所需的输入和输出接口，并为其他代码接口打桩。再将处理后的测试代码编译为DLL，通过指定路径将DLL导入功能模型即可。
测试代码
仿真测试
如前文所述，建模是为了需求和代码联动，也就是需求和代码一起“跑起来”，而测试场景就是“跑起来”的发动机。
借助工具提供的测试功能，我们定义了不同的测试场景，通过常量赋值、状态机转换、随机取值等语句定义每个变量，以仿真所需的测试场景。同时，每个测试场景的运行模式、运行次数、最大运行周期等参数可以分别指定，实现一键运行多个场景，充分验证软件行为。
测试过程中，需求模块实时校验软件模块的输出结果。若一致，则“观察者”状态为“1”，并且测试场景运行完成后显示绿色。如果出现代码和需求模型不一致现象，工具将提示“观察者违背”并在状态栏报错。如下图所示，前三个测试场景均触发“观察者违背”错误（仅作效果演示，非正式软件），可根据详细错误信息定位到具体步骤进一步分析。此外，测试完成后状态栏还可以提示需求覆盖率等信息。
运行实时显示
测试结果展示
结语
以上便是我们今天介绍的通过建模与仿真工具实现需求与代码联动的示例。在功能建模的基础上，将相关软件代码以DLL格式导入到模型中，实现了需求与软件的联动。通过测试场景定义，需求模块与代码模块的输入变量完全一致，需求模块实时检验代码运行结果，得到错误信息与覆盖率统计帮助分析需求与代码实现。
与上一篇文章中介绍的一样，建模与仿真最大的优势便是可以安全分析“动起来”，而功能模型中需求与代码的联动不仅实现了动态的功能安全分析，还引入了软件代码，使两者可以一起动，以需求为参照实时检验软件运行结果，让软件安全分析也可以动态化。就像最近的网红工具ChatGPT根据已知数据给出带有不确定性的最佳答案，与代码联动的功能模型也可以通过海量数据驱动软件行为，对于功能的安全属性，给出确定性的答案。
袁捷
上海电气泰雷兹交通自动化系统有限公司系统安全工程师
余志浩
上海电气泰雷兹交通自动化系统有限公司系统安全工程师
文章转自公众号“上海电气泰雷兹 TST”
- 用户评论
