




已阅读5页,还剩38页未读, 继续免费阅读
版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
模型检测 例子,中国科学院软件研究所 计算机科学国家重点实验室 张文辉 /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
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 2025年绥化市青冈县人民政府办公室选调工作人员5人考前自测高频考点模拟试题(含答案详解)
- 2025甘肃天水市武山县人力资源和社会保障局招聘城镇公益性岗位人员26人考前自测高频考点模拟试题及答案详解(网校专用)
- 基因检测疫病识别-洞察与解读
- 2025河南郑州二七区一国企招聘各部门人员9人考前自测高频考点模拟试题及参考答案详解1套
- 2025湖南长沙高新区中心幼儿园和馨园招聘教师2人模拟试卷及答案详解一套
- 2025年泉州安溪城建集团有限公司招聘17人考前自测高频考点模拟试题及答案详解(夺冠)
- 2025广东韶关市始兴县事业单位招聘暨“青年人才”和“急需紧缺人才”招聘89人模拟试卷含答案详解
- 2025广西百色市西林县社会保险事业管理中心招聘编外聘用人员6人考前自测高频考点模拟试题附答案详解(完整版)
- 2025甘肃嘉陵关市卫生健康委公开招聘公益性岗位人员考前自测高频考点模拟试题附答案详解
- 2025呼伦贝尔市政务服务与数据管理局所属事业单位竞争性比选工作人员考前自测高频考点模拟试题及答案详解(典优)
- 食品新产品开发 课件 第二章 食品新产品开发流程
- 高中化学374个必备知识点
- 单轴燃气蒸汽联合循环机组调试程序
- 舟山海域赤潮发生特点及成因分析
- 湿陷性黄土湿陷量计算表
- 丝杠安全操作保养规定
- 体育测量与评价PPT课件-第九章 运动员选材的测量与评价
- 《情满今生》读书笔记模板
- 胸痛中心网络医院STEMI患者绕行急诊和CCU方案流程图
- 大众蔚揽保养手册
- 急危重病人营养与代谢支持
评论
0/150
提交评论