程序的形式验证

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预期目标程序逻辑程序与系统模型验证方法掌握并能够综合应用以下知识:基本原理几类简单的几类简单的课程资料网页http:/ Loeckx and Kurt Sieber. The Foundation of Pr

3、ogram 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., 1992.Edmund Clark, Orna Grumberg and Doron Peled. Model Checking. MIT press, 1999.Doron

4、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 Sequential and Concurrent Programs. Springer-Verlag. 2009. Questions?课程主要内容形式验

5、证形式模型逻辑公式程序推理模型检测谓词逻辑模型显式状态模型程序逻辑课程主要内容(1)形式模型谓词逻辑模型显式状态模型Kripke Structures-AutomataTimed AutomataPetri Nets结构化循环语句模型流程图模型卫式迁移模型课程主要内容(2)逻辑公式程序逻辑线性时序逻辑LTL计算树逻辑CTL/CTL*-演算课程主要内容(3,4)形式验证程序推理模型检测卫式迁移模型/LTL流程图模型/前后断言线性时序逻辑PLTL计算树逻辑CTL课程主要内容形式验证形式模型逻辑公式程序推理模型检测谓词逻辑模型显式状态模型程序逻辑课程主要内容形式验证形式模型逻辑公式程序推理模型检测谓词逻辑模型显式状态模型程序逻辑描述问题刻