验证方法 Verification Methods

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

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

    • 证明=有效公式=适用于所有型号；

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

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

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

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

  • 前期开发与后期开发

模型检查 1 Model Checking

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

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

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

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

克里普克构造 Kripke Structures

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

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

  • 这些宇宙之间存在着可及性关系，而操作符则表示了它们之间的关系

这样的宇宙，导致了各种各样的形态。

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

程序的Kripke结构 Kripke Structures for Programs

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

  • 宇宙对应一种状态；

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

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

在这一点上，我们缺乏一种机制来联系这些宇宙（状态）。在本课程中，应引入各种此类机制。

时间观 Views of Time

我们有以下时间特征：

  • 线性 - 时间实例链，或

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

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

  • 连续 - 时间用实数集表示。

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

模型检查 2 Model Checking

对于任何模型检查问题（基于CTL或其他逻辑），我们需要回答以下问题： alt 其中

  • M是给定系统的合适模型，s是模型的状态；

  • Φ是系统拟满足的CTL公式。

CTL的语法 The Syntax of CTL

BNF对CTL的定义： alt 新的连接词AX、EX、AU、EU、AG、EG、AF和EF称为时间连接词。

深度和广度量化 Depth and Breadth Quantification

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

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

    • 分支点中的所有【All】备选方案；

    • 分支点中至少存在【Exists】一个备选方案

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

    • 全球【Globally】路径上的所有未来状态；
    • 路径上至少存在一个未来【Future】状态

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

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

  • U-直到【Until】运算符。

优先事项 Priorities

公约：

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

  • 下一步∧ 和∨ ;

  • 最低优先级→, AU和EU。

例子 Examples

alt alt 公式的解析树 alt

CTL语义 CTL Semantics

CTL的模型alt包括

  • 一组状态S

  • 二元关系→ 在S上，每个s ∈ S都有s' ∈ S和s → s'

  • 一个标号函数L:S→ P（原子）

直觉是L在一种状态下哪些原子是真的和→ 描述系统如何从一个状态移动到另一个状态。

alt

图形说明： alt

满意关系 The Satisfaction Relation

设alt为CTL，s∈S和φ一个CTL公式的模型。满意度关系alt归纳定义为： alt alt

注释 Comments

  • 注意，“未来”是自反传递闭包alt （直接）可及性关系的定义→
  • 通俗地说：

    • 未来包含现在和

    • t的未来的未来就是t的未来。

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

Unfolding

alt

CTL图及其展开

alt

EF、EG、AG和AF的含义 The Meaning of EF, EG, AG, and AF

EF Φ

alt

EG Φ

alt

AG Φ

alt

AF Φ

alt

直到 Until

alt

直到线性时间模型中的p U q[或CTL中的路径]。

公式puq适用于s3，但不适用于s0（我们假设p仅适用于指定状态）

例子 Examples

alt alt

规范的实用模式 Practical Patterns of Specifications

可检查的实际相关属性示例：

  • 可以达到started保持但未就绪的状态：

EF( started ∧¬ready )

  • 对于任何状态，如果请求发生，那么它最终将被确认：

AG ( request → AF acknowledged )

  • 某个进程在每个计算路径上被无限地启用：

AG ( AF enabled )

  • 无论发生什么情况，某个过程最终都将永远陷入僵局：

AF ( AG deadlocked )

  • 从任何状态都可以进入重新启动状态：

AG (EF restart )

  • 当乘客前往五楼时，二楼上行电梯不会改变方向：

AG(floor =2 ∧ direction =up ∧ ButtonPressed5 → A[direction = up ∪ floor = 5])

  • 电梯可以在三楼门关闭的情况下保持闲置

AG(floor = 3 ∧ idle ∧ door = closed → EG(floor = 3 ∧ idle ∧ door = closed))

有用的等价物 Useful Equivalences

定义：两个CTL公式φ和ψ在语义上是等价的，如果任何模型中满足其中一个的任何状态也满足另一个，则表示为φ ≡ ψ。

有用的等价物：

alt

