《程序的形式验证.ppt》由会员分享,可在线阅读,更多相关《程序的形式验证.ppt(23页珍藏版)》请在三一办公上搜索。
1、程序的形式验证,张文辉http:/,程序正确性的重要性,应用广泛航空航天金融设备的控制日常生活软件错误的可能后果火箭 Ariane 5 Explosion(1997)火星气候轨道器 NASA Mars Climate Orbiter(1999),程序正确性,程序软件系统软件系统行为,正确性,符合行为规范,程序正确性,软件系统行为,行为规范,测试,Program testing can be used to show the presence of bugs,but never to show their absence!-Edsger W.Dijkstra,程序正确性,软件系统行为,行为规范,
2、形式验证?,程序正确性,软件系统行为,行为规范,形式验证,形式模型,逻辑公式,程序正确性,软件系统行为,行为规范,形式模型,逻辑公式,基于谓词逻辑的描述,基于显式状态的描述(有穷状态系统),程序正确性,软件系统行为,行为规范,形式模型,逻辑公式,命题逻辑、谓词逻辑:状态描述,时序逻辑:行为描述,程序正确性,软件系统行为,行为规范,形式验证,形式模型,逻辑公式,程序推理,模型检测,课程主要内容,形式验证,形式模型,逻辑公式,程序推理,模型检测,谓词逻辑模型,显式状态模型,程序逻辑,11,预期目标,程序逻辑,程序与系统模型,验证方法,掌握并能够综合应用以下知识:,基本原理,几类简单的,几类简单的,
3、课程资料网页,http:/,主要参考资料,软件系统行为与程序正确性。http:/,参考书,Jacques Loeckx and Kurt Sieber.The Foundation of Program Verification.John Wiley&Sons Ltd.,1984.Gerard J.Holzmann.Design and Validation of Computer Protocols.Prentice Hall,1990.Nissim Francez.Program Verification.Addison-Wesley Publishing Company Inc.,199
4、2.Edmund Clark,Orna Grumberg and Doron Peled.Model Checking.MIT press,1999.Doron A.Peled.Software Reliability Methods.Springer-Verlag.2001.Christel Baier and Joost-Pieter Katoen.Principles of Model Checking.MIT Press.2008.Krzysztof R.Apt,Frank S.de Boer,Ernst-Rdiger Olderog.Verification of Sequentia
5、l and Concurrent Programs.Springer-Verlag.2009.,Questions?,课程主要内容,形式验证,形式模型,逻辑公式,程序推理,模型检测,谓词逻辑模型,显式状态模型,程序逻辑,课程主要内容(1),形式模型,谓词逻辑模型,显式状态模型,Kripke Structures,-Automata,Timed Automata,Petri Nets,结构化循环语句模型,流程图模型,卫式迁移模型,课程主要内容(2),逻辑公式,程序逻辑,线性时序逻辑LTL,计算树逻辑CTL/CTL*,-演算,课程主要内容(3,4),形式验证,程序推理,模型检测,卫式迁移模型/LTL,流程图模型/前后断言,线性时序逻辑PLTL,计算树逻辑CTL,课程主要内容,形式验证,形式模型,逻辑公式,程序推理,模型检测,谓词逻辑模型,显式状态模型,程序逻辑,课程主要内容,形式验证,形式模型,逻辑公式,程序推理,模型检测,谓词逻辑模型,显式状态模型,程序逻辑,描述问题刻画行为,描述问题刻画行为,课程主要内容,形式验证,形式模型,逻辑公式,程序推理,模型检测,谓词逻辑模型,显式状态模型,程序逻辑,方法/算法原理及应用,方法/算法原理及应用,23,问题?,
链接地址:https://www.31ppt.com/p-6138912.html