逻辑与形式化方法

课程视频杨子江-逻辑与形式化方法;参考书籍Handbook of Model Checking

Model Checking

Definition (Model checking) Given a Kripke structure M = (S,R,L), a designated initial state s0 ∈ S, and a temporal logic formula ϕ, the model-checking problem is to decide whether M is a model of ϕ, i.e., whether M,s0 |= ϕ.

三个问题:

  1. 模型Model:怎么把程序等转化成Model?怎么样建立有效的Model?有很多的Model在建立时已经决定了验证时是不确定的。
  2. 形式化验证Specification:Properties很难写。LTL和CTL很难写
  3. 算法Algorithm:软件和硬件系统是不是Properties的一个子集?不是说公式表达的状态越多越复杂,有时候反而会很简单。用BDD做model checking很难预测大小。故现在主要用SAT做验证
    Higher-order theorem proving 是比 Testing 更强大的用于证明程序复杂性的

时序逻辑概述

在一个模型中,公式的真与假不是静态的。

Kripke Structures 克里普克结构

用来做Model Checking 很重要的一个Model。是有限有向图,其顶点用一组原子命题标记。图的顶点和边分别被称为“状态”和“转换”。

Definition (Kripke structure) Let AP be a finite set of atomic propositions.A Kripke structure is a triple (S,R,L) where S is a finite set of states, R ⊆ S × S is a transition relation, and $L: S \mapsto \mathcal{P}(AP)$ labels each state with a set of atomic propositions.

image

分支时序逻辑-计算树逻辑(CTL)

CTL是一种分支时态逻辑,在状态上解释路径量词,在路径上解释时态运算符。可用于断言一条路径的存在。
复杂度大小为:Model大小 * formula大小
路径量词
$A$: 沿所有路径
$E$: 沿至少一条路径
时态操作符(用于原子命题$p$和$q$)
$Xp$: $p$为真在下一个状态
$Fp$: $p$为真在某个未来状态
$Gq$: $q$为真在所有未来状态
$qUp$: $p$在某个未来状态为真,在所有状态$q$一直为真,直到 $p$为真

CTL语法定义:A为给定的原子命题

If $p \in A$, then $p$ is a formula of CTL* .
If $\varphi$ and $\psi$ are formulas of CTL* , then $\varphi \vee \psi$, $\varphi \wedge \psi$, $\neg \varphi$, $A\varphi$, $E\varphi$, $X\varphi$, $F\varphi$, $G\psi$, and $\varPsi U \psi$ are formulas of CTL*.

CTL状态公式真值表
$K$是一个Kripke structure,$\pi$是一个路径,$s$是一个状态,$p$是一个原子命题,$f$和$g$是状态公式,$\varphi$和$\psi$是CTL*公式

image

线性时序逻辑(LTL)

LTL将时间建模成状态的序列,无限延伸到未来。这个状态序列称为计算路径。如果定义系统的一个状态满足一个LTL公式,则由给定状态出发的所有路径都满足该LTL。即LTL隐含着对所有路径做全称量词限定。LTL是CTL的一个语法子集?但是算法时间复杂度比CTL大。Model的大小 * formula的指数大小。

If $p \in A$, then $p$ is a formula of LTL- .
If $\varphi$ and $\psi$ are formulas of LTL- , then $\varphi \vee \psi$, $\varphi \wedge \psi$, $\neg \varphi$, $X\varphi$, $F\varphi$, $G\psi$, and $\varPsi U \psi$ are formulas of LTL-.
If $\psi$ is a formula of LTL-, $A\psi$ is an LTL formula.

Modeling Software Systems

多线程系统相较于单线程系统存在新的问题:资源竞争、死锁、运算顺序等。
状态空间爆炸问题。

时序逻辑

语言要求:Formal(规范)、Intuitive(易懂)、Succinct(简介)、Effective(有效)、Expressive(表达力)

Linear Temporal Logic: LTL

LTL公式使用析取和否定的普通布尔连接词构造,并引入时序操作符next、previous、until和since。
$\varphi ::= (\varphi)|\neg\varphi|\varphi\vee\varphi|\varphi\wedge\varphi|\varphi U \varphi|\Box\varphi|\diamondsuit\varphi|\bigcirc\varphi|P$
$\bigcirc p$等同于$Xp$: $p$为真在下一个状态
$\diamondsuit p$等同于$Fp$: $p$为真在某个未来状态
$\Box q$等同于$Gq$: $q$为真在所有未来状态
$qUp$: $p$在某个未来状态为真,在所有状态$q$一直为真,直到 $p$为真
$P$为布尔变量

Explicit-State Model Checking

显式状态模型检验(Explicit-state model checking) 非常适合应用于软件验证,特别是交互异步进程系统的验证。

  • 基本的可达性分析最容易用于安全 属性的验证,例如不变量、断言的有效性,或者多进程系统中不存在死锁 。
  • 算法也可以用来证明活跃属性,包括所有可以在线性时序逻辑(LTL)中形式化的属性

使用Explicit-State Model Checking需要满足两个假设:

  • 作为验证目标的系统必须是有限状态的
  • 系统执行可以被建模为一个单独的状态转换序列。

抽象很重要

