南京大学：模型检测（PPT课件讲稿）Model Checking

大房 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

美国电力监测与控制管理系统 多计算机 系统试图 同时访问 同一资源 引起的软 件失效

美国空管软件 1N271 20U4 原因是 Without waming, at about 5p. m PDT, air traffic controllers lost contact with about 400 airplanes tey were Lacking over te soutweslennl US. A backup systeun that was supposed to take over in such an event crashed within a mimute after it was turned on. 空管软 件时钟 RB745 0L100 入 B757彬6710N 缺陷 F 737C-28 HO-REG I(LRR-PHNI Pln] B76764R EELL-KIRH

美国空管软件 原因是 空管软 件时钟 缺陷

东京证券交易软件 2005年11月1日, 比 东京证券交易所 因为软件升级出安 安 现系统故障,导 日 揮 千代建日本粉日请G 致早间股市“停出 摆 aHD XINHUAS

东京证券交易软件 2005年11月1日， 东京证券交易所 因为软件升级出 现系统故障，导 致早间股市“停 摆

我们的信息基础设施 正建立在脆弱的软件之上

我们的信息基础设施 正建立在脆弱的软件之上

软件的根本问题: 任何机构和个人都无法确保所开发的软件一定没有问题。 就间接损害不赔付责任: o在法律所允许的最大范围内, Microsoft Corporation或其 他供应商绝不就因使用或不能使用本“软件产品”所发生 的其他损害负赔偿责任,即使 Microsoft Corporation事先 被告知该损害发生的可能性 ■若为 Windows的每一次Bug出现赔偿1美分,比尔盖 茨早已一贫如洗

◼ 软件的根本问题： 任何机构和个人都无法确保所开发的软件一定没有问题。 ◼ 就间接损害不赔付责任：  在法律所允许的最大范围内，Microsoft Corporation或其 他供应商绝不就因使用或不能使用本“软件产品”所发生 的其他损害负赔偿责任，即使Microsoft Corporation事先 被告知该损害发生的可能性。 ◼ 若为Windows的每一次Bug出现赔偿1美分，比尔盖 茨早已一贫如洗

提高系统可靠性 测试( testing)或仿真( simulation) 以运行系统(模型)为主要手段发现系统错误。 验证( Verification) 建立系统模型,确认系统模型是否存在错误。 质量管理 在系统开发过程中加强管理,防止可能出现的错误

提高系统可靠性 • 测试（testing）或 仿真（simulation） 以运行系统（模型）为主要手段发现系统错误。 • 验证（Verification） 建立系统模型，确认系统模型是否存在错误。 • 质量管理 在系统开发过程中加强管理，防止可能出现的错误