模型验证器VERDS Wenhui Zhang 31 MAY 2011.

Presentation on theme: "模型验证器VERDS Wenhui Zhang 31 MAY 2011."— Presentation transcript:

1 模型验证器VERDS Wenhui Zhang 31 MAY 2011

2 内容 模型验证器VERDS 模型 性质 VERDS验证方法 模型检测/隐式状态/TBD 模型检测/限界语义/CTL限界语义/QBF

3 模型 System level specification Module specification Keywords: VVM
VAR INIT PROC FAIRNESS SPEC MODULE TRANS System level specification name of the system model (optional), global variables, Initial values of the global variables, processes , fairness constraints (optional), and properties (optional). Module specification name and the parameters of the module, local variables, initial values of the local variables, transition rules, Fairness constraints (optional), and

4 例子：互斥协议

5 例子：互斥协议 迁移系统 VVM me005 VAR x[0..1]:0..1; t:0..1;
INIT x[0]=0; x[1]=0; t=0; PROC p0:p0m(x[],t,0); p1:p0m(x[],t,1); SPEC AG(!(p0.a=s2&p1.a=s2)); AG((!p0.a=s1|AF(p0.a=s2|p1.a=s2))& (!p1.a=s1|AF(p0.a=s2|p1.a=s2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.a=s1|AF(p1.a=s2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.a=s1|EF(p1.a=s2)));

6 例子：互斥协议 模块 MODULE p0m(x[],t,i) VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS
a= s0: (x[1-i],t,a):=(1,1-i,s1); a=s1&(x[i]=0|t=i): (a):=(s2); a=s1&!(x[i]=0|t=i): (a):=(s1); a=s2: (x[1-i],a):=(0,s3); a=s2: (a):=(s2); a=s3: (x[1-i],t,a):=(1,1-i,s1); FAIRNESS running;

7 性质描述语言 Computation Tree Logic p p pq AX p EX p pq AF p EF p pq
AG p A (p U q) A (p R q) EX p EF p EG p E (p U q) E (p R q)

8 例子：互斥协议 性质 AG(!(p0.a=s2&p1.a=s2)) AG((!p0.a=s1|AF(p0.a=s2|p1.a=s2))& (!p1.a=s1|AF(p0.a=s2|p1.a=s2))) AG((!p0.a=s1|AF(p0.a=s2))&(!p1.a=s1|AF(p1.a=s2))) AG((!p0.a=s1|EF(p0.a=s2))&(!p1.a=s1|EF(p1.a=s2)))

9 VERDS验证方法 模型检测 隐式状态/TBD 限界语义/CTL限界语义/QBF

10 隐式状态 Kripke结构M= (S,T,I,L) 状态 状态集 公式/BDD/TBD
时序逻辑公式 状态集[[]] 公式F([[]]) M |=  即 I  [[]] 即 F(I)F([[]])

11 时序逻辑公式 公式 s  (v1,v2,…,vn) p [[p]]  F[[p]]  p

12 Fairness Fair Constraints f1,…,fk f [[f]]  F[[f]]  f

13 公式/TBD

14 验证运行情况

15 Verification Results Property Conclusion AG(!(p0.a=2&p1.a=2)) true
AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) false AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

16 Verification Results Property Conclusion AG(!(p0.a=2&p1.a=2)) true
AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) with the additional fairness constraint (a!=s2) in the module p0m() AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

17 限界语义 Kripke结构 M= (S,T,I,L) 限界模型 Mk= (S, Phk,I,L) Mk,s|=b  则 M,s |= 
Mk,s |=b  则 M,s |=  即 M,s |= 

18 CTL限界语义 M,s |=  当且仅当 存在 k 使得 Mk,s|= 

19 CTL限界语义的QBF刻画 Mk,s|=  当且仅当 [[,v(s)]]k 成立

20 CTL限界语义模型检测 给定Kripke结构 M和CTL公式。 0. k=0；
1. 若 v.(I(v )[[,v]]k) 成立，则 M|= ； 2. 若 v.(I(v )[[,v]]k)成立，则 M|=  ； 3. k=k+1，返回到1。

21 ACTL限界语义的SAT刻画

22 QBF/SAT-Solver

23 验证运行情况

24 Verification Results Property (without Fairness) Conclusion
AG(!(p0.a=2&p1.a=2)) true AG((!p0.a=1|AF(p0.a=2|p1.a=2))&(!p1.a=1|AF(p0.a=2|p1.a=2))) false AG((!p0.a=1|AF(p0.a=2))&(!p1.a=1|AF(p1.a=2))) AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

25 工具网页 工具和网页都尚在发展和完善中