Engee中形式化验证的基本示例
本文提供了形式化模型验证的基本示例，演示了Ltl规范在Spin中的实际使用以及所获得结果的解释。
例子1
座 Chart 模型 promela_a.engee包含单个状态 A.
找出状态是否为活动状态 A 或者不是，可以通过全局变量的值。 promela_a_S.Chart.state.a.is_active 在生成的文件中 promela_a.pml.
*Chart*的活动也可以通过全局变量的值来判断 promela_a_S.Chart.state.is_active.
使用预处理器，我们将为这些变量分配缩写别名，以便在规范的公式中使用。:
#define a promela_a_S.Chart.state.A.is_active
#define chart promela_a_S.Chart.state.is_active我们会把它们和规格一起添加。:
// состояние "A" не активно в начальный момент времени:
ltl spec1 { !a }
// состояние "A" обязано стать активным в начальный момент времени или когда-нибудь в будущем:
ltl spec2 { <>a }
// блок Chart не активен в начальный момент времени:
ltl spec3 { !chart }
// активность состояния "A" и блока Chart изменяется синхронно:
ltl spec4 { [] (chart == a) }到文件末尾 promela_a.pml.
我们将验证规格:
$ spin -run -ltl spec1 promela_a.pml 2>&1 | grep errors:
State-vector 40 byte, depth reached 0, errors: 0
$ spin -run -ltl spec2 promela_a.pml 2>&1 | grep errors:
State-vector 40 byte, depth reached 6, errors: 0
$ spin -run -ltl spec3 promela_a.pml 2>&1 | grep errors:
State-vector 40 byte, depth reached 0, errors: 0
$ spin -run -ltl spec4 promela_a.pml 2>&1 | grep errors:
State-vector 40 byte, depth reached 12, errors: 0*Spin*程序的控制台输出显示正在满足每个规范-验证成功。
例子2
模型 abcpq.engee图中有三个特点:
-
无尽的循环
P→Q→P→ …; -
不可达的状态
C; -
死锁情况
B.
让我们尝试验证这些语句。
像往常一样，我们将为决定我们状态活动的变量声明缩写别名。 为此，请添加到文件中 abcpq。pml,pml 预处理器的宏部分:
#define a abcpq_S.Chart.state.A.is_active
#define b abcpq_S.Chart.state.B.is_active
#define c abcpq_S.Chart.state.C.is_active
#define p abcpq_S.Chart.state.B.P.is_active
#define q abcpq_S.Chart.state.B.Q.is_active指定状态的不可达性 C 您可以使用公式"永远不要 `C`"，其中的验证，如预期的那样，是成功的:
ltl spec1 { []!c } // состояние C недостижимо此规范可以被认为是*安全*（safety）的属性 □p 对于公式 p，禁止条件 C 激活（即 p=C).
但是，如果您替换上面公式中的名称 c 上 q:
ltl absurd2 { []!q } // утверждается (неверно), что Q никогда не станет активным修改后的公式的验证预计会导致错误，因为它最初是显而易见的条件 Q 可实现的:
$ spin -run -ltl absurd2 abcpq.pml
pan: ltl formula absurd2
pan:1: assertion violated !( !( !(abcpq_S.Chart.state.B.Q.is_active))) (at depth 49)
pan: wrote abcpq.pml.trail
...
State-vector 64 byte, depth reached 49, errors: 1
...从跟踪文件中获取的反例:
$ spin -t -p -k abcpq.pml.trail abcpq.pml我应该在哪里注意指示赋值的字符串，根据规范，不应该是:
42: proc 0 (fsm:1) abcpq.pml:114 (state 34) [abcpq_S.Chart.state.B.Q.is_active = 1]和跟踪末尾具有与规范相矛盾的变量值的字符串。:
abcpq_S.Chart.state.B.Q.is_active = 1现在让我们检查*liveness*（liveness）的属性-需要变得活跃:
ltl absurd3 { <>c } // утверждается, что C рано или поздно станет активным核实结果:
$ spin -run -ltl absurd3 abcpq.pml
...
pan: ltl formula absurd3
pan:1: acceptance cycle (at depth 31)
pan: wrote abcpq.pml.trail
...
State-vector 56 byte, depth reached 65, errors: 1
...在这里，调查路线是无效的：反例显然是无止境的。
这里是活泼的属性 ◊A∧ ◊_BP_PQ_Q 其余状态验证成功。:
ltl spec4 { (<>a) && (<>b) && (<>p) && (<>q) } // свойство живости состояний A, B, P и Q您还可以使用LTL来验证*公平性*属性。 □□P 或 □□Q 也就是说，要求事件（P或Q的激活）将无限频繁地发生:
ltl spec5 { []<>p } // свойство справедливости P
ltl spec6 { []<>q } // свойство справедливости Q和*稳定*属性(稳定) □□B -某些事件（死锁b活动）迟早会永远发生的要求:
ltl spec7 { <>[]b } // свойство стабилизации B使用含义和排他性"或"，可以指定父状态和子状态的活动相关性。:
ltl spec8 { [](b -> (p ^ q)) } // если активно родительское состояние, то активно и одно из дочерних可以使用等价关系而不是暗示。:
ltl spec9 { [](b <-> (p ^ q)) } // родительское состояние активно тогда и только тогда, когда активно одно из дочерних结合含义和操作符 下一个，您可以确保活动状态 P 和 Q 以1步的频率振荡:
ltl spec10 { []((p -> X q) && (q -> X p)) } // за активацией состояния P всегда следует активация Q и наоборот示例3
让我们考虑另一个简单的模型 link:/helpcenter/stable/_next/static/media/ab.engee[ab．在直接模拟模式下，对其属性的验证可能需要相当长的时间，而对相同属性的形式化验证几乎是立即进行的。
国家之间的过渡 A 和 B 在变量之后执行 i 它将增加十亿倍。
让我们宣布缩写名称:
#define chart ab_S.Chart.state.is_active
#define a ab_S.Chart.state.A.is_active
#define b ab_S.Chart.state.B.is_active
#define i ab_S.Chart.locals.i
#define x ab_S.Chart.output.x
#define y ab_S.Chart.output.y一个验证国家之间强制过渡事实的公式 A 和 B 在未来的某个时候:
ltl spec1 { <>(a -> X b) }让我们确保这种转换不可能在每一步都发生;更强大的规范会导致错误。:
ltl absurd2 { [](a -> X b) } // неверно!操作员 直到 它也正在"未来某个时候"成功验证。:
ltl spec3 { <>(a U b) }鉴于运算符在激活*Chart*块后立即变为true，因此可以更严格地编写:
ltl spec4 { [](!chart || (a U b)) }或等价物，但更短:
ltl spec5 { [](chart -> (a U b)) }较弱的形式也被成功验证。:
ltl spec6 { [](chart -> (a W b)) }和"解放"运算符（发行版）导致错误，因为状态 A 和 B 它们不能在同一时间处于活动状态:
ltl absurd7 { [](chart -> (a V b)) } // неверно!让我们使用*Chart块的输出变量的值来检查相同的属性。* x 和 y，最初安装于 错误:
ltl spec8 { <>(y U x) }
ltl spec9 { [](chart -> (y U x)) }
ltl spec10 { [](chart -> (y W x)) }
ltl absurd11 { [](chart -> (y V x)) } // неверно!最后，让我们检查变量的值范围。 i.
在初始时刻，变量的值 i 同样 0:
ltl spec12 { i == 0 }意义 i 它总是在范围内 [0..1000000001]:
ltl spec13 { [](0 <= i && i <= 1000000001) }永远 i 取其最大值 1000000001:
ltl spec14 { <>(i == 1000000001) }