大房 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秒后爆 炸，原因是惯 性参考系统 软件的数据 转换异常造 成的失效