第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 , 简写成 – 语义等价 并且 – 可满足性 是可满足的，若存在一种指派使的值为真
命题逻辑的▣顾 命题逻辑是可靠的和完备的 命题逻辑的可靠性 若T w是有效的（可证明的），则T w成 立 命题逻辑的完备性 若Tw成立，则T w是有效的 命题逻辑的可靠性和完备性 T w有效，当且仅当 w成立
命题逻辑的回顾 • 命题逻辑是可靠的和完备的 – 命题逻辑的可靠性 若 是有效的（可证明的），则 成 立 – 命题逻辑的完备性 若 成立，则 是有效的 – 命题逻辑的可靠性和完备性 有效，当且仅当 成立
谓词逻辑的回顾 合式公式 谓词符号集合、函数符号集合 (包括常量符 号)》 -基于 来定义项集 t::=xc ft,...,t) 归纳地定义基于(， )的合适公式 φ：=P(t1,t2,,tn)1(φ)1（φvφ）1（φ∧φ）1 (中→中)1(xφ)|（目xφ） (P∈ ·自由变量、约束变量、代换
谓词逻辑的回顾 • 合式公式 – 谓词符号集合 、函数符号集合 （包括常量符 号） – 基于 来定义项集 t ::= x | c | f(t, …, t) – 归纳地定义基于（ , ）的合适公式 ::= P(t1 , t2 , …, tn ) | ( ) | ( ) | ( ) | ( → ) | (x ) | ( x ) ( P ) • 自由变量、约束变量、代换
谓词逻辑的回顾 新增推理规则（包括公理） 一项相等的证明规则 一全称量词证明规则 一存在量词证明规则 -量词间的等价规则 语义模型、可靠性、完备性 一它们都可以基于命题逻辑相应概念进行拓展 -T 中和T yw的意思与前面的一致 Ψw表示y在模型 中成立
谓词逻辑的回顾 • 新增推理规则（包括公理） – 项相等的证明规则 – 全称量词证明规则 – 存在量词证明规则 – 量词间的等价规则 • 语义模型、可靠性、完备性 – 它们都可以基于命题逻辑相应概念进行拓展 – 和 的意思与前面的一致 – 表示在模型 中成立
形式证的动机 形式验证技术由三部分组成 一用于系统建模的框架，通常是某种描述语言 一用于描述待验证性质的规范语言 一用来确立系统描述是否满足规范的验证方法 基于逻辑推理的方法 -系统描述是适当逻辑中的一组公式 待证性质的规范是另一个公式 验证就是试图通过该逻辑的公理和推理规则来证 明T
形式验证的动机 • 形式验证技术由三部分组成 – 用于系统建模的框架，通常是某种描述语言 – 用于描述待验证性质的规范语言 – 用来确立系统描述是否满足规范的验证方法 • 基于逻辑推理的方法 – 系统描述是适当逻辑中的一组公式 – 待证性质的规范是另一个公式 – 验证就是试图通过该逻辑的公理和推理规则来证 明
形式证的动机 ·形式验证技术由三部分组成 基于逻辑推理的方法 -系统描述是适当逻辑中的一组公式工 -待证性质的规范是另一个公式少 一验证就是通过该逻辑来证明 基于模型的方法 -系统由适当逻辑的某个模型 表示 -待证性质的规范仍由公式表示 验证就是计算模型是否满足中( )
形式验证的动机 • 形式验证技术由三部分组成 • 基于逻辑推理的方法 – 系统描述是适当逻辑中的一组公式 – 待证性质的规范是另一个公式 – 验证就是通过该逻辑来证明 • 基于模型的方法 – 系统由适当逻辑的某个模型 表示 – 待证性质的规范仍由公式表示 – 验证就是计算模型 是否满足（ ）