面向复杂系统的嵌入式软件高可信建模与验证方法

01

引 言

在航空航天、轨道交通、核能电力、汽车电子等安全关键领域，嵌入式控制软件一旦出现故障，其造成的损失无法接受。面对软件规模和复杂度的不断提升，传统的软件开发方法已无法满足越来越繁杂庞大的安全关键系统。为应对这一挑战，上海控安研发了高可信嵌入式软件建模开发工具SmartRocket Modeler。

高可信嵌入式软件建模开发工具

SmartRocket Modeler

本文主要介绍SmartRocket Modeler工具的研发背景、核心理论支撑、功能模块概览，阐述它如何为复杂软件的开发提供更可靠、高效的解决方案。

02

研发背景

嵌入式控制软件是嵌入式系统的重要组成部分，在航空航天、轨道交通、核能电力、汽车电子等安全攸关领域的重要性尤为突出，一旦出现故障，其造成的损失无法接受。如波音737 Max坠机事件是由自动失速防止系统（MCAS）的软件缺陷导致的未能准确处理传感器故障造成的，最终导致346人遇难，经济损失达4万亿元的严重后果。

随着计算机技术的快速发展、工业制造业的不断升级，对安全关键系统的要求也越来越严格，从而使得软件应用在安全关键系统中承担越来越多的功能。与此同时软件的规模和复杂度也不断提升，导致软件的缺陷密度和失效问题也显著增加。采用传统的软件开发方法来进行现代高可信嵌入式软件开发具有研发工作反复进行、研发周期大幅延长、成本大幅度增加、软件难以进行维护以及升级等问题。近半个世纪以来，由于软件问题造成安全关键系统出现故障所导致的损失难以衡量，传统的软件开发模式已无法满足越来越繁杂庞大的安全关键系统。因此SmartRocket Modeler可视化建模开发工具应需而生。它可以根据用户在可视化建模系统中所建立的应用软件模型，自动生成应用软件的框架和源代码。其优点包括：

✦ 构建的模型不具有二义性，可读性强。在代码自动生成的过程中，可以通过可视化图形界面的方式让用户使用起来更加明确、清晰，唯一模型便于交流和维护；

✦ 代码自动生成具有特定规则。通过加载预先定制好的模型库，自动生成代码的规范性可以大幅度提升；

✦ 准确且高效。模型在进行代码生成前需经过验证，保证正确的模型生成正确的代码。避免手工编程带来的繁琐和与需求不一致性的风险，从而保证代码质量符合规则要求；

✦ 在缩短软件开发周期的情况下，可节省时间、节约成本、大大减少代码错误产生率。

该产品可实现国外垄断工具SCADE Suite的国产化替代，解决需求建模、验证领域的“卡脖子”技术，可填补国内在数据流可视化建模和验证领域的空白，并达到国内先进水平。

03

理论支撑

1. 从V字开发模型到Y字开发模型

传统的“V”字软件开发流程中，以文档开发为中心，用户经历需求分析-概要设计-详细设计-编码-单元测试-集成测试-系统测试等阶段，得到相对可靠的软件产品。在此过程中，由于自然语言的二义性、文档沟通难以完全表述清晰等原因，可能存在如下问题：

✦ 手动编码与用户需求难以完全贴合；

✦ 以代码为核心，早期开发难以验证；

✦ 安全关键领域要求高，编码逻辑易混乱。

✦ ......

而符合MBSE的“Y”字开发则具有如下优势：

✦ 人机互动友好易用，模块化设计，便于资产留存和理解；

✦ 以模型为中心，避免实现过程二义性；

✦ 简化软件开发过程，缩短软件开发周期与成本；

✦ ......

因此，对于功能安全性和可靠性要求更高的嵌入式控制软件，更适合使用SmartRocket Modeler提供的基于模型的开发方式。

2. 同步假设

同步假设是指假设反应式系统响应速度足够快，则系统接收环境输入后可立即响应并产生输出，并等待下一个输入，在此期间系统内部状态保持不变。对于嵌入式控制系统而言，系统周期性运行，一个周期内的计算瞬时完成，不会存在系统资源不足或超时的情况。

在实际运行中，由于技术或成本的限制，一般是通过控制系统获得任意两次输入的时间间隔大于系统的响应时间的方式来实现同步假设的。当周期性运行的系统满足如下条件时，即可认为符合同步假设：

