Simulink模型转换为UPPAAL模型(2016)
在CoCoSim中，提到支持将Simulink模型转换为Lustre模型。Simulink模型，还能转换为为其他模型检测工具的模型，比如下面提到的UPPAAL模型。
MATLAB/Simulink 作为汽车系统建模的主流工具，虽能通过仿真助力开发，但在复杂系统的形式化验证上仍有局限。而 UPPAAL 统计模型检查器在随机混合系统分析上的优势，为解决这一难题提供了新路径。下面将介绍2016年一项Simulink模型转换为UPPAAL模型的工作。
参考
详细内容，可参考Filipovikj, Predrag & Marinescu, Raluca & Seceleanu, Cristina & Ljungkrantz, Oscar & Lönn, Henrik. (2016). Simulink to UPPAAL Statistical Model Checker: Analyzing Automotive Industrial Systems. 9995. 748-756. 10.1007/978-3-319-48989-6_46. 。
为什么要做 Simulink 到 UPPAAL 的模型转换？
Simulink本身已具备验证能力（如 Simulink Design Verifier，SDV）。但SDV在可扩展性和需求覆盖方面存在不足。相比之下，UPPAAL SMC的优势能弥补这些不足：
-
支持随机混合自动机网络建模，能同时刻画连续时间行为、离散逻辑和随机特性。
-
基于统计模型检查，可高效分析大型模型。
-
支持概率化查询。
Simulink转换为UPPAAL
工作提出了模式化转换与执行顺序保障”方案，换过程中保留Simulink的执行语义，如块的执行顺序、输入输出逻辑，同时适配 UPPAAL的stochastic timed/hybrid automata模型。
从块到自动机的语义映射
Simulink模型的组成是Block，每个块可视为一个原子动态系统；而UPPAAL的组成是自动机网络，每个自动机通过状态、迁移、变量刻画行为。转换是将Simulink块的语义映射到UPPAAL自动机的数学定义上。
分类型设计自动机模式
Simulink块主要分为离散时间块和连续时间块，两者的行为特性差异较大，因此工作设计了两种不同的自动机模式。
（1）离散时间块的自动机模式
离散块的作用是按固定采样时间执行计算，其自动机包含3个状态：
- Start（初始状态）：块初始化，加载参数。
- Offset（延迟状态）：通过局部时钟t模拟采样间隔，当t达到ts时，触发迁移到 Operate 状态；
- Operate（运行状态）：执行块的核心计算逻辑，输出结果后，重置局部时钟t，回到Offset状态，进入下一个采样周期。
此外，模式中引入全局时钟记录仿真时间，通过执行顺序编号与块间到达时间计算自动机的启动时间，确保与Simulink的执行节奏一致。
（2）连续时间块的自动机模式
连续块的作用是实时无间断执行，其模式与离散块的关键区别在Operate状态。不依赖固定采样时间，而是通过指数速率刻画连续行为。
连续变量的演化通过UPPAAL的延迟函数F定义，如模拟微分方程，而非离散块的周期性更新。
两种模式的统一设计，确保了无论Simulink块是离散还是连续类型，都能被UPPAAL自动机刻画。
Simulink的执行顺序不变
Simulink在仿真时，会通过slist函数生成块的执行顺序，编号越小，优先级越高，这直接影响系统的行为正确性。如果转换后UPPAAL自动机的执行顺序错乱，整个模型的语义会完全失真。
论文通过两个手段解决这一问题：
（1）自动展平子系统，生成原子块的全局执行顺序
Simulink模型常包含嵌套的子系统，论文设计了展平算法，递归解析slist输出，将嵌套子系统中的原子块提取出来，并赋予全局唯一的执行顺序编号。确保无论块嵌套多少层，都能明确其在整个模型中的执行优先级。
（2）在UPPAAL中通过同步机制强制执行顺序
转换后的UPPAAL自动机网络中，通过以下规则保障执行顺序：
- 初始化阶段：按执行顺序编号依次启动自动机，编号小的先初始化；
- 运行阶段：当多个自动机同时满足执行条件时，通过执行顺序仲裁，优先触发编号小的自动机；
- 数据完整性：针对RateTransition块单独设计转换逻辑，避免因执行顺序导致的数据读写冲突。