当前位置：首页 > news >正文

Lustre/Scade 语言时序算子与形式化验证的联系

news 来源：原创 2025/4/29 15:36:21

在巴黎高师同步反应式系统的第一课中，描述时序算子特性的过程中，讨论到了 Lustre/Scade 语言时序算子与形式化验证方法之间的联系。

在 Lustre/Scade 中，程序的时序逻辑性质(temporal property)可以由Lustre 程序本身描述，而不需要引入新的时序逻辑去表达。在 Lustre/Scade 语言中，有同步观察(Synchronous Observer)的概念。其逻辑如下

node check(x: t) returns (ok: bool);
letassert H(x,y);y = F(x);ok = P(x,y);
tel;

assert H(x,y) 描述对程序环境的假设，如果 y = F(x)的话，则x与y的之间的性质 P(x,y)成立。该程序的描述的逻辑的意义为，只要假设H(x,y) 成立，则性质P(x,y)总成立。

在Lustre程序中，通过Lustre描述的时序性质，可使用模型检查检查工具 lesar, kind 2 等进行验证。

一些时序性质例子

连续两个`true`的情况始终不能发生

该时序性质可以用如下 Lustre 程序表达

node never_twice(A: bool) returns (OK: bool);
letOK = true -> (A and pre A);
tel;

在首周期，不可能出现连续两次true，因此性质为true。在往后周期中，当前周期值，与上一周期值不能同时为 true。如此，通过Lustre时序算子->，构造了该时序性质。

任何事件A的发生，都需要跟随着B发生，B发生在C之前

如下的时序逻辑能描述该性质

-- 在`implies` 中，只要A不发生，不论B是否发生，结果都为`true`。如果A发生了，则B必须发生，才能使`implies`为true。
node implies(A, B: bool) returns (OK: bool);
letOK = not(A) and B;
tel;-- 在 `once` 中，只要出现过一次A 发生(ture)，则`once`始终为 true。
node once(A: bool) returns (OK: bool);
letOK = A -> A or pre OK;
tel;node followed_by(A, B: bool) returns (OK: bool);
letOK = implies(B, once(A));
tel;

followed_by(A, B) and followed_by(B, C) 可描述该时序性质。