模型检验 ■模型检验是一种自动验证有穷状态系统的技术 ■模型检验的基本思想是通过遍历系统模型的状态 空间来检验系统模型是否满足给定的性质。 ■模型检验技术的创始人(1981): o E.M. Clarke (CMU,US) o E.A. Emerson (UT Austin, US) o J. Sifakis (Verimag, France)
模型检验 ◼ 模型检验是一种自动验证有穷状态系统的技术。 ◼ 模型检验的基本思想是通过遍历系统模型的状态 空间来检验系统模型是否满足给定的性质。 ◼ 模型检验技术的创始人（1981）： E.M. Clarke (CMU,US) E.A. Emerson (UT Austin, US) J. Sifakis (Verimag, France)
在硬件,协议设计上巨大成功 ■现有手段:测试、仿真 太多可能、慢、无法穷尽、没有保障 o举例:加法器测试:2160个浮点数对 形式化方法 o自动证明、确定性结果 o奔4浮点数计算部牛刀小试: 2003: FV found many high-quality bugs in P4 and verified"20%of design FV is now standard practice in the floating-point domain o Can we do more? 2009: Replacing Testing with Formal Verification in Intel CoreTM Processor Execution Engine validation a CAV09
在硬件，协议设计上巨大成功 ◼ 现有手段：测试、仿真 太多可能、慢、无法穷尽、没有保障 举例：加法器测试：2 160个浮点数对… ◼ 形式化方法 自动证明、确定性结果 奔4 浮点数计算部 牛刀小试： Can we do more？ 2003：FV found many high-quality bugs in P4 and verified “20%” of design FV is now standard practice in the floating-point domain 2009：Replacing Testing with Formal Verification in Intel 𝐂𝐨𝐫𝐞𝐓𝐌 i7 Processor Execution Engine Validation @ CAV09
07 Turing award!
07 Turing Award!
模型检验的过程 建模( Modeling) 规约( Specification) ■验证( Verification)
模型检验的过程 ◼ 建模（Modeling） ◼ 规约（Specification） ◼ 验证（Verification）
模型检验 在模型检验中涉及两种形式说明语言: 性质说明语言用于描述系统的性质 模型描述语言用于描述系统的模型。 模型检验技术用于检验由模型描述语言描述的系 统模型是否满足由性质说明语言描述的系统性质
模型检验 ◼ 在模型检验中涉及两种形式说明语言： 性质说明语言用于描述系统的性质; 模型描述语言用于描述系统的模型。 ◼ 模型检验技术用于检验由模型描述语言描述的系 统模型是否满足由性质说明语言描述的系统性质