形式证的动机 ·形式验证技术由三部分组成 基于逻辑推理的方法 -系统描述是适当逻辑中的一组公式 -待证性质的规范是另一个公式 -验证就是通过该逻辑来证明 基于模型的方法 -系统由适当逻辑的某个模型 表示 -待证性质的规范仍由公式表示 验证就是计算模型 是否满足中( φ) 比 基于证明方法简单，因为只考虑单个模型
形式验证的动机 • 形式验证技术由三部分组成 • 基于逻辑推理的方法 – 系统描述是适当逻辑中的一组公式 – 待证性质的规范是另一个公式 – 验证就是通过该逻辑来证明 • 基于模型的方法 – 系统由适当逻辑的某个模型 表示 – 待证性质的规范仍由公式表示 – 验证就是计算模型 是否满足（ ） 比 基于证明方法简单，因为只考虑单个模型
形式殓证的一些特性 自动化程度 -基于模型的方法高于基于逻辑的方法 性质验证和完全验证 一规范可描述单个性质或全部行为 -完全验证的代价要高昂得多 潜在应用领域 -硬件或软件、串行或并发、反应式或终止式 开发前与开发后 -开发前验证可及早发现错误，降低纠错代价
形式验证的一些特性 • 自动化程度 – 基于模型的方法高于基于逻辑的方法 • 性质验证和完全验证 – 规范可描述单个性质或全部行为 – 完全验证的代价要高昂得多 • 潜在应用领域 – 硬件或软件、串行或并发、反应式或终止式 • 开发前与开发后 – 开发前验证可及早发现错误，降低纠错代价
模型检测及所用逻辑概述 模型检测 一基于模型的性质验证的自动化方法 -最初试图用于并发、反应式系统 一作为一种开发后的方法论问世 模型检测的大体步骤 由用户描述的一个模型开始 -判断用户所断言的假设在模型中是否有效 若无效，则产生由执行轨迹构成的反例
模型检测及所用逻辑概述 • 模型检测 – 基于模型的性质验证的自动化方法 – 最初试图用于并发、反应式系统 – 作为一种开发后的方法论问世 • 模型检测的大体步骤 – 由用户描述的一个模型开始 – 判断用户所断言的假设在模型中是否有效 – 若无效，则产生由执行轨迹构成的反例
模型检测及所用逻辑概述 Model checking,narrowly interpreted Decision procedures for checking if a given Kripke structure is a model for a given formula of a modal logic. Why is this of interest to us? - Because the dynamics of a discrete system can be captured by a Kripke structure. Because some dynamic properties of a discrete system can be stated in modal logics. Model checking System verification
模型检测及所用逻辑概述 • Model checking, narrowly interpreted – Decision procedures for checking if a given Kripke structure is a model for a given formula of a modal logic. • Why is this of interest to us? – Because the dynamics of a discrete system can be captured by a Kripke structure. – Because some dynamic properties of a discrete system can be stated in modal logics. Model checking = System verification
模型检测及所用逻辑概述 Model checking,generously interpreted Algorithms for system verification which operate on a system model (semantics) rather than a system description (syntax). There are many different model-checking problems for different (classes of)system models for different (classes of)system properties
模型检测及所用逻辑概述 • Model checking, generously interpreted – Algorithms for system verification which operate on a system model (semantics) rather than a system description (syntax). • There are many different model-checking problems – for different (classes of) system models – for different (classes of) system properties