提高可信度的途径 测试( testing)或仿真( simulation) 无法回答系统一定没有错误这样一类问题 ■验证( Verification) 可以从某一个角度回答系统一定没有错误这样一类问题, 从而进一步提高我们对系统可靠性的可信度
提高可信度的途径 ◼ 测试（testing）或 仿真（simulation） 无法回答系统一定没有错误这样一类问题 ◼ 验证（Verification） 可以从某一个角度回答系统一定没有错误这样一类问题， 从而进一步提高我们对系统可靠性的可信度
形式化方法 ■形式化方法是指为说明和验证复杂计算机系 统所采用的基于数学的语言、技术和工具 ■形式化方法不能确保系统的可靠性,但其可 以通过揭示系统的不一致性、歧义性和不完 备性来增加我们对系统的理解程度,从而提 高我们对系统可靠性的可信度
形式化方法 ◼ 形式化方法是指为说明和验证复杂计算机系 统所采用的基于数学的语言、技术和工具。 ◼ 形式化方法不能确保系统的可靠性，但其可 以通过揭示系统的不一致性、歧义性和不完 备性来增加我们对系统的理解程度，从而提 高我们对系统可靠性的可信度
形式验证 形式化方法包括: 规约( specification) 验证( verification) 形式验证包括: 模型检验( model checking 推理验证( theorem proving
形式验证 ◼ 形式化方法包括： 规约（specification） 验证（verification） ◼ 形式验证包括： 模型检验（model checking） 推理验证（theorem proving）
模型检验 ■模型检验是一种自动验证有穷状态系统的技术。 ■模型检验的基本思想是通过遍历系统模型的状态 空间来检验系统模型是否满足给定的性质。 ■模型检验技术的创始人(1981): o E.M. Clarke o E A. Emerson (USA) o J. Sifakis (France)
模型检验 ◼ 模型检验是一种自动验证有穷状态系统的技术。 ◼ 模型检验的基本思想是通过遍历系统模型的状态 空间来检验系统模型是否满足给定的性质。 ◼ 模型检验技术的创始人（1981）： E.M. Clarke E.A. Emerson (USA) J. Sifakis (France)
07 Turing award
07 Turing Award!