中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http://lcs.ios.ac.cn/~zwh/ 模型检测 – 例子 中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http://lcs.ios.ac.cn/~zwh/

程序正确的重要性 应用广泛 软件错误的可能后果 航空 航天 金融 设备的控制 日常生活 火箭 Ariane 5 Explosion (1997) 火星气候轨道器 NASA Mars Climate Orbiter (1999)

程序正确性方法 测试 形式验证 黑盒测试 白盒测试 推理验证 模型检测 可执行代码 程序代码 程序代码或其抽象模型 程序运行环境模型 规则 算法

例子: ISR ./isr INFO: system is now active N: 2 RESULT: 1 N: 10 #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { ./isr INFO: system is now active N: 2 RESULT: 1   N: 10 RESULT: 3 N: 20 RESULT: 4 N: 30 INFO: the input number must be in {0,...,20} N: 5 RESULT: 2 N:

例子: ISR 输入为0和20之间的整数时， 输出为其平方根的整数部分。 对ISR的要求: 输入为0和20之间的整数时， #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { 对ISR的要求: 输入为0和20之间的整数时， 输出为其平方根的整数部分。 输入为0和20之间的整数时， 输出为其平方根的整数部分。

测试 黑盒测试 白盒测试 Program testing can be used to show the presence of bugs, but never to show their absence! -- Edsger W. Dijkstra

形式验证 推理验证 模型检测 正确性 正确性+不正确性

例子: ISR 对ISR的要求: (at line 18):((m*m)<=n)&&((m*m)+2*m+1>n) #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); m=isr(n,k); k=isk(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { 对ISR的要求: (at line 18):((m*m)<=n)&&((m*m)+2*m+1>n)

程序的模型检测(例子)

模型检测 ./verds –c isr.c –sp isr.sp 验证结果 反例

验证过程 Automatic Translator C Program Model VERDS Model Checker Specification Negative Conclusion Error Trace

反例分析 以下输入产生不正确结果 1 3 5 7 9 11 13 15 17 19 0 2 4 6 8 10 12 14 16 18 4 不正确运行

修正后的例子: ISR2 ./isr2 INFO: system is now active N: 2 RESULT: 1 N: 10 #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { ./isr2 INFO: system is now active N: 2 RESULT: 1   N: 10 RESULT: 3 N: 20 RESULT: 4 N: 30 INFO: the input number must be in {0,...,20} N: 5 RESULT: 2 N:

模型检测 ./verds –c isr2.c –sp isr.sp 验证结果

验证过程 Automatic Translator C Program Model VERDS Model Checker Specification Positive Conclusion

模型检测的缺点与优点 缺点 可直接验证的程序规模小 可直接验证的程序结构简单 优点: 自动验证 对不正确的程序可生成诊断信息

形式验证 推理验证 模型检测 推理验证与模型检测相结合