✦ 系统在周期开始时获得输入，且当前周期内输入不变；

✦ 中间变量与输出变量在周期内计算后，值在本周期内不会改变；

✦ 运行周期之间不会重叠。

3. 同步数据流语言Lustre

Lustre建模语言每一个变量都代表一个数据流，流是一个给定数据类型的值的无限序列，具有数值和时钟两个特性。Lustre提供的时间运算符对数据流进行采样，也可以获取之前周期的流值，为控制系统的建模提供了方便。其主要应用领域有自动化控制以及信号处理系统等。

SmartRocket Modeler功能背后以Lustre语言为支撑，提供具有精确语义的可验证模型的构建、验证、测试和C代码生成等功能。

4. 反应式系统

SmartRocket Modeler面向反应式系统，即与环境持续交互的系统。反应式系统可看作序列到序列的函数，其工作模式为：

✦ 反应式系统读入环境变量；

✦ 计算出逻辑运算结果，并反馈至环境中；

✦ 通过系统逻辑运算更改内部状态。

当使用f作为反应式系统的一次逻辑计算时，工作模式可以表达为：

04

产品功能

SmartRocket Modeler工具面向航空航天、轨道交通、核能、汽车电子等领域，作用于传统软件开发流程的详细设计阶段和编码阶段，提供模型设计、分析、测试、代码生成一系列功能。

1. 图形化建模：根据对系统需求的分析，运用数据流构件、状态机构件库进行基于模型的系统设计。图形化建模基于同步数据流语言，因此建模机制具有严格的数学语义。Modeler提供的构件库包含数学构件、比较构件、数组/结构体构件、逻辑构件、位构件、时态构件、分支构件、条件块构件、状态机构件和高阶构件等，支持数据流和状态机建模，全面对标SCADE Suite建模算子。

2. 静态分析：静态分析通过从设计模型中抽取出的多层次模型刻面，充分呈现系统不同层次的功能、行为、数据定义及数据传递特征，用于进行交互式完整性检查。检查模型是否满足预定义的设计规则的维度包含类型检查、数据依赖关系分析、状态迁移分析。可帮助设计人员在开发的早期就排除模型中的基本错误。

3. 耦合度分析：耦合度分析功能以报告的形式展示项目模型中控制耦合（CC）、数据耦合（DC）的分析结果。工具提供的耦合度分析功能可帮助航空航天领域的客户满足DO-178B/C相关规定。

4. 模拟仿真：模拟仿真功能通过模型仿真和断点调试确保模型在特定物理场景中的动态运行能力，并对运行结果进行可视化展示满足更直观的分析。该功能包含两种模式：基于模型的仿真调试和基于C代码的仿真调试。 对于同样的仿真用例，两种仿真模式的仿真结果相同。

5. 基于模型的测试：工具提供基于模型的测试功能。分为批量测试和覆盖率分析两个部分。批量测试功能允许用户同时执行多个测试用例文件，验证模型运行结果是否符合预期，确保设计模型的正确性。覆盖率分析功能基于测试用例文件进行指定覆盖准则的覆盖率分析，可选择的覆盖率准则包括：OMC/DC、influence、ODC。

6. 代码生成：在排除模型早期错误，保障模型一致性、正确性和安全性基础上，通过模型、LUSTRE 语言、代码转换，工具可实现 C 代码自动生成，有效减少用户重复编码工作。

7. 代码与模型的追溯：工具提供模型与代码的追溯查看，以变量为单位，直观展示C 代码和模型的对应关系，从侧面证明代码生成的可靠性。

8. 设计文档生成：工具支持对模型的设计文档自动生成，封面信息可进行配置，提供生成格式为html和docx文档。

9. 模型迁移：Modeler对SCADE Suite的模型进行了兼容，支持现有SCADE项目的一键导入，以及Modeler项目的一键导出，无缝衔接现有开发流程，便于模型资产复用。

05

总 结

SmartRocket Modeler基于严谨的理论和工程实践，为高可信嵌入式软件的开发提供了从建模、验证到代码生成的全流程支持。

本文主要介绍了工具的起源与核心理论。在后续的推送中，我们将逐一详细介绍各项具体功能，如图形化建模、静态分析、代码生成等，欢迎您持续关注。

审核编辑 黄宇