模型检验 ■模型检验是一种自动验证有穷状态系统的技术 ■模型检验的基本思想是通过遍历系统模型的状态 空间来检验系统模型是否满足给定的性质。 ■模型检验技术的创始人(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)