模型验证器VERDS Wenhui Zhang 31 MAY 2011

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

模型 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

例子：互斥协议

例子：互斥协议 迁移系统 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)));

例子：互斥协议 模块 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;

性质描述语言 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)

例子：互斥协议 性质 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)))

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

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

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

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

公式/TBD

验证运行情况

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)))

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)))

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

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

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

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。

ACTL限界语义的SAT刻画

QBF/SAT-Solver

验证运行情况

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)))

工具网页 http://lcs.ios.ac.cn/~zwh/verds/index.html 工具和网页都尚在发展和完善中