基本的搜索算法

(使用DFS)?
状态机定义$A={S,s_0,L,T,F}$

  • $S$是 状态的有限集,
  • $s_0$是S中的一个元素,称为初始状态,
  • $L$是一组符号,称为 标签集或字母表,
  • $T\subseteq S \times L \times S$是过渡集,
  • $F \subseteq S$是 最终状态集。
  • 自动机A接受任何以在$s\in F$状态下结束的有限执行。

BFS和DFS比较

  • 同:两种算法具有相同的计算复杂度
    • 在可达状态的数量上是线性
    • 这两种算法都可以在运行中工作,故不不需要预先知道可达图
  • 异:行为不同
    • DFS:必须存储在集合D中使反例生成更小。
    • DFS:很容易扩展,不仅支持安全性的验证,且支持活跃属性的验证,而不会增加搜索的计算复杂性。(显著优点)
    • BFS:生成的任何反例往往更小

$\omega$自动机

任何LTL公式都可以机械地转换为Büchi自动机$B={S,s_0,L,T,F}$。$B$接受执行序列$\sigma$,当且仅当$\sigma$包含集合$F$的无穷多个状态时。即Büchi只接受无限序列。

模型检验的问题
给定一个系统A,形式化为一个有限自动机 A,和一个Büchi自动机B, 形式化满足LTL公式的A的所有执行。在两个自动机接受的语言的交集中找到一个接受运行的问题。

A 和B的交集是通过计算A × B得到的,A × B是一个Büchi 自动机。

有限状态自动机A和B的同步积为有限状态自动机$P={S’,s_o’,L’,T’,F’}$

  • $S’=A.S\times B.S$
  • $s_0’=(A.s_0,B.s_0)$
  • $L’=A.L\times B.L$
  • $T’\in S’\times L’\times S’$, 其中$((A.s,B.t),(e,f ),
    (A.s′,B.t′)) ⊆ T′,\ (A.s,e,A.s′) ∈ A.T, \ and (B.t,f,B.t′) ∈ B.T$
  • $F’\subseteq A.S × B.S$,对于每一对$(e, F)\in F’$有$e\in A.F\wedge F\in B.F$

形式化如下

  • 将LTL公式$f$转换为相应的Büchi自动机$B$。
  • 计算A0,…,AN的 交叉积(interleaving product) A。
  • 计算$A \times B$的同步积(synchronous product) P。
  • 使用Büchi接受规则找到自动机P的接受运行。

Nested depth-first search(嵌套DFS?)

可以用嵌套的深度优先搜索算法有效地解决。在P中是否存在至少一个可到达的最终状态,也可以从它自身到达?

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
Open D = {}; // ordered set
Visited V = {};

State seed = nil;

start()
{ V!s0,0; D!s0,0;
ndfs(); // start the first search
}

ndfs()
{ Bit b; // b=0: first search, b=1: nested search
D?s,b;

foreach (s,e,s’) in T
{ if (s’ == seed) // seed reachable from itself
{ liveness_violation(); return;
}
if !(s’,b ∈ V) // if s’ not reached before
{ V!s’,b; D!!s’,b; ndfs(); // continue search
} }

// in post-order, in first search only

if (s ∈ F && b == 0)
{ seed = s; // a reachable final state
D!!s,1; // push s on stack D
ndfs(); // start the nested search
seed = nil; // nested search completed
} }

算法中的符号定义:

  • $X!y$将y添加到集合X中;如果X是有序的,那么它将y作为X的最后一个元素,
  • $X!!y$将y添加到集合X中;如果X是有序的,那么它将y作为X的第一个元素,
  • $X?y$从集合X中移除一个元素并命名为y;如果X有序,则删除的元素是X中的第一个元素,如果X为空,则操作返回空元素 $\emptyset$ 。

Binary Decision Diagrams

使用真值表或者二进制决策树来表示二进制布尔变量情况,其复杂度是指数倍增长的。采用二进制决策图来表示可以降低复杂度

**二进制决策图(BDD)**:将布尔函数表示为无环有向图,

  • 非终端顶点用布尔变量标记
    对于非终端顶点$v$,其变量记为$var(v)$,而对于叶顶点$v$,其值记为$val(v)$。
    每个非终端顶点v都有两条出边:$hi(v)$,变量值为1;$lo(v)$变量值为0。
  • 叶子顶点用值1和0标记。
    我们将$hi(v)$和$lo(v)$称为顶点$v$的$hi$和$lo$子结点。这两个叶结点被称为$1-leaf$和$0-leaf$。

    Definition 1 (BDD) Reduced ordered BDDs are canonical representations of Boolean propositional formulas. The BDD for a formula f , denoted by Bdd(f ), is a directed acyclic graph (DAG).

BDD相关规则

