美国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）