推理验证+模型检测 int in() { char c=0; int k=0; while (1) { k=0; … #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int in() { char c=0; int k=0;   while (1) { k=0; … if (c=='\n') { return k; } return k; } k>=0; k<=20; 不可达 k>=0; k<=20;

推理验证+模型检测 int in() FUNCTION r=in() { ASSUMPTION TRUE; char c=0; #include <stdio.h> /**************************************************/ int in(); int isr(int x,int k); int isk(int n,int k); int main() { int n=0; int m=0; int k=1; printf("INFO: system is now active\n"); while (1) { n=in(); k=isk(n,k); m=isr(n,k); printf("RESULT: %i\n\n",m); } int isr(int x,int k) int y1=0; int y2=0; int y3=0; y1=0; y2=1; y3=1; if (x==2||(x>2&&k==20)) x=x-1; while (y3<=x) { y1=y1+1; y2=y2+2; y3=y3+y2; return y1; int isk(int n,int k) if (k!=20) { if (k!=n) k=21; else if (k==19) k=0; else k=k+2; } else { k=21; return k; int in() char c=0; int k=0; k=0; putc('N',stdout); putc(':',stdout); putc(9,stdout); c=getc(stdin); if (c=='\n') { printf("INFO: the input must be 1 or 2 digits\n\n"); continue; if (c<'0'||c>'9') { if (c=='\n') break; k=c-'0'; if (c=='\n') { return k; } if (k<2) k=k*10+(c-'0'); else if (k==2&&c=='0') k=20; else { printf("INFO: the input number must be in {0,...,20}\n\n "); if (c!='\n') { int in() { char c=0; int k=0;   while (1) { k=0; … if (c=='\n') { return k; } return k; } FUNCTION r=in() ASSUMPTION TRUE; GUARANTEE r>=0&&r<=20; k>=0; k<=20; 不可达 k>=0; k<=20;

模型检测 时间优势对比: Time Time (with A/G) Model Checking 1233 205 ./verds –c isr.c –sp isr.sp –fsp isr.fsp 时间优势对比: 验证结果 Time Time (with A/G) Model Checking 1233 205

验证过程 http://lcs.ios.ac.cn/~zwh/verds/ Automatic Translator C Program Model VERDS Model Checker Specification Function Specification Positive Conclusion http://lcs.ios.ac.cn/~zwh/verds/

并发模型的模型检测(例子)

并发模型的模型检测(例子) a=s0 b=t0 x=0 y=0 t=0

并发模型的模型检测 建模 验证问题 Model

并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

并发模型(进程模块说明1) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1);

并发模型(进程模块说明2) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1);

模型检测 ./verds -ck 1 me002.vvm VERSION: verds 1.42 - DEC 2012 FILE: me001.vvm PROPERTY: A G ! ((a = 2 )& (b = 2 )) bound = 1 time = 0 ---------- time = 0 bound = 2 time = 0 bound = 3 time = 0 bound = 4 time = 0 bound = 5 time = 0 bound = 6 time = 0 CONCLUSION: TRUE (time=0)

模型检测结论 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))) 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)))

进程公平性说明

并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

并发模型(进程模块说明1a) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1); FAIRNESS running;

并发模型(进程模块说明2a) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1); FAIRNESS running;

模型检测结论 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)))

进程公平性说明2

并发模型(主程序) VVM VAR x: 0..1; y: 0..1; t: 0..1; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2&p1.b=t2)); AG((!p0.a=s1|AF(p0.a=s2|p1.b=t2))&(!p1.b=t1|AF(p0.a=s2|p1.b=t2))); AG((!p0.a=s1|AF(p0.a=s2))&(!p1.b=t1|AF(p1.b=t2))); AG((!p0.a=s1|EF(p0.a=s2))&(!p1.b=t1|EF(p1.b=t2)));

并发模型(进程模块说明1b) MODULE p0m() VAR a: {s0,s1,s2,s3}; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1&(x=0|t=0): (a):=(s2); a=s1&!(x=0|t=0): (a):=(s1); a=s2: (y,a):=(0,s3); a=s2: (a):=(s2); a=s3: (y,t,a):=(1,1,s1); FAIRNESS running; a!=s2;

并发模型(进程模块说明2b) MODULE p1m() VAR b: {t0,t1,t2,t3}; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1&(y=0|t=1): (b):=(t2); b=t1&!(y=0|t=1): (b):=(t1); b=t2: (x,b):=(0,t3); b=t2: (b):=(t2); b=t3: (x,t,b):=(1,0,t1); FAIRNESS running; b!=t2;

模型检测结论 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))) AG((!p0.a=1|EF(p0.a=2))&(!p1.a=1|EF(p1.a=2)))

验证过程 http://lcs.ios.ac.cn/~zwh/verds/ 建模 验证问题 Model VERDS Model Checker Positive Conclusion Negative Conclusion 安全性质 Error Trace http://lcs.ios.ac.cn/~zwh/verds/

模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的模型 建立新方法 改建算法以增加可应用性 与其他方法结合以增加可应用性

模型检测的学习与研究 学习 应用 研究 原理 相关知识 将其应用于一些简单程序 将其应用于不同类型的模型 建立新方法 改建算法以增加可应用性 与其他方法结合以增加可应用性 符号模型检测 限界模型检测 硬件/协议/软件 实时系统模型 概率系统模型 混成系统 抽象方法 反例制导抽象求精 偏序归约 对称技术 组合方法 推理方法

问题?