图形化建模在嵌入式高可信软件开发中的应用

01

引 言

在上一篇推送中（面向复杂系统的嵌入式软件高可信建模与验证方法），我们介绍了上海控安研发的高可信嵌入式软件建模开发工具SmartRocket Modeler。它基于严谨的同步数据流语言理论，为航空航天、轨道交通等安全关键领域的嵌入式软件开发，提供了从建模、验证到代码生成的全流程支持。本文将深入探讨SmartRocket Modeler的核心功能之一——图形化建模，详细阐述它如何将复杂、抽象的系统需求，转化为直观、精确、无二义性的可视化模型，从而为构建高可靠性的嵌入式软件奠定坚实的基础。

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

SmartRocket Modeler

02

为何需要图形化建模？

传统的软件开发方法，在需求分析、详细设计和编码阶段，主要依赖自然语言描述的文档和手写代码。这种方式存在着天然的鸿沟：自然语言固有的二义性，使得需求分析人员、设计人员与编码人员之间对同一功能的理解容易出现偏差；随着软件规模的增长，用文字难以清晰描述系统中错综复杂的数据流和控制逻辑，设计缺陷难以在早期发现；手动编码不仅效率低下，而且容易引入与设计不符的人为错误，对安全关键系统而言，这种风险是致命的。

为了解决这些问题，基于模型的设计方法应运而生。SmartRocket Modeler的图形化建模功能，正是这一方法论的最佳实践。它允许工程师使用标准化的图形元素（如数据流图、状态机）来构建系统。这个模型不仅是设计的蓝图，更是后续仿真、验证和代码自动生成的唯一、精确的源头，从根本上解决了传统开发模式的痛点。

03

核心理论与技术支撑

1. 从“以文档为中心”到“以模型为中心”

回顾第一篇中提到的软件开发“V字模型”，其核心是“以文档为中心”。而SmartRocket Modeler所倡导的，是基于模型的“Y字开发流程”。图形化建模正是实现这一转变的关键。

在“Y字模型”中，图形化模型取代了冗长的设计文档，成为开发流程的核心资产。所有的后续工作，如分析、仿真、测试和代码生成，都围绕这个统一的模型展开。这种转变带来的优势是革命性的：

✦ 消除二义性：模型具有精确的数学语义，确保了设计与实现的高度一致性。

✦ 早期验证：在设计阶段即可对模型进行仿真运行，直观地验证功能逻辑是否符合预期，将缺陷消灭在萌芽状态。

✦ 高效沟通：图形化的表达方式直观易懂，能够有效拉近领域专家、系统工程师和软件开发人员之间的距离，降低沟通成本。

✦ 自动化实现：基于模型可以自动生成高质量的生产级代码，将工程师从繁琐易错的手工编码中解放出来。

2. 坚实的理论基石：同步数据流与Lustre语言

SmartRocket Modeler图形化建模的强大功能，并非空中楼阁，而是建立在同步假设和同步数据流语言Lustre这两个坚实的理论基础之上。同步假设是反应式系统建模的核心。它假设系统在接收输入的瞬间就能完成计算并产生输出，然后等待下一个时钟周期。这为复杂的嵌入式控制逻辑提供了简洁而强大的时间抽象，使得工程师可以专注于功能逻辑的设计，而无需过早陷入复杂的时间调度细节。而同步数据流语言Lustre则是SmartRocket Modeler的“灵魂”。每个图形化构件、每一条数据连线，在后台都对应着精确的Lustre代码。Lustre语言将系统中的所有变量都视为随时间变化的“数据流”，并提供了丰富的操作符（如算术运算、逻辑运算、以及`pre`（前一周期值）、`->`（初始化）等时态算子）来对这些流进行操作。这种严格的数学语义保证了模型的确定性、完整性和一致性，为后续的形式化验证和高质量代码生成提供了可能。

因此，您在SmartRocket Modeler画布上拖拽的每一个构件，连接的每一条线，都是在“书写”一份形式化的、可验证的、无二义性的系统规范。

04

产品功能：图形化建模

SmartRocket Modeler的图形化建模环境，旨在为用户提供高效、直观、所见即所得的设计体验。它不仅仅是将构件简单罗列，而是提供了一套完整、强大的建模体系。