ODBB表示布尔函数的规则:
将函数$f_v$与图中的每个顶点$v$相关联来定义由BDD表示的布尔函数。BDD中的每个顶点都表示一个布尔函数

  • 对于两个叶子,相关联的值是 1 (1-leaf)和0 (0-leaf)。
  • 对于非终端顶点v,相关的函数定义为为$f_v = (var(v) \wedge f_{hi(v)}\vee (\neg var(v) ∧ f_{lo(v)}).$

对于有序二进制决策图(obdd),我们对与图顶点相关的变量强制执行一个排序规则 。(不同的排序规则会导致不同的BDD大小)

  • 对于每个顶点$v$有 $var(v) = x_i$,对于顶点$u\in {hi(v),lo(v)}$有$var(u) = x_j$且必须 $i < j$。

树表示

OBDD表示
(x1 ∧ x2 ∧ ¬x3) ∨ (¬x1 ∧ x3) 的表示。
图中,我们将lo子结点的弧表示为虚线,将hi子结点的弧表示为实线。

简化的OBDD定义为满足以下规则的OBDD:

  1. 一个叶子最多只能有一个给定的值。
  2. 不可能有顶点v使得$hi(v) = lo(v)$。一个节点的两个孩子不能指向一个地方。
  3. 不可能存在不同的非终端顶点u和v,使得$var(u) = var(v), hi(u) = hi(v), lo(u) = lo(v)$。没有另外一个节点跟当前节点表达同一个意思

化简为reduced OBDD的规则

  1. 如果叶u和v有val(u) = val(v),那么消除其中一个,并将所有传入的边重定向到另一个。
  2. 如果顶点v具有lo(v) = hi(v),则消除顶点v并将所有传入的边重定向到它的子顶点。
  3. 如果顶点u和v有var(u) = var(v), hi(u) = hi(v), lo(u) = lo(v),那么消除其中一个顶点,并将所有传入的边重定向到另一个顶点。

布尔函数抽象数据类型的基本操作

图中$f$和$g$表示布尔函数(用obdd表示),$i$是 1到n之间的变量索引,$b$是0或1, $\bold{a}$是n个0和1的向量。索引$I\subseteq {1,…,n}$,$X_I$表示对应的一组变量${x_i|i\in I}$
| 操作 | 结果 | 解释 |
| :—————– | :——————————————- | :———————– |
| 基本函数 |
| $CONST(b)$ | $\bold{1} (b = 1)\ or\ \bold{0} (b = 0)$ |
| $VAR(i)$ | $x_i$ |
| 代数运算 |
| $NOT(f)$ | $\neg f$ |
| $AND(f,g)$ | $f \wedge g$ |
| $OR(f,g)$ | $f \vee g$ |
| $XOR(f,g)$ | $f \oplus g$ |
| 非代数操作 |
| $RESTRICT(f,i,b)$ | $ f\vert_{x_i} \leftarrow b$ | 把$x_i$值替换成0或1 |
| $COMPOSE(f,i,g)$ | $ f \vert_{ x_i} \leftarrow g $ | 把$x_i$值替换成布尔函数g |
| $EXISTS(f,I)$ | $ \exist X_I.f$ |
| $FORALL(f,I)$ | $ \forall X_I.f$ |
| $RELPROD(f,g,I)$ | $ \exist X_I.(f \wedge g)$ |
| 检验函数 |
| $EQUAL(f,g)$ | $ f = g$ |
| $EVAL(f,\bold{a})$ | $ f (\bold{a})$ |
| $SATISFY(f )$ | some $\bold{a}$ such that $f (\bold{a}) = 1$ |
| $SATISFY-ALL(f )$ | $ {\bold{a} \vert f (\bold{a}) = 1}$ |

APPLY算法

Apply算法,一种实现二进制布尔代数运算的通用方法。
在从递归调用返回时从下往上生成一个简化的OBDD 。

image

变量排序和重组

有些函数对变量排序非常敏感,甚至出现从线性到变量数量的指数级的复杂度的差异。
使用相邻变量的成对交换作为基本操作,大多数OBDD库通过称为筛选 [59]的过程实现动态变量排序。单个变量或一小组变量[57],通过相邻变量交换序列在排序中上下移动,直到确定产生的位置(总顶点数可接受)。在筛选的原始公式中,变量在整个可能的位置范围内移动,然后返回到使整体OBDD大小最小化的位置。

表示非布尔函数

OBDD的关键属性:

  • 主要是通过子图的共享实现了紧凑性,,
  • 关键操作可以通过图算法实现,
  • 表示的函数的属性可以很容易地测试。

无界域上的函数
当一个函数变量x在一个无限大的定义域D上时,我们不能简单地用一组二进制值来编码它的可能值,或者向决策图的顶点添加多个分支。然而,在某些应用程序中,只需要捕获状态变量的一组有界属性。
差异决策图(DDDs:Difference Decision Diagrams (DDDs))
差分约束:每一种形式为$x_i−x_j≤c$或$x_i−x_j < c$,其中$x_i$和$x_j$为时钟变量,c为整数或实值。
| image | image | image |
| :————————————————————————————– | :——————————————————————————————————— | :—————————————————————————————————– |
| $C_1 = (x_1 − x_2 > 4) ∧ (x_1 − x_3 ≤ 12)$
$C2 = (x_1 − x_2 ≤ 4) ∧ (x_2 − x_3 ≤5)$ | $C_1 = (x_1 − x_2 > 4) ∧ (x_1 − x_3 ≤ 12)$
$C’_2 = (x_1 − x_2 ≤ 4) ∧ (x_2 − x_3 ≤ 5) ∧ (x_1 −x_3>10)$ | $C_1 = (x_1 − x_2 > 4) ∧ (x_1 − x_3 ≤ 12)$
$C_2’’ = (x1 − x2 ≤ 4) ∧ (x2 − x3 ≤ 5) ∧ (x1 − x3 ≤ 9)$ |

差分决策图(DDD)示例。顶点由差分约束标记

BDD-Based Symbolic Model Checking

  • BDDs用于符号表示所分析的自动机或Kripke结构的转换关系,以及由模型检查算法控制的状态集。
  • 表示和操作转换关系及状态集对于实现广泛的时序逻辑的模型检查算法是足够的

基于bdd的符号模型检查对形式化验证和形式化方法的影响。

  • 首先,它实现了工业系统的实际验证。
  • 其次,它导致了bdd的重要发展,例如新类型的bdd[22],变量排序启发式[2,24]和高效实现[31]。
  • 最后,它为其他形式的符号模型检查铺平了道路,

image
一个Kripke结构和一个BDD的转换关系 (虚线和实线分别表示BDD中的0和1边)

状态集 和 关系的表示

状态集的表示

对于任意$X⊆S$,特征函数$[[X]]$用命题公式$f (X)$表示,定义为:$f (X) = \bigvee\limits_{s∈X}\chi (s)$
形式上,设$\chi$为从S到minterms的映射,定义为:$\chi(s) = l_1 ∧ ··· ∧ l_k\ where\ l_i =\left{\begin{matrix} p_i & if\ p_i ∈ L(s) \ \neg p_i & otherwise \end{matrix}\right.$
以上图Kripke结构图为例。
$χ(s0) = p ∧ ¬q,\ χ(s1) = p ∧ q,\ χ(s2) = ¬p ∧ q,\ χ(s3) = ¬p ∧ ¬q$
让$X = \emptyset, Y = {s0,s1}, and Z = {s1,s3}$.那么 对应的特征函数的符号表示为:
$\begin{matrix} f (X) = FALSE & f (Y) = (p ∧ ¬q) ∨ (p ∧ q) = p &
f (Z) = (p ∧ q) ∨ (¬p ∧ ¬q)\end{matrix}$

关系的表示

对于任意$R⊆S × S$,特征函数$[[R]]$用命题公式$f (R)$表示为:$f (R) = \bigvee\limits_{(s, t)∈R}\chi (s, t)$

为了表示转换关系$R⊆S × S$,我们引入了一组新的原子命题$AP’ = {p_1’,…, p_k’}$。$p$为当前状态中的$p$,$p’$为当前状态可转换到的下一个状态中的$p$。
对于AP上的公式$f$,$Prime(f )=f [p_1,…,p_k/p_1′ ,…,p_k′]$,$UnPrime(f ) = f [p_1′ ,…,p_k′ /p_1,…,p_k]$
使用BDD 重命名操作将这些操作提升到BDD。我们现在将χ扩展为S × S与 minterms集合对AP∪AP’的双射:$χ(s,t) = χ(s) ∧ Prime(χ(t))$

上图右侧为以下关系的BDD表示:
$f (R) =(p ∧ ¬q ∧ p’ ∧ q’) ∨ (p ∧ ¬q ∧ ¬p’ ∧ q’) ∨ (p ∧ q ∧ p’ ∧ q’)
∨ (p ∧ q ∧ ¬p’ ∧ q’) ∨ (¬p ∧ q ∧ ¬p’ ∧ ¬q’) ∨ (¬p ∧ ¬q ∧ ¬p’ ∧ ¬q’)
\=(p ∧ q’)∨ (¬p ∧ ¬p’ ∧ ¬q’)$

图像运算

图像和预图像计算——即分别计算一组状态的后继集合或前身的集合——是任何模型检查算法的基本操作

给定一组状态S,转换关系R下S的图像用Image (S,R)表示 ,定义为:
$Image(S,R) = {t \vert ∃s ∈ S_▪ (s,t) ∈ R}$ ,是过渡关系R中从S一步可达的状态集。

设$\bold{S}$和$\bold{R}$分别是$\bold{S}$和$\bold{R}$用 BDD 对$AP$和$AP∪AP’$的符号表示。然后计算 $Image(\bold{S,R})$的符号表示,记为$BDDIMAGE(\bold{S,R})$,计算公式如下:
$BDDIMAGE(\bold{S,R}) = UnPrime(∃AP_▪ \bold{S ∧ R})$

首先为S和R的合取构造BDD,然后使用存在量化投射所有的预状态变量$AP$,最后 将结果从$AP’$重命名为$AP$变量。

以$BDDIMAGE(\bold{S,R})$为例,其中$R$为s上图中Kripke结构的跃迁关系,$\bold{S} = {s0}$:
$$
\begin{align*}
& BDDIMAGE(S,R)\
& = UnPrime(∃p,q_▪ (p ∧ ¬q) ∧ ((p ∧ q′) ∨ (¬p ∧ ¬p′ ∧ ¬q′)))\
& = UnPrime(∃p,q_▪ (p ∧ ¬q) ∧ (p ∧ q′))\
& = UnPrime(q’) = q = Bdd(f ({s1,s2}))
\end{align*}
$$
$(p ∧ ¬q)$为$S_0$,$((p ∧ q′) ∨ (¬p ∧ ¬p′ ∧ ¬q′)))$为化简后的转换关系符号表示$f(R)$

$R$下$S$的预像记为$PreImage(S,R)$,定义为:$PreImage(T,R) = {s | ∃t ∈ T_▪ (s,t) ∈ R}$
$PreImage(S,R)$是由转换关系R的一步可以到达$S$中某个状态的所有状态的集合,给定T和R的符号表示T和R,$PreImage(T,R)$的符号表示为 $BDDPREIMAGE(T,R)$,计算公式如下:
$BDDPREIMAGE\bold{(T,R)} = ∃AP′ ▪ \bold{R} ∧ Prime(\bold{T})$

以$BDDPREIMAGE(\bold{T,R})$为例,其中$R$为s上图中Kripke结构的跃迁关系,$\bold{T} = {s_1,s_2}$:
$$
\begin{align*}
&BDDPREIMAGE(T,R) \
&= ∃p′,q′ ▪ ((p ∧ q′) ∨ (¬p ∧ ¬p′ ∧ ¬q′)) ∧ Prime(q)\
&= ∃p′,q′ ▪ (p ∧ q′) ∧ q′\
&= p = Bdd(f ({s0,s1}))\
\end{align*}
$$

分区转换关系

通常在实践中,即使$R, S$和$Image(S,R)$具有有效的BDD表示,中间结果也非常大。这通常被称为 图像计算的“驼峰”。在这种情况下,需要将转换关系$R$划分为一组BDDs,并直接对这样一个已分区的关系进行操作。

析取分解 Disjunctive Decomposition

当R是几个转换关系异步组合的结果时,通常会出现这种情况。
存在量词下的析取:$∃X ▪ A ∨ B ⇐⇒ (∃X ▪ A) ∨ (∃X ▪ B)$
假设R为一组BDD的集合$\bold{R}=\bigvee\limits_{1\le i\le n }\bold{R}i$
$$\begin{align*}
BDDIMAGE(S,R) &= UnPrime(∃AP ▪ S ∧ R)\
&= UnPrime\left(∃AP ▪ S ∧\left( \bigvee\limits
{1≤i≤n} R_i\right)\right) \
&= \bigvee\limits_{1≤i≤n}\underbrace{UnPrime(∃AP ▪ S ∧ Ri)}{done\ one\ \bold{R}i\ at\ a time}\
\end{align*}
$$
$$\begin{align*}
BDDPREIMAGE(S,R) &= ∃AP’ ▪ Prime(S) ∧ R\
&= ∃AP’ ▪ Prime(S)\wedge \left( \bigvee\limits
{1≤i≤n} R_i\right) \
&= \bigvee\limits
{1≤i≤n}\underbrace{∃AP’ ▪ Prime(S) \wedge \bold{ R_i}}_{done\ one\ \bold{R}_i\ at\ a time}\
\end{align*}
$$

合取分解 Conjunctive Decomposition

当R是几个转换关系同步组合的结果时,通常会出现这种情况。
设X为一组变量,两个命题公式A、B且满足 $X\cap var(A) =\emptyset$。则$∃X ▪ A ∧ B ⇐⇒ A ∧ ∃X ▪ B$
假设R为一组BDD的集合 $\bold{R}=\bigwedge\limits_{1\le i\le n }\bold{R}i$
$$\begin{align*}
BDDIMAGE(S,R) &= UnPrime(∃AP ▪ S ∧ R)\
&= UnPrime\left(∃AP ▪ S ∧\left( \bigwedge\limits
{1≤i≤n} R_i\right)\right) \
&= UnPrime(∃V_1 ▪ (∃V_2 ▪ …∃Vn ▪ (S ∧ R_n)··· ∧ R_2) ∧ R1)\
&\text{where, for}\ 1 ≤ i ≤ n,\ V_i = AP ∩ \left(Var(R_i)/ \bigcup\limits_{1≤j<i}Var(R_j)\right)
\end{align*}
$$
$V_i$是原子命题p的集合,使得i是p出现在Ri中的最小值。
$$\begin{align*}
BDDPREIMAGE(S,R) &= ∃AP’ ▪ Prime(S) ∧ R\
&= ∃AP’ ▪ Prime(S)\wedge \left( \bigwedge\limits_{1≤i≤n} R_i\right) \
&= ∃V’1 ▪ (∃V_2’ ▪ ···∃V_n’ ▪ (Prime(S) ∧ R_n)··· ∧ R_2) ∧ R1\
& \text{where, for}\ 1 ≤ i ≤ n,\ V_i = AP’ ∩ \left(Var(R_i)/ \bigcup\limits
{1≤j<i}Var(R_j)\right)\
\end{align*}
$$

Kripke结构的Model Checking (!!!算法,对应书的P231)

我们假设M是一组原子命题AP上的Kripke结构$(S,R,L)$(即 我们的模型系统);R用BDD表示,M有一个指定的初始状态$s_0∈S$,用BDD $s_0$表示。

任何安全属性的模型检查都可以简化为表单$\bold{AG}p$的CTL公式的模型检查,其中p是单个原子命题。这是因为对任何安全属性的违反都可以简化为某些定义良好的坏状态的可达性。如果$M \models \varphi$,则$\varphi$被称为$M$的一个不变量。
判断$M \models \varphi$的算法如下:
工作原理是迭代计算从初始状态s0(第2-7行)可到达的状态集,然后检查是否存在不满足p (第8行)的可达状态。
判断M |= AGp

CTL Model Checking

每个CTL公式$\varphi$是一个状态公式。当且仅当M的初始状态$s_0$满足$\varphi$时,$M \models \varphi$

将CTL的语法限制如下,其中$\varphi、\varphi_1、\varphi_2$为CTL公式,$p\in AP$:
$\varphi = p | ¬\varphi_1 | \varphi_1 ∧ \varphi_2 | EX\varphi_1 | EG\varphi_1 | E(\varphi_1 U \varphi_2)$。
用⊥和⊤分别表示$(p_0∧¬p_0)$和$¬⊥$,其中$p_0\in AP $是一个特殊的原子命题。其他操作符使用标准的等价符替换。见 计算树逻辑(CTL)
CTL模型检测算法:
两步工作:

  • 使用辅助函数$CTLSTATES$来计算满足$\varphi$的关于M的状态集S;
  • 当且仅当$s0∈S$时返回true。
    CTL模型检测算法

    函数 EXSTATES(M,S) 使用章节中描述的PreImage方法计算S的前一状态集合。
    函数 EGSTATES(M,S) 迭代地计算一个状态集,该状态集存在一个只包含集合S中的状态的路径。
    函数 EUSTATES(M,S1,S2) 计算存在一条从S1到S2的路径的状态集。

SAT求解器(Propositional SAT Solving)

给定一个命题逻辑公式,确定是否存在一个变量赋值,使得公式的计算结果为真,这被称为布尔可满足性问题,通常缩写为SAT(Boolean Satisfiability Problem)。

  • 是一个NP完备问题。
    • 不太可能存在任意多项式的SAT算法
    • 不排除找到足够高效的算法的可能性
  • 完整的SAT求解者可以找到一个解(即一个令人满意的变量赋值)或证明不存在解。对于许多其他领域,包括使用模型检查的验证,主要任务是证明实例的不可满足性
  • 随机方法不能证明实例是不可满足的,即使他们可能能够为某些类型的可满足实例快速找到解决方案。

    相关知识

    布尔公式$\mathcal{F}$是在一组 命题变量是用标准逻辑连接词,¬,∧,∨归纳定义的,如下:
  • 原子(atom)$x$是布尔公式。
  • 如果$\mathcal{F}$是一个布尔公式,则$(¬\mathcal{F})$是一个布尔公式。(当$\mathcal{F}$表示一个原子$x$时,$¬\mathcal{F}$用$\overline{x}$表示。)
  • 如果$\mathcal{F}$和$\mathcal{G}$是布尔公式,那么$(\mathcal{F}∨\mathcal{G})$也是布尔公式。
  • 如果$\mathcal{F}$和$\mathcal{G}$为布尔公式,则$(\mathcal{F}∧\mathcal{G})$为布尔公式。

表达方式:

  • 合取范式( conjunctive normal form (CNF))
    任何命题公式,最终都能够化成$ (A 1 ∨A 2 )∧(A 3​ ∨A 4 ) $的形式
  • 析取范式(disjunctive normal form (DNF))
    任何命题公式,最终都能够化成 $( A 1 ∧ A 2 ) ∨ ( A 3 ∧ A 4 )$的形式

给定一个公式$\mathcal{F}$,一个真值赋值$\mathcal{ν}$是一个从变量$\mathcal{F}$到$ {0,1}$的映射,$\mathcal{ν}: var(\mathcal{F}) \mapsto {0,1}$。公式所取的值(公式结果)为$\mathcal{F^v}$

  • 如果存在一个字面量$l\in c$,使得$l^ν = 1$,则子句$c$是满足的(satisfied)。
  • 如果所有$c$中的字面量取值都为0,则子句$c$是假的(falsified)。
  • 除一个字面值赋值为0外,其余的字面值未赋值,那么这个子句是单元(unit)。
  • 如果一个子句既没有 falsified ,也没有被satisfied,也没有unit,那么它就是未解决的unresolved。
  • 如果所有子句都satisfied,那么CNF公式satisfied。如果有至少一个子句falsified,那么CNF公式falsified。
  • 如果 $\mathcal{F^v} = 1$,则F的真值赋值是令人满意satisfying的(或简单地说是令人满意的真值赋值 a satisfying truth assignment)。公式F是可满足的前提是它有一个令人满意的真值赋值;否则是无法满足的。如果公式F是可满足的,则为$F \models\mkern-15mu/ ⊥$。如果公式F是 不满足的,则$F⊨⊥$。

SAT求解器中的一个关键程序是单元子句规则unit clause rule:

  • 如果子句是单元,那么它唯一未赋值的字面量必须赋值1才能满足子句。
  • 单元子句规则的迭代应用称为单元传播(unit propagation)或 布尔约束传播(BCP:Boolean constraint propagation)。
  • 如果识别出一个falsified的子句,则声明冲突条件,且算法回溯。

在CDCL SAT求解器中,每个变量x由许多属性来描述,包括值(value)、前项(antecedent)子句(或仅仅是前项)和决策级别(decision level),分别用$ν(x)∈{0,u,1}, α(x)∈F∪{NIL}和 δ(x)∈{−1,0,1,…,| x |}$表示。

  • 一个变量x被作为应用单位子句规则的结果赋值,则被称为被推导的(implied)。用于推演变量x的单元子句c被认为是x的前项子句,$α(x) = c$。
  • 变量x的决策级别表示该变量被赋值为{0,1}的决策树的深度。未分配变量x的决策水平为−1,$δ(x) =−1$。
    image
    上图示例中,除了决策级别0之外,一个决策文字与每个决策级别相关联。例如,对于决策 级别1,决策文字为w,表示w被赋值为1。给定推导图,可以从传入边推断给定推导赋值的前项。例如,b被赋值为 1,因为a和x被赋值为1。因此,b的先行项是$(\overline{x}\vee \overline{a}\vee \overline{b})$。

    CDCL SAT Solvers

    Organization

    image

算法1显示了CDCL SAT求解器的标准组织,它基本上遵循DPLL的组织。与DPLL主要的区别是每次识别冲突时调用CONFLICTANALYSIS函数 ,以及在发生回溯时调用BACKTRACK。此外,BACKTRACK过程允许非按时间顺序进行回溯

  • UNITPROPAGATION由单元子句规则的迭代应用组成。如果识别出falsified的子句,则返回冲突指示。
  • PICKBRANCHINGVARIABLE由选择一个变量并为其赋值组成。
  • CONFLICTANALYSIS包括分析最近的冲突,并从冲突中学习一个新的从句。
  • BACKTRACK返回到由CONFLICTANALYSIS计算的决策级别。
  • ALLVARIABLESASSIGNED 测试是否所有变量都已赋值,在这种情况下,算法终止,表明CNF公式是可满足的。

    Clause Learning and Non-chronological Backtracking

    算法2总结了冲突分析(和 学习)过程的主要步骤。输入参数是CNF公式和当前赋值集。
  • 从⊥顶点(表示已证伪的子句)开始遍历当前决策级别上可推导的字面量。
  • 对于每个遍历的字面量,将分析先行词中的字面量。
    • 在比当前决策级别低的决策级别分配的字面量将记录其补充字面量,
    • 而在当前决策级别分配的字面量将被安排遍历。
  • 重复该过程直到访问当前决策级别的分支变量。

image

图2显示了一个产生冲突的单元传播的简单示例。x推出a,z推出a、b,a、b导致冲突发生。
图3显示了冲突学习算法的处理过程。从冲突节点⊥开始。a、b、 和z会被访问,因为它们都分配在决策级别3。记录的文字是$\overline{x}$和$\overline{z}$。因此,所创建的子句是$(\overline{x}∨\overline{z})$。
图4还显示了 回溯后的结果。
| image | image | image |
| :——————————————————————————– | :——————————————————————————– | :——————————————————————————– |

SAT-Based Model Checking

Modern satisfiability (SAT)求解器已成为许多模型检查器的核心技术。

  • 与基于bdd的模型 检查器相比,大大提高了容量。
  • SAT解算器通常能够解决比基于二进制决策图(bdd)的经典技术更大的公式
  • 基于bdd的技术允许有效地实现量词消除,这对于符号定点算法中的终止检查至关重要。

SAT-based bounded modelchecking (BMC) 有界模型检验?

  • 转换系统和属性的符号表示在给定的K个步骤中一起展开
  • 如果存在长度k以内的反例,则得到一个可满足的公式。
  • 然后,公式被传递给一个有效的SAT求解器。

Bounded Model Checking on Kripke Structures

这里仅限于线性时序逻辑(LTL)中给出的属性。
安全属性(Safety Properties):
$\bold{G}p$:对于这种性质,可以被给出满足¬p的状态s结束的有限路径作为反例。
$$
\exists s_{0}, \ldots, s_{k} . \quad I\left(s_{0}\right) \wedge \bigwedge_{i=0}^{k-1} T\left(s_{i}, s_{i+1}\right) \wedge \neg p\left(s_{k}\right) \quad(1)
$$
第一个连接符$I\left(s_{0}\right)$确保 状态$s_0$是初始状态之一。第二个连词对需求进行编码,即对于每个$i∈{0,…,k−1}$有从$s_i$到$s_{i+1}$的换。这相当于创建了转换关系T的k个副本。最后,连接符$\neg p\left(s_{k}\right)$断言状态$s_k$满足$¬p$ 。
活跃属性(Liveness Properties):
$\bold{F}p$:这种形式的属性的反例总是可以给出一个有限(可能是空的)前缀(称为词干),后面跟着一个有限循环。路径上的所有状态满足¬p。
$$
\exists s_0,\ldots,s_k.\quad I(s_0)\wedge\bigwedge\limits_{i\equiv0}^{k-1}T(s_i,s_{i+1})\wedge\bigwedge\limits_{i=0}^{k-1}\neg p(s_i)\wedge\bigvee\limits_{i\equiv0}^{k-1}s_k=s_i\quad(2)
$$

Combining Model Checking and Testing

模型检查是一种基于穷举状态空间探索的形式验证
在实践中,验证保证往往是有限的:仅检查程序或程序模型的特定属性,在一些特定的环境假设下,检查本身通常是近似的。

模型检查应该更多地被视为“超级测试”,而不是严格数学意义上的形式验证:提供更好的覆盖范围,计算成本更高,在测试和正式验证之间提供了一个有吸引力的实际权衡

模型检查的关键实用优势在于,它能够发现极其难以发现的bug

软件模型检查的两种主要方法:
image

  • 一种方法使用抽象 abstraction:它包括通过静态分析其代码自动从软件应用程序中提取抽象模型,然后使用传统的模型检查算法分析该模型。
  • 另一种方法使用适配adaptation:包括将模型检查调整为一种适用于工业规模软件的系统测试形式

顺序软件的系统测试

符号执行是指用符号值而不是具体值执行程序。赋值语句表示为其(符号)参数的函数,而条件语句 表示为对符号值的约束。可用于错误检测、程序修复、调试、维护和故障本地化。

测试生成的方式:

  • 静态测试生成是对程序进行静态分析的过程符号执行技术,试图计算驱动器的输入P沿着特定的执行路径或分支,而无需执行程序。
    • 静态测试生成不能通过条件语句的任何分支生成测试输入来驱动 程序模糊的执行:静态测试 生成对于这样的程序是无用的。
  • 动态测试生成执行程序p,它由执行程序P组成,通常从一些随机输入开始,同时动态执行符号执行,在执行过程中从分支语句中的谓词收集输入上的符号约束,然后使用约束求解器推断出前一个输入的变体,以便引导程序的下一次执行转向替代程序分支。
    • 符号执行现在是具体执行的附属品。
    • 使用具体值和随机化可以缓解符号执行的不精确性
    • 动态测试生成是目前已知的最精确的代码驱动测试生成形式

动态测试生成示例1:

1
2
3
4
int obscure(int x, int y) {
if (x == hash(y)) abort(); // error
return 0; // ok
}
  • 最初x =33. y = 42.
  • 假设hash(y)=567,路径约束变为$\phi_{\rho}=(x \neq 567)$
  • 新的输入向量x=567.y=42

动态测试生成示例2:
image
考虑图5所示的函数h。函数h是有缺陷的,因为它对其输入向量 (由输入参数x和y组成)的某个值可能导致中止。但使用随机值运行x和y的程序不太可能发现错误。

  • 最初,x=269167349,y=889801541
  • 符号动态执行产生路径约束$\phi_{\rho}=(x\neq y)\wedge(2\cdot x\neq x+10)$。
  • 对当前路径约束的最后一个约束求反得到约束 $\phi_{\rho}’=(x\neq y)\wedge(2\cdot x= x+10)$
  • 新的路径约束的解是(x = 10,y = 889801541)。

优势与局限

优势:

  • 即使定向搜索通常不能在合理的时间内探索大型程序的所有可行路径,但它通常比纯随机测试获得更好的覆盖率,因此可以发现新的程序错误。
  • 可以增量地实现

在高层次上,系统动态测试生成受到两个主要限制:

  • 沿个别路径符号执行的频繁不精确,以及
  • 通常需要探索的大量路径,或者路径爆炸。

挑战

  • 从符号执行的不精确中恢复
  • 将符号执行扩展到数十亿条指令,有效地检查许多属性
  • 有关指针、不同大小的输入、浮点指令、无限循环的原因
  • 优先搜索
  • 跨代码更改重用以前的分析结果

数据输入并发软件的系统测试

jCUTE是一种动态测试生成技术:

  • 生成一个随机输入和一个计划,计划指定线程的执行顺序
  • 回溯并生成一个新的调度或新的输入,并再次执行程序
  • 继续执行,直到使用深度优先搜索策略探索了所有可能的不同执行路径

image

  1. Z=2345354且顺序$(t_1,1) (t_2,, 1) (t_2,2)$是约束$〈2 ∗ z_0 + 1! = 2〉$的唯一执行路径
  2. 约束求反$2 * z_0 +1 = 2$,仍无解
  3. 回溯并生成一个调度,以便下一次执行变成$(t_2,, 1) (t_2,2)(t_1,1) $
  4. 再次回溯(t2,1)(t1,1)(t2,2) 路径约束为$〈2 ∗ z_0 + 1! = 3〉$
  5. 负约束$2 ∗ z0 + 1 = 3$有解$z0 = 1$
  6. (t2,1)(t1,1)(t2,2)(t2,3)导致中止

反例引导的抽象细化 (CEGAR:CounterExample-Guided Abstraction Refinement)

书13.5章

Partial-Order Reduction

书6章

  • 版权声明: 本博客所有文章除特别声明外,著作权归作者所有。转载请注明出处!

扫一扫,分享到微信

微信分享二维码
  • Copyrights © 2022-2024 Konsin
  • 访问人数: | 浏览次数:

请我喝杯咖啡吧~

支付宝
微信