《模型检测例子》PPT课件.ppt

模型检测 例子,中国科学院软件研究所 计算机科学国家重点实验室 张文辉 /zwh/,程序正确的重要性,应用广泛 航空 航天 金融 设备的控制 日常生活 软件错误的可能后果 火箭 Ariane 5 Explosion (1997) 火星气候轨道器 NASA Mars Climate Orbiter (1999),程序正确性方法,测试 黑盒测试 白盒测试 形式验证 推理验证 模型检测,可执行代码,程序代码,程序代码或其抽象模型 程序运行环境模型,规则,算法,例子: ISR,#include /*/ 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 activen“); while (1) n=in(); m=isr(n,k); k=isk(n,k); printf(“RESULT: %inn“,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|(x2 ,./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,#include /*/ 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 activen“); while (1) n=in(); m=isr(n,k); k=isk(n,k); printf(“RESULT: %inn“,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|(x2 ,对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,#include /*/ 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 activen“); while (1) n=in(); m=isr(n,k); k=isk(n,k); printf(“RESULT: %inn“,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|(x2 ,对ISR的要求:,(at line 18):(m*m)n),程序的模型检测(例子),模型检测,./verds c isr.c sp isr.sp,验证结果,反例,验证过程,C Program,Model,Automatic Translator,VERDS Model Checker,Negative Conclusion,Specification,Error Trace,反例分析,以下输入产生不正确结果 1 3 5 7 9 11 13 15 17 19 0 2 4 6 8 10 12 14 16 18 4,不正确运行,修正后的例子: ISR2,#include /*/ 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 activen“); while (1) n=in(); k=isk(n,k); m=isr(n,k); printf(“RESULT: %inn“,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|(x2 ,./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,验证结果,验证过程,C Program,Model,Automatic Translator,VERDS Model Checker,Specification,Positive Conclusion,模型检测的缺点与优点,缺点 可直接验证的程序规模小 可直接验证的程序结构简单 优点: 自动验证 对不正确的程序可生成诊断信息,形式验证,推理验证 模型检测 推理验证与模型检测相结合,推理验证+模型检测,#include /*/ 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 activen“); while (1) n=in(); k=isk(n,k); m=isr(n,k); printf(“RESULT: %inn“,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|(x2 ,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;,推理验证+模型检测,#include /*/ 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 activen“); while (1) n=in(); k=isk(n,k); m=isr(n,k); printf(“RESULT: %inn“,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|(x2 ,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;,FUNCTION r=in() ASSUMPTION TRUE; GUARANTEE r=0,模型检测,./verds c isr.c sp isr.sp fsp isr.fsp 时间优势对比:,验证结果,验证过程,C Program,Model,Automatic Translator,VERDS Model Checker,Specification,Positive Conclusion,Function Specification,/zwh/verds/,并发模型的模型检测(例子),并发模型的模型检测(例子),a=s0 b=t0 x=0 y=0 t=0,并发模型的模型检测,验证问题,Model,建模,并发模型(主程序),VVM VAR x: 01; y: 01; t: 01; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2,并发模型(进程模块说明1),MODULE p0m() VAR a: s0,s1,s2,s3; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1,并发模型(进程模块说明2),MODULE p1m() VAR b: t0,t1,t2,t3; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=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 - time = 0 bound = 3 time = 0 - time = 0 bound = 4 time = 0 - time = 0 bound = 5 time = 0 - time = 0 bound = 6 time = 0 - time = 0 CONCLUSION: TRUE (time=0),模型检测结论,进程公平性说明,并发模型(主程序),VVM VAR x: 01; y: 01; t: 01; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2,并发模型(进程模块说明1a),MODULE p0m() VAR a: s0,s1,s2,s3; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1,并发模型(进程模块说明2a),MODULE p1m() VAR b: t0,t1,t2,t3; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1,模型检测结论,进程公平性说明2,并发模型(主程序),VVM VAR x: 01; y: 01; t: 01; INIT x=0; y=0; t=0; PROC p0: p0m(); p1: p1m(); SPEC AG(!(p0.a=s2,并发模型(进程模块说明1b),MODULE p0m() VAR a: s0,s1,s2,s3; INIT a=s0; TRANS a=s0: (y,t,a):=(1,1,s1); a=s1,并发模型(进程模块说明2b),MODULE p1m() VAR b: t0,t1,t2,t3; INIT b=t0; TRANS b=t0: (x,t,b):=(1,0,t1); b=t1,模型检测结论,验证过程,验证问题,Model,建模,VERDS Model Checker,Positive Conclusion,/zwh/verds/,Negative Conclusion,Error T