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
这个问题还没有解决。在某些特定情况下，开发了以下技术来克服这一问题：
-
有效的数据结构-例如，有序二进制决策图OBDD（OBDD用于表示状态集，而不是单个状态）
-
抽象-可以抽象出模型中与所检查公式无关的变量
-
部分降阶-就要检查的公式而言，不同的运行可能是等效的；偏序缩减只检查此类类中的一个跟踪
-
归纳法-当考虑大量过程时，使用该技术
-
组成-尝试将问题分解为单独检查的小部分
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}
京公网安备 11010502036488号