LAMA(2014): 一项对SCADE模型进行基于SMT验证的开源方案

在github上，有一项名为LAMA的IR项目LAMA。项目的目标是为SCADE程序的验证提供一种中间语言。下面将介绍这项工作。

SCADE Suite中包含了形式化验证工具Design Verifier(DV)，Basold等人想要提供开源的、针对SCADE程序的形式化验证方案，因此设计实现了LAMA。

LAMA中间语言与两级翻译流程

为搭建SCADE模型与SMT求解器之间的桥梁，提出了中间语言LAMA，并设计了从SCADE到LAMA、再从LAMA到SMT实例的两级翻译流程，实现SCADE模型的基于SMT的验证。

LAMA的架构与模块间交互描述如下

LAMA中间语言设计

LAMA的定位是将SCADE简化，同时保留利于SMT框架优化的关键特性（如结构化数据类型、自动机）。其语言结构与特性如下：​

• 程序组成：包含类型、常量、输入变量/局部变量/状态变量、节点的声明，以及全局数据流、初始化、断言和不变式。节点作为核心单元，由子节点、自身变量、局部流、初始化、自动机定义和不变式构成。​
• 自动机支持：LAMA自动机借鉴模式自动机思想，语义与SCADE安全状态机的强迁移语义一致，支持层级与并行组合，允许在不同模式下分配局部数据流，还通过默认块处理变量未显式定义的情况。​
• 类型系统：遵循Cardelli的思想，支持布尔型（bool）、整型（int）、实型（real）、有符号整型（sint[n]）、无符号整型（uint[n]）等基础类型，以及数组、乘积类型等复合类型，明确了各类型的语义范围。​
• 因果性分析：与SCADE类似，通过构建变量依赖图，检查是否存在变量求值顺序，确保程序因果性——变量当前时刻的定义不会依赖自身。

SCADE到LAMA的翻译

该翻译过程需针对SCADE的不同语言构造分别处理，核心是将SCADE算子映射为LAMA节点，并妥善处理状态相关与无关的数据流：​

• 节点实例化：SCADE每个算子实例都有独立状态存储，因此翻译时需为每个SCADE算子实例生成带有新名称的LAMA节点拷贝。​
• 状态无关数据流：SCADE中的逻辑、算术基础操作，变量、常量、数组函数及if-then-else等，在LAMA中有直接对应结构，可直接翻译；流算子（如fby）需先替换为pre和￫ (init)算子链，再根据不同情况翻译，例如对于x = M → pre N（M为常量、N无流算子），翻译为LAMA的初始化与迁移定义，非常量情况则通过自动机处理。​
• 状态相关数据流：SCADE同步状态机翻译为LAMA状态机，层级状态机通过引入子节点处理（如SCADE状态中的子状态机翻译为LAMA节点，在原状态中通过use构造调用）；强迁移直接翻译，弱迁移需特殊处理，重启迁移转化为语义一致的恢复迁移。​
• 优化措施：一是将pre算子尽可能移到表达式根部（利用非流算子的pre分配律），二是内联消除文本SCADE代码中的辅助变量，减少后续SMT实例的状态变量数量。

LAMA到SMT的翻译

翻译目标是将LAMA程序转化为SMT公式集，用于验证程序附带的不变式，核心是将LAMA节点递归翻译为Mealy机，并构建数据流对应的Mealy机：​

• 签名与公式定义：为LAMA节点的输入、输出、变量及自动机（活跃/选中模式）添加流类型符号到SMT签名；根据LAMA中的等式、状态过渡、初始化等，定义对应的SMT公式，例如等式v = M对应D_v:λn.v(n) ≡ M(n)，状态过渡s'=M对应D_s:λn.s(n+1) ≡ M(n)。​
• 自动机处理：LAMA自动机的选中模式（sel_A）通过sel_A(n+1) ≡ act_A(n)定义，初始化为初始模式；活跃模式（act_A）由act_A(n) ≡ next(sel_A,E_A)(n)确定（next函数返回当前活跃模式），变量根据活跃模式通过match函数选择对应的流定义。​
• 节点激活条件：当节点在某模式下使用时，仅该模式活跃时节点数据流才生效，激活条件公式e_N:λn.act_A(n) ≡ l（l为节点所在模式）控制节点数据流公式的启用。​
• 顶层程序翻译：LAMA顶层程序的节点声明与数据流按上述规则处理，不变式直接翻译为SMT公式。

参考

详细内容，可参考Basold, Henning & Günther, Henning & Huhn, Michaela & Milius, Stefan. (2014). An Open Alternative for SMT-Based Verification of Scade Models. 8718. 124-139. 10.1007/978-3-319-10702-8_9.