Lesar: 面向 Lustre/Scade 语言的形式化模型检测工具

在《同步反应式系统》的第一课中，介绍了同步数据流语言 Lustre 生态中的形式化模型检查器 Lesar 的用法。Lesar 可对 lustre v4 语言以及 Scade 语言中部分数据流核心特性进行模型检查。

Lesar 介绍

Lesar 是 Verimag 研发维护的形式化方法模型检查工具。该工具的理论基础基于抽象解释（abstract interpretation）和固定点计算（fixpoint computation），主要用于检查系统是否满足特定的时序逻辑性质，如安全性和活性等。

Lesar 的主要功能包括：

• 状态空间构建：从 Lustre 程序构建状态空间转移系统（transition system）。
• 模型检查：自动验证是否满足指定的逻辑公式，通常为安全性属性（如 invariants）。
• 属性验证：使用布尔逻辑或时序逻辑表达式；可以验证如“某个变量永远不会为某值”或“某个条件一旦成立，之后总保持”等性质。
• 反例生成：若属性不满足，Lesar 会生成反例（counterexample），帮助调试。

Lesar 的下载与部署

Lesar 可在 Verimag 官方网站下载，对面向 Ubuntu 22.04 平台的部署包，也可通过这里下载 lustre-v4-IV.2024.144-linux64.tgz。

在 Linux 环境或 WSL 环境中，解压压缩包

tar zxf lustre-v4-IV.2024.144-linux64.tgz

参考 README, 在 ~/.bashrc 中，添加

export LUSTRE_INSTALL=/[path_to_your_dir]/lustre-v4-IV.2024.144
source $LUSTRE_INSTALL/setenv.sh

通过 source ~/.bashrc 后，lesar 可通过 which lesar 找到。

使用示范

这里将通过示例演示 Lesar 工具的使用。假设有如下两段 Lustre 程序：

-- in F.lus 
node SWITCH1 (set, reset, initial: bool) returns (level: bool);
letlevel = initial -> if set then trueelse if reset then falseelse pre(level);
tel

以及

-- in F.lus 
node SWITCH (set, reset, initial: bool) returns (level: bool);
letlevel = initial -> if set and not pre(level) then trueelse if reset then falseelse pre(level);
tel

在 SWITCH1 中，输入set 激活将使输出 level 为 true；reset 激活将使输出为 false；其他情况输出level 保持之前周期的值。

在 SWITCH 中，拓展了 SWITCH1 的适用范围，可通过一个按钮即可控制 level 的变化。与 SWITCh1 的区别为，当set激活，并且之前level 为false 时，才会触发 level 为 true。

通过观察可知，当set 与 reset 不同时为 true 时，SWITCH 与 SWITCH1 行为一致。

如何验证？可通过 Lesar 实现。增加如下 Lustre 程序:

-- in F.lus 
node verif_switch(set, reset, initial: bool) returns (ok: bool);
var level, level1: bool;
letlevel = SWITCH(set, reset, initial);level1 = SWITCH1(set, reset, initial);ok = (level = level1);assert not(set and reset);
tel

我们注意到，模型检查的验证程序，是使用同编程语言相同的Lustre所写，而不用引入新的语言编写性质。这段 lustre v4 程序描述的含义为当 not(set and reset) 总为真时，SWITCH 与 SWITCH1 的结果相同。使用 lesar 进行验证的方法如下

lesar F.lus verif_switch 

回显结果为

--FILE=F.lus MAIN=verif_switch
--Pollux Version 2.53
Var::GlobalName symb=set printag=12 prefix='' return=set
Var::GlobalName symb=reset printag=13 prefix='' return=reset
Var::GlobalName symb=initial printag=14 prefix='' return=initial
Var::GlobalName symb=ok printag=15 prefix='' return=ok
Var::GlobalName symb=level printag=16 prefix='' return=level
Var::GlobalName symb=level1 printag=17 prefix='' return=level1
Var::GlobalName symb=set printag=12 prefix='' return=set
Var::GlobalName symb=reset printag=13 prefix='' return=reset
Var::GlobalName symb=ok printag=15 prefix='' return=ok
Var::GlobalName symb=level printag=16 prefix='' return=level
Var::GlobalName symb=level1 printag=17 prefix='' return=level1
Var::GlobalName symb=level printag=16 prefix='' return=level
Var::GlobalName symb=initial printag=14 prefix='' return=initial
Var::GlobalName symb=set printag=12 prefix='' return=set
Var::GlobalName symb=level printag=16 prefix='' return=level
Var::GlobalName symb=reset printag=13 prefix='' return=reset
Var::GlobalName symb=level printag=16 prefix='' return=level
Var::GlobalName symb=level1 printag=17 prefix='' return=level1
Var::GlobalName symb=initial printag=14 prefix='' return=initial
Var::GlobalName symb=set printag=12 prefix='' return=set
Var::GlobalName symb=reset printag=13 prefix='' return=reset
Var::GlobalName symb=level1 printag=17 prefix='' return=level1TRUE PROPERTY

注意到验证通过 TRUE PROPERTY。