大房 NANJING UNIVERSITY Model Checking Lei bu
Lei Bu Model Checking
随着计算机技术在各行各业应用的日 益普及,计算机已经渗透到我们工作 和生活的方方面面,成为我们工作和 生活的一部分,从而极大地促进了社 会的发展和生产力的提高。 与此同时,工作在我们身边的各种计 算机系统由于其中的软件系统失效经 常表现不尽人意,呈现出脆弱、难以 信任的特征,甚至造成不可挽回的损 失,因此研究相关的可信软件关键技 术以提高软件系统的可信性已经成为 十分迫切的需求
◼ 随着计算机技术在各行各业应用的日 益普及,计算机已经渗透到我们工作 和生活的方方面面，成为我们工作和 生活的一部分，从而极大地促进了社 会的发展和生产力的提高。 ◼ 与此同时，工作在我们身边的各种计 算机系统由于其中的软件系统失效经 常表现不尽人意，呈现出脆弱、难以 信任的特征，甚至造成不可挽回的损 失，因此研究相关的可信软件关键技 术以提高软件系统的可信性已经成为 十分迫切的需求
欧洲阿丽亚娜5型火箭 1996年6月4日 因软件失效在 发射40秒后爆 炸,原因是惯 性参考系统 软件的数据 转换异常造 成的失效
欧洲阿丽亚娜5型火箭 1996年6月4日 因软件失效在 发射40秒后爆 炸，原因是惯 性参考系统 软件的数据 转换异常造 成的失效
美国F22猛禽战斗机 2007年2月9 日同样因软 件问题延迟 在日本部署 2004年12月20日,美空军第422测试评估大队的 架F-22战斗机因软件问题在起飞过程中失控坠毁
美国F-22猛禽战斗机 2007年2月9 日同样因软 件问题延迟 在日本部署 2004年12月20日，美空军第422测试评估大队的一 架F-22战斗机因软件问题在起飞过程中失控坠毁
与美国电力监测与控制管理系统 多计算机 August 14. 2003 A programming error has been identified as the cause of the Northeast power 系统试图 blackout. The Tailure occurred when multiple computer systems trying to access he Equivalent of busy signals. 同时访问 同一资源 引起的软 件失效 Price tag $6-10 billian EAT,e甲tax45 A11
美国电力监测与控制管理系统 多计算机 系统试图 同时访问 同一资源 引起的软 件失效