1. 丰富的建模元素库

工欲善其事，必先利其器。SmartRocket Modeler提供了涵盖11个大类、超过66个精心设计的图形化构件，全面对标国际主流工具SCADE Suite的建模算子，能够满足各种复杂嵌入式系统的建模需求。

✦ 基础运算构件：包括数学构件（加、减、乘、除等）、比较构件（大于、小于、等于等）、逻辑构件（与、或、非等）和位构件（移位、按位与/或等），用于构建核心的算法逻辑。

✦ 数组/结构体构件：专门为处理复杂数据结构设计，如针对数组的`Concatenation`（拼接）、`Reverse`（反转）、`Transpose`（转置）构件，针对结构体的`Make`（构建）、`Flatten`（展开）构件，方便用户高效地操作和管理数据。

✦时态构件：如`Pre`（取前一周期值）、`Init`（初始化）、`FollowedBy`（延迟N个周期），是构建具有“记忆”功能的时序逻辑的基础。

✦ 状态机构件：提供完整的状态机建模支持，包括状态(State)、迁移(Transition)，并支持强迁移、弱迁移、同步迁移等多种迁移语义，以及Restart/Resume等高级属性，完美描述系统的控制流和模式切换。

✦ 高阶构件：通过高阶构件（如Map、Fold、MapFold等迭代器）和激活构件（如Boolean Activate），允许用户在更高的抽象层次上建模，实现复杂的循环、迭代和条件执行逻辑，极大地提升了建模的简洁性和表达力。

2. 灵活的建模方式

SmartRocket Modeler充分考虑了不同用户的使用习惯和复杂场景下的设计需求，提供了多种灵活的设计方式：

✦ 自顶向下与自底向上设计：支持从系统顶层开始，逐步细化分解功能模块；也支持先构建底层的基础组件，再通过组合搭建完整的系统。

✦ 图形与文本的无缝融合：

- 图形画布：是主要的建模场所，用户通过拖拽构件、绘制连线，可以直观地构建数据流图和状态机。

- 文本画布：支持在组件内部直接编写Lustre文本代码，为熟悉文本方式的用户或处理某些复杂的表达式提供了便利。图形画布可以一键转换为文本画布。

✦ 多画布设计：对于一个复杂的组件，允许创建多个图形/文本画布，通过中间变量进行逻辑连接。其作用是将复杂的模型分解为多个逻辑清晰的步骤，极大地提升了大型模型的可读性和可维护性。

3. 强大的模型管理能力

✦ 类型系统：提供强类型的建模环境，支持基本类型（int8、uint32、float64、bool等）以及用户自定义的数组(Array)、结构体(Structure)、枚举(Enum) 和基础类型别名，确保模型在数据层面上的精确性。

✦ 构件库与资产复用：

- 内置类库：工具自带多个系统类库，提供了常用的预定义组件。

- 用户类库：用户可以将自己开发的、经过验证的模块作为私有类库在多个项目中轻松复用，实现知识和资产的沉淀。

✦ SCADE模型迁移：支持一键导入SCADE Suite的模型文件（.etp格式），并能将Modeler项目导出为SCADE兼容格式，实现了与现有开发生态的无缝衔接，有效保护历史资产。

05

总 结

图形化建模是SmartRocket Modeler的核心价值所在。它不仅仅是一个画图工具，更是一个基于严格形式化语义的设计与思考平台。通过提供丰富而精确的建模元素、灵活的设计方式以及强大的模型管理能力，SmartRocket Modeler帮助工程师将错综复杂的嵌入式软件需求，转化为清晰、无二义性、可验证、可执行的模型。

这标志着软件开发的重心，从难以捉摸的文档和易错的手工编码，转移到了精确、直观的模型之上。它为后续的静态分析、模拟仿真、形式化验证和自动化代码生成奠定了坚实的基础，是打造高可信、高安全嵌入式控制软件的不二之选。

在接下来的推送中，我们将继续深入探索SmartRocket Modeler的其他关键功能，如静态分析与验证，敬请期待。

审核编辑 黄宇