CoCoSim(2020): 连接Simulink与Lustre生态的模型检测框架

github中，CoCoSim项目提供了基于契约的Simulink模型组合验证。这里将介绍CoCoSim框架。

在高安全领域，系统的开发往往采用模型驱动设计，Simulink/Stateflow凭借直观的图形化建模能力和丰富的工具链支持，成为行业内的主流选择。然而，随着系统复杂度提升，如何确保模型从需求到代码的语义一致性，并通过严格的形式化验证排查潜在风险，成为开发过程中的关键挑战。

CoCoSim框架作为一款开源工具，它不仅能实现Simulink/Stateflow模型到同步编程语言Lustre的语义转换，还能集成Kind 2等形式化模型检查工具，打通 “建模-转换-验证” 的全流程。

CoCoSim ：连接Simulink与同步编程生态

CoCoSim提供了Simulink与同步编程生态之间的桥梁：​

• 语义转换：将Simulink/Stateflow模型转换为等价的Lustre代码；​
• 全流程工具集成：不仅支持模型转换，还整合了形式化验证（如Kind 2）、代码生成（如LustreC生成C/Rust代码）、测试用例生成（如LustreT）等工具；​
• 开源与可扩展：作为开源框架，CoCoSim支持用户通过API自定义转换规则和工具链，适配不同领域的需求。

CoCoSim的功能架构如下

Simulink到Lustre的语义转换

CoCoSim对Simulink模型的转换并非语法映射，而是基于形式化语义分析，确保转换后的Lustre代码与原模型行为一致。过程主要分为三个关键步骤:

模型预处理

Simulink模型中可能包含复合模块或非标准块，CoCoSim首先会对模型进行预处理：​

• 将复杂模块拆解为基础块，确保每个块的行为可被映射；​
• 区分虚拟子系统和原子子系统，保留模型的执行语义；​
• 检查模型的合法性，避免隐式语义导致的验证漏洞。

形式化语义定义：Simulink与Lustre的行为一致性

CoCoSim为Simulink的离散块子集定义了形式化语义，并与Lustre的语义建立对应关系：

• 单周期模型：Simulink中离散模型的执行基于固定时间步长，这与Lustre中基于抽象时钟的周期性计算语义匹配。CoCoSim将Simulink的每个子系统转换为Lustre的节点，每个原子块转换为Lustre的方程；​
• 多周期模型：CoCoSim通过公共基准时钟（Common Base Clock），将所有模块的周期和偏移量转换为基准时钟的整数倍，再通过Lustre的时钟算子（when、merge）实现多周期数据交互，确保语义一致性。

层次化映射：保留模型结构，提升可追溯性

为了方便后续的验证结果分析和代码调试，CoCoSim 采用层次化转换策略：​

• Simulink的每个Subsystem对应Lustre的一个Node，子系统间的信号交互对应Lustre节点的输入输出；​
• Simulink中的注释、信号名等信息会被保留到Lustre代码中，同时生成可追溯性报告，将Lustre代码的每一行与原Simulink模块关联，便于定位问题。

例如，一个包含Sum和UnitDelay的Simulink子系统，转换后的Lustre代码如下

node Simulink_Subsystem(in1: real) returns (out1: real);
var sum_val: real;
letsum_val = in1 + pre(sum_val);out1 = sum_val;
tel

集成Kind2，实现形式化模型检查

转换为Lustre代码后，CoCoSim的下一步是借助形式化验证工具排查模型中的潜在缺陷。其中，Kind2作为SMT-based模型检查工具，是CoCoSim的验证后端之一，能够验证Lustre模型的安全性、活性等属性。

CoCoSim 的其他关键能力：代码生成、测试用例生成

除了Simulink-Lustre转换和Kind 2验证，CoCoSim还支持从验证后的模型生成安全可靠的代码，形成 “建模-验证-代码生成” 的开发闭环。

代码生成：从Lustre到C/Rust的转换

• LustreC后端：将验证通过的Lustre模型转换为结构化的C代码，保留原模型的层次结构，便于后续集成到嵌入式平台；​
• Kind2的Rust代码生成：Kind2不仅能验证模型，还能直接从Lustre模型生成内存安全、并发安全的Rust代码。

测试用例生成：LustreT辅助验证完整性

CoCoSim集成的LustreT工具，可基于Lustre模型生成测试用例，补充形式化验证的覆盖范围：​

• 基于覆盖准则：如MC/DC，生成满足特定覆盖要求的测试用例，确保模型的关键逻辑被充分测试；​
• 基于变异的测试：生成变异模型，再生成能区分原模型与变异模型的测试用例，评估测试集的有效性。

参考

详细内容，可参考Hamza Bourbouh, Pierre-Loïc Garoche, Thomas Loquen, Éric Noulard, Claire Pagetti. CoCoSim, a code generation framework for control/command applications An overview of CoCoSim for multiperiodic discrete Simulink models. 10th European Congress on Embedded Real Time Software and Systems (ERTS 2020), Jan 2020, Toulouse, France. ffhal-02441334f