Simulink模型转NuSMV模型（2006）
在CoCoSim中，提到其中的步骤之一为将Simulink模型转为Lustre模型。对Simulink模型进行模型检查，还可以将Simulink模型转换为其他模型检测工具的模型，比如下面即将提到的NuSMV模型。
2006年，Honeywell团队设计了将Simulink模型翻译成模型检测工具NuSMV的输入模型的工作。
参考
详细内容，可参考Meenakshi B, Abhishek Bhatnagar, and Sudeepa Roy. "Tool for Translating Simulink Models into Input Language of a Model Checker." In IEEE International Conference on Formal Engineering Methods, 2006.
为什么要把Simulink模型转成NuSMV模型？
航空电子软件须满足DO-178C标准，标准鼓励用形式化方法。工程师熟悉Simulink的框图逻辑，但NuSMV等模型检测工具需要用专有模块化语言描述系统。要验证 Simulink模型，工程师得手动把框图翻译成NuSMV模型。
NuSMV是一种自由软件形式发布的符号模型检测器，能基于CTL/LTL时序逻辑公式验证系统是否满足需求。NuSMV用二进制决策图（BDD）压缩状态空间，能处理多组件交互场景，同时NuSMV擅长处理离散系统。
Simulink转NuSMV
Honeywell团队提出的转换算法，目的是结构化映射与语义保持，既要把Simulink的每个模块对应到NuSMV的模块，还要确保两者行为一致。
支持的Simulink模块范围
不是所有Simulink模块都能转，转换器只支持能构成有限状态机的离散模块。核心支持的模块库包括：
- 信号路由：多路复用器（Mux）、解复用器（Demux）、开关（Switch）；
- 逻辑运算：关系运算符（≤、≥）、逻辑与 / 或、区间检测；
- 数学运算：加减乘除、绝对值、最大值 / 最小值（离散型）；
- 离散模块：单位延迟（Unit Delay）、整数延迟、计数器；
- 源与sink：常数、输入端口、输出端口、文件读取
这些模块覆盖了常见控制逻辑（比如传感器数据处理、故障判断），而连续模块因NuSMV不支持暂未纳入。
从Simulink的MDL文件到NuSMV模型
转换器的输入是Simulink模型的MDL文件，输出是可直接运行的NuSMV代码。整个过程分三步：
第一步：解析MDL文件，提取有效信息。
MDL文件中包含很多无用信息，比如模块颜色、字体大小，第一步要做的就是过滤和结构化。丢弃图形相关数据，保留模块类型、输入输出端口、变量名、连接关系，把Simulink的层级结构转化为树状图，方便后续处理。
第二步：计算模块输入类型，解决类型匹配问题。
Simulink模块是通用的，但NuSMV的模块是强类型的。所以第二步需要确定每个模块的输入类型。从源模块（如常数、输入端口）开始，反向推导所有模块的输入类型。比如常数模块输出是标量，那么它连接的加法模块的一个输入就是标量。
处理子系统：先解析子系统内部的模块类型，再推导子系统外部的连接类型。
终止条件：所有模块的输入类型都确定。
例子：如果Simulink的关系运算符模块输入1是长度为2的向量，输入2是标量，运算类型是≤，那么NuSMV会生成一个对应的模块：
MODULE relational_operator_2(in1, in2)
VARout : array 0..1 of boolean;
ASSIGNout[0] := in1[0] <= in2;out[1] := in1[1] <= in2;
第三步：生成NuSMV代码，保留层级结构。
最后一步是组装：用第二步确定的模块类型，调用预定义的模块生成库，输出完整的NuSMV模型。Simulink的子系统对应NuSMV的子模块。Simulink的变量名在NuSMV中保留。模块间的连接关系与Simulink一致。
比如Simulink的单位延迟模块，会对应NuSMV中一个包含状态变量的模块，确保语义一致：
MODULE unit_delay(in)
VARout : integer;
ASSIGNnext(out) := in;
解决状态爆炸问题所作的优化
模型检测中的挑战是状态爆炸，模块越多，状态数呈指数增长。转换器提供了一个实用的优化，即变量范围绑定。工程师可以手动指定某些变量的取值范围，转换器会将这些范围写入NuSMV代码，限制状态空间大小。
反向翻译：从NuSMV反例到Simulink轨迹
当NuSMV发现某个需求不满足，会生成一条反例轨迹。转换器的反向翻译功能会把NuSMV的变量名映射回Simulink的模块输出，并把步骤对应到Simulink的采样时间，再
生成文本报告，工程师能在Simulink中复现这个场景，定位问题。