大房 NANJING UNIVERSITY Model Checking Lei bu
Lei Bu Model Checking
大纲 ■为什么模型检验? ■什么是模型检验? ■怎么做模型检验? 更高更快更强 复杂系统模型检验
大纲 ◼ 为什么模型检验？ ◼ 什么是模型检验？ ◼ 怎么做模型检验？ ◼ 更高更快更强 ◼ 复杂系统模型检验
■计算机已经渗透到我们工作和 生活的方方面面,极大地促进 了社会的发展和生产力的提高 ■工作在我们身边的各种计算机 系统由于其中的软硬件系统失 效经常表现不尽人意,甚至造 成不可挽回的损失
◼ 计算机已经渗透到我们工作和 生活的方方面面，极大地促进 了社会的发展和生产力的提高。 ◼ 工作在我们身边的各种计算机 系统由于其中的软硬件系统失 效经常表现不尽人意，甚至造 成不可挽回的损失
硬件 奔腾芯片93-94 60-100MHz FDI Bug:某数学家发现用一个数字去 除以8245633,702,441时,答案一直错误 1200 $500 million nte内部统计每设计一个新版本Bug数目 增加4倍 物价飙升 ■奔腾四芯片2000-2007 1.5GHz,4200万晶体管 pentium 4 8000 Bugs!
硬件 ◼ 奔腾芯片 93-94 ◼ 60-100 MHz ◼ FDIV Bug：某数学家发现用一个数字去 除以824,633,702,441时，答案一直错误 ◼ $500 million ◼ Intel内部统计 每设计一个新版本Bug数目 增加4倍… ◼ 物价飙升… ◼ 奔腾四芯片 2000-2007 ◼ 1.5GHz，4200万晶体管 ◼ 8000 Bugs！
欧洲阿丽亚娜5型火箭 1996年6月4日 因软件失效在 发射40秒后爆 炸,原因是惯 性参考系统 软件的数据 转换异常造 成的失效
欧洲阿丽亚娜5型火箭 1996年6月4日 因软件失效在 发射40秒后爆 炸，原因是惯 性参考系统 软件的数据 转换异常造 成的失效
美国F22猛禽战斗机 2004年12月20日,美空军第422测试评估大队的 架F-22战斗机因软件问题在起飞过程中失控坠毁。 2007年2月9 日同样因软 件问题延迟 在日本部署
美国F-22猛禽战斗机 2004年12月20日，美空军第422测试评估大队的一 架F-22战斗机因软件问题在起飞过程中失控坠毁。 2007年2月9 日同样因软 件问题延迟 在日本部署
我们的信息基础设施 正建立在脆弱的软硬件之上
我们的信息基础设施 正建立在脆弱的软硬件之上
提高系统可靠性 ·质量管理 在系统开发过程中加强管理,防止可能出现的错误。 测试( testing)或仿真( simulation) 以运行系统(模型)为主要手段发现系统错误。 ·验证( Verification) 建立系统模型,确认系统模型是否存在错误
提高系统可靠性 • 质量管理 在系统开发过程中加强管理，防止可能出现的错误。 • 测试（testing）或 仿真（simulation） 以运行系统（模型）为主要手段发现系统错误。 • 验证（Verification） 建立系统模型，确认系统模型是否存在错误
提高可信度的途径 测试( testing)或仿真( simulation) 无法回答系统一定没有错误这样一类问题 形式化验证( Formal verification) 可以从某一个角度回答系统一定没有错误这样一类问题, 从而进一步提高我们对系统可靠性的可信度
提高可信度的途径 ◼ 测试（testing）或 仿真（simulation） 无法回答系统一定没有错误这样一类问题 ◼ 形式化验证（Formal Verification） 可以从某一个角度回答系统一定没有错误这样一类问题， 从而进一步提高我们对系统可靠性的可信度
形式化方法 形式化方法是指为说明和验证复杂计算机系统所 采用的基于数学的语言、技术和工具。 ■形式化方法包括: 规约( specification) o验证( verification) 形式验证包括: o定理证明( theorem proving 模型检验( model checking)
形式化方法 ◼ 形式化方法是指为说明和验证复杂计算机系统所 采用的基于数学的语言、技术和工具。 ◼ 形式化方法包括： 规约（specification） 验证（verification） ◼ 形式验证包括： 定理证明（theorem proving） 模型检验（model checking）