第6章 模型检测 验证是提高软件可信程度的重要方法 模型检测 -基于逻辑推理的程序验证 模型检测 一种验证系统 满足性质p( 中)的方法。它 操作在系统的模型 (语义)上，而不是在系统 的描述（语法）上 通过遍历系统所有状态空间，能够对有穷状态系 统进行自动验证，并自动构造不满足验证性质的 反例第6章 模型检测 • 验证是提高软件可信程度的重要方法 – 模型检测 – 基于逻辑推理的程序验证 • 模型检测 – 一种验证系统 满足性质 (  )的方法。它 操作在系统的模型 （语义）上，而不是在系统 的描述（语法）上 – 通过遍历系统所有状态空间，能够对有穷状态系 统进行自动验证，并自动构造不满足验证性质的 反例