模型检测例子.ppt
《模型检测例子.ppt》由会员分享,可在线阅读,更多相关《模型检测例子.ppt(43页珍藏版)》请在三一文库上搜索。
1、模型检测 例子,中国科学院软件研究所 计算机科学国家重点实验室 张文辉 http:/ 航空 航天 金融 设备的控制 日常生活 软件错误的可能后果 火箭 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 m
2、ain() 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 RESU
3、LT: 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); /*/ i
4、nt 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,形式验证,推理验证 模型检测,正确性,正确性+不正确性
5、,例子: 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
6、 (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 /*/
7、 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 INF
8、O: 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,模型检测的缺点与优点,缺点 可直接验证的程序规模小 可直接验证
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 模型 检测 例子
链接地址:https://www.31doc.com/p-2596063.html