Verification Methods

验证方法可根据以下主要标准进行分类：

• 基于证明与基于模型-如果可靠性和完整性定理成立，则：

  • 证明=有效公式=在所有模型中均为真；

  • 基于模型=检查一个模型中的可满足性

• 自动化程度-完全自动化、部分自动化或手动

• 完整-与属性-验证-单个属性与完整行为

• 应用领域-硬件或软件；连续的或并发的；反应的或终止的；等

• 前期开发与后期开发

Model Checking

• 模型检查是一种验证方法，即：

基于模型、自动化、使用属性验证方法，主要用于验证并发程序和反应式系统，通常在后开发阶段。

• 程序验证（稍后研究）是：

基于证明的计算机辅助（部分自动化），主要用于顺序终止程序

对于任何模型检查问题（基于CTL或其他逻辑），我们需要回答 的问题？

其中M是给定系统的适当模型，s是模型的状态；

φ是系统要满足的CTL公式。

Kripke Structures

经典命题和谓词演算使用一个独特的宇宙来解释公式。

20世纪50年代，克里普克引入了一种语义模型，在这种模型中，更多的（局部）宇宙是可能的

在这些宇宙之间存在着一种可接近性的关系，以及表达这些宇宙之间关系的运算子，导致了各种各样的形态。

当添加这样的操作符时，就会得到模态日志。当时间是导致从一个宇宙传递到另一个宇宙的参数时，我们谈论时间逻辑。

Kripke Structures for Programs

程序（软件）非常适合此框架：

• 宇宙对应一种状态；

• 可达性关系由一种状态到另一种状态的转换给出；

• 经典谓词逻辑可用于指定状态中变量之间的关系。

在这一点上，我们缺乏一种机制来联系这些统一体（国家）。本课程应介绍各种此类机制。

Views of Time

我们有以下时间特征：

• 线性-时间实例链，或

• 分支-在一个给定的时间点上可能有几个可供选择的未来世界；或

• 离散-时间由一组整数表示，或

• 连续-时间由一组实数表示。

接下来，我们将研究计算树逻辑（CTL），它是一种使用分支和离散时间的时态逻辑。

The Syntax of CTL

BNF对CTL的定义：

新的连接词AX、EX、AU、EU、AG、EG、AF和EF称为时间连接词。

Depth and Breadth Quantification

时间连接词使用两个字母：

• A和E在分支点的宽度上进行量化：

  • A分支点中的所有备选方案；

  • E分支点中至少存在一个备选方案

• G和F沿路径进行量化：

  • G全球所有未来国家都在一条道路上；

  • F路径上至少存在一个未来状态

• 使用另外两个运算符X和U沿路径表示属性：

  • X表示路径中的下一个状态（这导致时间的离散特征），以及

  • U-直到运算符。

Priorities

公约：

一元连接词（包括AX、EX、AG、EG、AF和EF）结合最紧密；

下一步∧ 和∨

最低优先级→ , AU和EU。

Examples

CTL Semantics CTL语义

The Satisfaction Relation

Comments

注意，“未来”是自反传递闭包→* （直接）可及性关系的定义→.

通俗地说：

未来包含现在和未来

t的未来就是t的未来。

通过展开CTL模型的图形，可以得到一个无限树，因此是“计算树逻辑”。

Unfolding

CTL图及其展开

The Meaning of EF, EG, AG, and AF

EF EG

AG AF

Until

直到线性时间模型中的p U q[或CTL中的路径]。公式puq适用于s3，但不适用于s0（我们假设p仅适用于指定状态）

An Improved Variant 改进型

• 使用EX、EU和EG代替EX、EU和AF

• 像以前一样处理EX和EU（使用向后广度优先搜索）

• 对于EGφ

  • 仅限于满足以下条件的国家：

  • 查找SCC（最大强连接组件；这些是最大区域，使得任何顶点都连接到该区域中的任何其他顶点）

  • 在受限图上使用向后广度优先搜索，以查找可到达SCC的任何状态

复杂性降低到

Pseudo-Code 伪码

Function SAT(φ)

Function SAT_EX(φ)

Function SAT_AF(φ)

Function SAT_EU(φ,ψ)

The State Explosion Problem

• 标记算法相当有效[模型大小呈线性]

• ... 但是模型本身可能很大，组件的数量是指数级的（在10个线程中并行运行，每个线程有10个状态，导致系统有10^10个状态！）

• 状态空间变得非常大的趋势通常被称为状态爆炸问题

• 状态爆炸问题主要没有解决，目前还没有通用的解决方案

Dealing With the State Explosion Code

这个问题还没有解决。在某些特定情况下，开发了以下技术来克服这一问题：

1. 有效的数据结构-例如，有序二进制决策图OBDD（OBDD用于表示状态集，而不是单个状态）

2. 抽象-可以抽象出模型中与所检查公式无关的变量

3. 部分降阶-就要检查的公式而言，不同的运行可能是等效的；偏序缩减只检查此类类中的一个跟踪

4. 归纳法-当考虑大量过程时，使用该技术

5. 组成-尝试将问题分解为单独检查的小部分

Assignment

检查以下模型是否满足CTL公式

AG(Start→AF Heat)

Solution

Translate

AG(Start→AF Heat)=¬E[⊤U(start∧¬AF Heat)]

Compute

S(M⊨Heat)={4,7}

S(M⊨AF Heat)={4,7,6}

S(M⊨¬AF Heat)={1,2,3,5}

S(M⊨(start∧¬AF Heat))={2,5}

S(M⊨E[⊤U(start∧¬AF Heat)])={1,2,3,4,5,6,7}

S(M⊨¬E[⊤U(start∧¬AF Heat)])=∅

AG(A[¬Error U (AF Close)])

Solution

Translate

AG(A[¬Error U (AF Close)])=¬E[⊤U(E[¬AF Close U (Error∧¬AF Close)]∨¬AF(AF Close))]

Compute

S(M⊨Close)={3,4,5,6,7}

S(M⊨AF Close)={1,2,3,4,5,6,7}

S(M⊨¬AF Close)=∅

S(M⊨¬AF(AF Close))=∅

S(M⊨Error∧¬AF Close)=∅

S(M⊨E[¬AF Close U (Error∧¬AF Close)])=∅

S(M⊨(E[¬AF Close U (Error∧¬AF Close)]∨¬AF(AF Close)))=∅

S(M⊨E[⊤U(E[¬AF Close U (Error∧¬AF Close)]∨¬AF(AF Close))])=∅

S(M⊨¬E[⊤U(E[¬AF Close U (Error∧¬AF Close)]∨¬AF(AF Close))])={1,2,3,4,5,6,7}