第6章 模型检测 验证是提高软件可信程度的重要方法 模型检测 -基于逻辑推理的程序验证 模型检测 一种验证系统 满足性质p( 中)的方法。它 操作在系统的模型 (语义)上，而不是在系统 的描述（语法）上 通过遍历系统所有状态空间，能够对有穷状态系 统进行自动验证，并自动构造不满足验证性质的 反例
第6章 模型检测 • 验证是提高软件可信程度的重要方法 – 模型检测 – 基于逻辑推理的程序验证 • 模型检测 – 一种验证系统 满足性质 ( )的方法。它 操作在系统的模型 （语义）上，而不是在系统 的描述（语法）上 – 通过遍历系统所有状态空间，能够对有穷状态系 统进行自动验证，并自动构造不满足验证性质的 反例
第6章 模型检测 模型检测的应用 -常用于硬件验证和通信协议的验证中 -现在开始用于软件的验证 模型检测过程的大体步骤 -由用户描述的一个模型开始 -判断用户所断言的假设在模型中是否有效 -若无效，则产生由执行轨迹构成的反例
第6章 模型检测 • 模型检测的应用 – 常用于硬件验证和通信协议的验证中 – 现在开始用于软件的验证 • 模型检测过程的大体步骤 – 由用户描述的一个模型开始 – 判断用户所断言的假设在模型中是否有效 – 若无效，则产生由执行轨迹构成的反例
第6章 模型检测 ·内容概述 -命题逻辑和谓词逻辑的简短回顾 -线性时态逻辑及其在模型检测中的应用 一计算树逻辑及其在模型检测中的应用
第6章 模型检测 • 内容概述 – 命题逻辑和谓词逻辑的简短回顾 – 线性时态逻辑及其在模型检测中的应用 – 计算树逻辑及其在模型检测中的应用
命题逻辑的回顾 合适公式的归纳定义 中：=p1(中)1（φv中）1（φΛ中）1（中→中） 推理规则（包括公理 () (e) (e2) b∧W 语法推论 若从4，，n可以证明必，表示成 ,,,中nΨ 简写成 逻辑等价 并且w
命题逻辑的回顾 • 合适公式的归纳定义 ::= p | ( ) | ( ) | ( ) | ( → ) • 推理规则（包括公理） ( i) (e1 ) (e2 ) • 语法推论 若从1 , 2 , …, n 可以证明，表示成 1 , 2 , …, n , 简写成 • 逻辑等价 并且
命题逻辑的回顾 命题逻辑的语义 定义真值集合（给p,q指派真值） 把各逻辑连接词映射到真值集合上的运算（真值 表方式) 各推理规则在该模型中成立 语义推论 若，，，n的值都为真，则y值也为真，写成 41,,,中n 简写成工 语义等价 w并且w 可满足性 是可满足的，若存在一种指派使的值为真
命题逻辑的回顾 • 命题逻辑的语义 – 定义真值集合（给p, q指派真值） – 把各逻辑连接词映射到真值集合上的运算（真值 表方式） – 各推理规则在该模型中成立 – 语义推论 若1 , 2 , …, n的值都为真, 则 值也为真, 写成 1 , 2 , …, n , 简写成 – 语义等价 并且 – 可满足性 是可满足的，若存在一种指派使的值为真