适当的时间连接词集 Adequate Sets of Temporal Connectives

推论（适当的时间连接词集）：以下连接词集适用于CTL（在某种意义上，每个CTL公式可以仅使用这些连接词转换为等效公式）：

  • AU,EU 和 EX;
  • EG,EU 和 EX;
  • AG,AU 和 AX;
  • AF,EU 和 AX

不动点定义 Fixed Point Definitions

更有用的等价物（定点定义）

alt 求解此类不动点方程Y= φ ∧ AX Y和下一个算子AX和EX的机制足以表示所有时态逻辑算子。

互斥 Mutual Exclusion

目标：开发访问某些关键部分的协议，以便一次只能有一个进程处于其关键部分。所需财产的集合是：

  • 安全性：协议在任何时候只允许一个进程处于其关键部分

  • 活跃性：当任何流程想要进入其关键部分时，最终都会被允许这样做

  • 非阻塞：进程始终可以请求进入其关键部分

  • 无严格顺序：流程无需按严格顺序进入其关键部分

一个简单的模型MUT1

alt

系统由两个过程P1和P2组成，每个过程构成一个循环n→t→c→……（非临界【noncritical】→尝试【trying】→临界【critical】）。系统的行为是P1和P2行为的乘积（交错），但状态(C1,C2)被排除。 alt

第二个模型是MUT2 A second model MUT2

alt

该模型是通过将MUT1的状态s3分为两种不同的状态s3和s8得到的。

通过将s3分为两种状态，我们可以确定哪个进程是第一个请求访问其关键部分的进程：如果P1是第一个，则得到的状态是s3，否则是s8。

注：所有四个属性（即公式φ1至φ4）是否在MUT2中有效？

模型检查算法 Model Checking Algorithms

回想一下，模型检查要解决的问题是

（A） “给定模型M、CTL公式φ和状态s，alt成立吗？”，其中

  • M是系统的模型，s是模型的状态；

  • φ是系统拟满足的CTL公式

系统使用的模型是什么？通常：

“一个系统由一个有限过渡系统（通常是一个巨大的有向图，通常有百万个状态）来表示”

通过展开这些图形获得的无限树有助于发展推理过程的直觉，但不能在有限的计算机上使用。

模型检验结果 A Model Checking Result

给定M、s和φ，模型检查器返回的结果为

（1） 是的：alt或者

（2） 否:alt

但是，非常有用的是，在后一种情况下，大多数模型检查器返回的跟踪/路径也会使φ无效（反例）。

替代问题：

（B） 给出一个模型M和一个CTL公式φ，找出满足φ的模型的所有状态s

这两个问题显然是等价的：一旦一个能够开发算法来解决其中一个问题，另一个问题也就解决了。我们将主要关注后一个问题B。

CTL连接词的约化集 Reduced Set of CTL Connectives

我们从一个使用以下简化的CTL连接词集的版本开始 alt

其中

  • alt 、¬和∧用于命题部分

  • AF、EU和EX用于时间部分

因此，有一个预处理过程来：

  1. 检查给定公式φ和φ的CTL语法正确性

  2. 用公式翻译（φ），仅用连接词写成Γ。

在续集中，我们假设φ是CTL Γ格式的。

标记算法 The Labeling Algorithm

该算法的思想是：

  • 将公式φ分解为若干部分（子公式），并应用结构归纳法以φ的子公式标记图形（直觉是，标记状态的公式在该状态下为真）

  • 对于每个这样的子公式，解析图以根据连接词的含义及其子公式的真值推断出状态中的真值

在2中，可能需要知道子公式在可能许多不同状态下的值；这是时间运算符的情况，但不是命题运算符的情况。

伪码 Pseudo-Code

function SAT

alt alt

function EX

alt

function AF

alt

function EU

alt

状态爆炸问题 The State Explosion Problem

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

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

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

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

处理状态爆炸代码 Dealing With the State Explosion Code

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

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

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

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

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

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

作业

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

  • AG(Start → AF Heat)
  • AG(A[¬Error U (AF Close)])

alt