精化(refinement)方法已在理论研究和工程实践中被广泛应用,一般过程是通过对抽象模型的逐步求精得到具体的系统实现,系统实现和抽象模型间即存在精化关系.两者均能满足某种性质,使得系统实现在代替抽象模型时能够保持一致性和正确性.在形式化验证方面,利用精化关系的验证(以下称精化检测)是一种十分重要的手段,代表性的精化检测工具FDR^[1]成功应用于学术界和工业界.精化检测方法可实现完全自动化:首先,对系统实现和规约用相同形式化语言进行建模,其中,规约代表系统需要满足的某种性质,只要证明系统实现和规约这两个模型间存在精化关系,并且该精化关系足以维持该性质,则系统实现一定满足规约.

为了验证不同类型的性质,如安全性(safety)和活性(liveness),已提出一系列不同的精化关系,包括traces精化、stable failures精化和failures-divergences精化关系等^[2].其中,安全性代表系统始终应保持安全状态,其验证通过traces精化关系实现;活性代表系统最终会达到的状态,其验证通过stable failures精化或failures- divergences精化关系来实现^[3].FDR^[1],PAT^[4]等工具支持上述精化检测,其主要过程为:将两个CSP进程转化成带标签的转移系统(labeled transition systems,简称LTS);然后,根据指定的语义模型(traces,failures,divergences等)证明一个进程与另一个进程是否存在精化关系.

标签转移系统LTS可以被认为是非确定型有穷自动机NFA.精化检测依赖于经典的子集构造方法,即:将NFA确定化,构造成一个确定型有穷自动机DFA.精化检测根据由系统模型转化的NFA与规约模型转化的DFA做同步求精操作,生成乘积自动机,并将问题转换为乘积自动机中的可达性问题.如果在乘积自动机中访问到了一个问题状态,则视为找到了一个反例,亦即精化关系不成立.在最差情况下,与NFA相比,DFA的状态数量呈指数级增长,因此,精化检测面临着状态空间爆炸问题.近年来,有关学者针对 NFA语言包含问题提出了基于模拟关系的方法^{[5, 6]}.该方法的主要思想为:不存储全部访问过的状态,只存储最大状态集合,并且满足状态空间中任意状态都能被这个最大状态集合中的某个状态模拟.因此,利用该方法能够避免完全的子集构造,从而减少不必要的搜索,极大地缩减状态空间.由于上述所有精化检测算法都是基于子集构造,很自然地,我们可以将基于模拟关系的方法应用到精化检测算法中.

针对精化检测常见的3种算法,即traces精化检测、stable failures精化检测和failures-divergence精化检测算法,本文在研究基于模拟关系的traces精化检测^[6]基础上,提出了基于模拟关系的stable failures和failures- divergence精化检测,提高了检测性能,并且证明了运用模拟关系后精化检测算法的正确性.即:在只访问部分状态的情况下,反例不会丢失.我们将基于模拟关系的精化检测算法集成到了PAT模型检测工具中,并以on-the-fly的可达性算法验证精化关系.实验结果表明,基于模拟关系的精化检测算法效率大大提高.

另一方面,已有学者将traces精化检测扩展到了概率系统中,称为概率精化检测^[7].其主要思想为:给定一个带概率的系统模型(用Markov decision process表示)和一种非概率的规约模型(用LTS表示),概率精化检测可以计算系统实现能够正确执行规约的概率(规约代表系统应该执行的行为).本文则将精化检测扩展到了时间系统中,即:给定带有时间约束的系统模型(用时间自动机timed automata表示,以下简称TA)和规约模型LTS,时间精化检测验证在有时间限制的情况下,系统能否正确执行规约规定的行为.该方法为文献^[8]关于时间自动机语言包含问题的扩充,其差别为规约模型的不同使得验证的系统性质不同.

本文第1节给出精化检测相关定义,并描述基于模拟关系的traces精化检测算法.第2节详细描述基于模拟关系的stable failures精化检测和failures-divergence精化检测算法.第3节给出基于模拟关系的时间自动机精化检测算法.第4节基于PAT工具和基准系统进行对比实验,说明利用模拟关系能够极大地提高精化检测算法性能.第5节为相关工作.最后总结并展望本文工作.

1 . 精化检测和模拟关系 1.1 定 义

首先给出LTS及其相关定义^{[9, 10]}.令S为可见事件的集合,τ为内部事件(或称隐藏事件),S_t为可见事件和内部事件的集合.

定义1. LTS L是四元组(S,init,Act,τ),其中,S是状态集合,init$\in $S是S中的初始状态,Act⊆S_t是事件集合,τ⊆SxActxS是所有带标签的转移关系的集合.

τ中的转移(s,e,s')被记为$s\buildrel e \over \longrightarrow s'$.LTS是确定化的,当且仅当对所有的s,e(s$\in $S且e⊆S_t),如果τ中存在$s\buildrel e \over \longrightarrow u$和$s\buildrel e \over \longrightarrow v$,则u=v.表达式enable(s)表示集合$\{ e|\exists s'.s\buildrel e \over \longrightarrow s'\} $,即,从状态s出发的转移上所有事件的集合.给定由状态组成的有穷序列〈s₀,s₁,…,s_n〉满足对所有整数i,${s_i}\buildrel \tau \over \longrightarrow {s_{i + 1}}$成立,并且令u=s₀,v=s_n,则该序列可以用uav来简单表示.假设在L中,uau',u'av'以及v'av成立,则记为$u\mathop \mapsto \limits^e v$.一系列事件的有穷序列被记为〈e₀,e₁,…,e_n〉,当且仅当L中存在由状态和事件组成的有穷序列〈s₀,e₀,s₁,e₁,…,e_n,s_n+1〉,使得对所有整数i,${s_i}\buildrel {{e_i}} \over \longrightarrow {s_{i + 1}}$成立,并且s₀=init,则称〈e₀,e₁,…,e_n〉是L的一条trace.L中所有trace的集合用符号traces(L)来表示.

接下来给出模拟关系的基本定义.令F⊆S为目标状态集合.给定S中的两个状态s₀和s₁,关于F,s₀被s₁模拟

(记为s₀ps₁),需满足:如果s₀$\in $F,则s₁$\in $F;对任意e$\in $S_t,如果$({s_0},e,{s'_0}) \in T$,则一定存在$({s_1},e,{s'_1}) \in T$,使得${s'_0}$被${s'_1}$模拟.

定义2. 设L₁=(S₁,init₁,Act₁,τ₁)和L₂=(S₂,init₂,Act₂,τ₂)为两个LTS,满足τ$\notin $Act₂.L₁和L₂的乘积自动机被记为L₁xL₂,也是一个LTS L=(S,init,Act,τ),其中,S=S₁xS₂;init=init₁xinit₂;Act=Act₁$\cup $Act₂;τ是一个带标签的转移关系,满足以下两个条件:

(1) 给定S中的乘积状态(s₁,s₂),如果$({s_1},\tau ,{s'_1}) \in {T_1}$,则$(({s_1},{s_2}),\tau ,({s'_1},{s_2})) \in T;$

(2) 给定S中的乘积状态(s₁,s₂),如果$({s_1},e,{s'_1}) \in {T_1},({s_2},e,{s'_2}) \in {T_2}$并且e≠τ,则$(({s_1},{s_2}),e,({s'_1},{s_2})) \in T.$

1.2 Traces精化检测

定义3. 设L₁和L₂为两个LTS.L₁和L₂之间存在traces精化关系,当且仅当traces(L₁)⊆traces(L₂)^{[9, 10]}.

前文已经提到,traces精化检测的标准算法基于子集构造.因此需要将L₂转化成一个确定化的LTS,其与确定化前的LTS具有完全相同的traces集合,并且该系统中消去了τ事件.确定化过程定义如下:

定义4. 设L=(S,init,Act,τ)为一个LTS.L的确定化后的LTS是四元组det(L)=(S',init',Act',τ'),其中,S'⊆2^S;init'={s|initas};Act'=Act\{τ};τ'是转移关系,满足:(N,e,N')$\in $τ'当且仅当$N' = \{ s'|\exists s:N.{\rm{ }}s\mathop \mapsto \limits^e s'\} .$

由以上定义可知:在det(L)中,同一个trace所到达的所有状态被合并成了集合.因此,det(L)中从某个状态集合出发,经过一个事件只能到达唯一一个确定的状态集合.给定L₁和L₂,标准的traces精化检测算法过程为:构建(通常是on-the-fly的方式)乘积自动机L₁xdet(L₂),然后,在L₁xdet(L₂)中查找状态(s₁,s₂)(其中,s₁是L₁的一个状态,s₂是L₂的一个状态集合),如果s₂是空集,则traces精化关系不成立.这样的目标状态被称为TR-目标状态.在最差情况下,这个方法的复杂度随着L₂的状态数量呈指数级增长.

1.3 基于模拟关系的traces精化检测

给定L₁和L₂,基于模拟关系的traces精化检测实际上是在L₁xdet(L₂)中检查状态间是否存在模拟关系.如果某个状态的行为能够被另一个状态模拟,则该状态可以用模拟状态替代.给定乘积自动机L₁xdet(L₂)中任意两个状态(s₁,s₂)和$({s'_1},{s'_2})$,如果满足${s_1} = {s'_1}$,并且对任意s$\in $s₂(s₂为一个状态集合)都存在$s' \in {s'_2}$,使得sps'(记为${s'_2} \le {s_2})$,则用$({s'_1},{s'_2}) \prec ({s_1},{s_2})$来表示对于TR-目标状态集合,(s₁,s₂)模拟$({s'_1},{s'_2}).$

引理1. 如果L₁xdet(L₂)中的两个状态(s₁,s₂)和$({s'_1},{s'_2})$满足$({s'_1},{s'_2}) \prec ({s_1},{s_2})$,并且存在$({s_1},{s_2})\buildrel e \over \longrightarrow (u,v)$,则必然存在$({s'_1},{s'_2})\buildrel e \over \longrightarrow (u',v')$,并且u=u',v'≤v.

基于以上引理,可得出以下结论:如果从$({s'_1},{s'_2})$出发,一个TR-目标状态是可达的,则从(s₁,s₂)出发,TR-目标状态一定也是可达的.因此在搜索时,如果已经访问过(s₁,s₂),当访问到$({s'_1},{s'_2})$时,可以停止搜索它之后的状态.同样,已存储(s₁,s₂)时,对于任意$({s'_1},{s'_2})$,只要它被( s₁,s₂)模拟,都可以将$({s'_1},{s'_2})$丢弃.(s₁,s₂)可看成是最大的状态.相反,如果已存储(s₁,s₂),之后又访问到一个状态满足$({s_1},{s_2}) \prec ({s''_1},{s''_2})$,则存储$({s''_1},{s''_2})$并将(s₁,s₂)丢弃.可知:算法搜索L₁xdet(L₂)中时,存储的最大状态集合中任意两个状态间不存在模拟关系.

算法1为基于模拟关系的traces精化检测算法.该算法首先初始化两个集合working和stored,working包含初始乘积状态,stored为空.然后,算法进入while循环.循环中,算法从working中取出状态(impl,spec),将其添加到stored中并移除所有非最大状态(第5行);然后,根据转移上的事件是否为τ,生成该 状态相应的所有后续状态.对任意后续状态(impl',spec'),检查是否存在$({s'_1},{s'_2}) \in stored$使得$(impl',spec') \prec ({s'_1},{s'_2})$成立:如果不成立,则将(impl',spec')放入working;反之,则舍弃该状态,不进行任何处理.算法在两种情况下结束,即,working为空或者找到了一个TR-目标状态(第9 行).算法中的第5行和第10行保证了stored中状态是两两不存在模拟关系的.

算法1. 基于模拟关系的traces精化检测算法.

1:  Let working={(init₁,{s|init₂as})};stored=∅;

2:  While {working≠∅}

3:  { pop (impl,spec) from working;

4:   stored:=stored$\cup $(impl,spec);

5:   remove all (s₁,s₂) satisfying (s₁,s₂)p(impl,spec) from stored;

6:   Forall {(impl,e,impl')$\in $τ₁}

7:   { If {e=τ} spec:=spec';

8:    Else $spec': = \{ s'|\exists s \in spec.{\rm{ }}s\mathop \mapsto \limits^e s'\} $;

9:    If {spec'=∅} return false;

10:    If {there is no $({s'_1},{s'_2}) \in stored$such that $(impl',spec') \prec ({s'_1},{s'_2})$}

11:     push (impl',spec') into working; }

12:  }

定理1. 当且仅当traces(L₁)⊆traces(L₂)时,算法1返回true^{[5, 6]}.

为了说明算法1如何工作,图1演示了具体例子.图1右侧显示了L₁xdet(L₂)的乘积自动机.由于${s'_1} \prec {s'_2}$,使得$({s_1},\{ {s'_1}\} )$和$({s_1},\{ {s'_2}\} )$间满足$({s_1},\{ {s'_2}\} ) \prec ({s_1},\{ {s'_1}\} )$,因此,$({s_1},\{ {s'_2}\} )$的后续状态不需要再进行搜索.

同理,由于$({s_1},\{ {s'_1},{s'_2}\} ) \prec ({s_1},\{ {s'_1}\} ),({s_2},\{ {s'_1},{s'_2}\} ) \prec ({s_2},\{ {s'_2}\} )$(因为一个状态总是可以模拟自己本身),$({s_1},\{ {s'_1},{s'_2}\} )$和$({s_2},\{ {s'_1},{s'_2}\} )$的后续状态也不需要再搜索.如图所示,原来基于子集构造的经典算法会产生13个状态,而算法1只需要搜索6个状态(用灰色表示).

2 . 基于模拟关系的Failures/Divergence精化检测

与traces精化检测相比,failure/divergence精化检测引入了failures和divergence语义.接下来将利用模拟关系给出failure/divergence精化检测算法.

2.1 基于模拟关系的stable failures精化检测

设L=(S,init,Act,τ)为一个LTS.给定S中的状态s,如果τ$\notin $enable(s),则称s是稳定的.在定义failures之前,需要先定义refusals子集.直观地说,如果从稳定状态s出发的所有事件集合中不包含某个事件e,则s拒绝事件e.对于任意一个状态s,s 的refusals子集用refusals(s)表示.refusals(s)被定义为集合:

X|s'.sas'∧τ$\notin $enable(s')∧X⊆S\enable(s')}.

L的failures被记为failures(L),其被定义成集合$\{ (tr,X):{\Sigma ^*} \times {2^\Sigma }|\exists s.{\rm{ }}init\mathop \mapsto \limits^{tr} s \wedge X \in refusals{\rm{ }}(s)\} ,$其中,$init\mathop \mapsto \limits^{tr} s$表示存在一条由状态和事件组成的有穷序列〈s₀,e₀,s₁,e₁,…,e_n,s_n+1〉,使得s₀=init,s_n+1=s,且tr=〈e₀,e₁,…,e_n〉.

定义5. 给定两个LTS L₁和L₂,当traces(L₁)⊆traces(L₂)成立时,L₁和L₂之间存在stable failures精化关系,当且仅当failures(L₁)⊆failures(L₂).

stable failures精化检测算法与traces精化检测算法类似,也是一个可达性算法.当traces精化关系成立时,在L₁xdet(L₂)中,stable failures精化检测算法需要搜索状态(x,y),满足refusals(x)不是refusals(y)的子集.这样的状态称为SFR-目标状态.给定一个状态集合X,其拒绝子集refusals(X)为集合 {ρ|s$\in $X.ρ$\in $refusals(s)}.因此,stable failures精化检测算法见算法2.于状态(impl,spec),检测refusals(impl)⊆refusals(spec)是否成立(第6行).

算法2. 基于模拟关系的stable failures精化检测算法.

1:  Let working={(init₁,{s|init₂as})};stored=∅;

2:  While {working≠∅}

3:  { pop (impl,spec) from working;

4:   stored:=stored$\cup $(impl,spec);

5:   remove all (s₁,s₂) satisfying (s₁,s₂)<(impl,spec) from stored;

6:   If {refusals(impl) is not a subset of refusals(spec)} return false;

7:   Forall {(impl,e,impl')$\in $τ₁}

8:   { If {e=τ} spec:=spec';

9:    Else $spec': = \{ s'|\exists s \in spec.s\mathop \mapsto \limits^e s'\} $;

10:    If {there is no $({s'_1},{s'_2}) \in stored$such that $(impl',spec') \triangleleft ({s'_1},{s'_2})$}

11:     push (impl',spec') into working; }

12:  }

由于stable failures精化检测关注系统不能执行的事件,因此并不能直接利用第1节的模拟关系.然而容易发现:一个状态必然能够模拟它本身,包括failures语义.因此,给定任意两个乘积自动机L₁xdet(L₂)中的状态

(s₁,s₂)和$({s'_1},{s'_2}),$当模拟关系为相等时,$({s_1},{s_2}) \prec ({s'_1},{s'_2})$事实上满足${s_1} = {s'_1}$,并且${s'_2} \subseteq {s_2}$,记为$({s_1},{s_2}) \triangleleft ({s'_1},{s'_2}).$

引理2. 给定L₁xdet(L₂)中的状态(s₁,s₂),对所有$({s_1},{s'_2})$,如果$({s_1},{s_2}) \triangleleft ({s_1},{s'_2})$,且从(s₁,s₂)出发,SFR-目标状态是可达的,则从$({s_1},{s'_2})$出发,SFR-目标状态也是可达的.

证明:该引理可以用归纳法来证明.

(1) 初始情况为:令(s₁,s₂)为SFR-目标状态,根据定义可以得出refusals(s₁)不是refusals(s₂)的子集.由于引理中假定${s'_2} \subseteq {s_2},$则$refusals{\rm{ }}({s'_2})$是refusals(s₂)的子集.如果refusals(s₁)不是refusals(s₂)的子集成立,则refusals(s₁)不是$refusals{\rm{ }}({s'_2})$的子集也成立,即,$({s_1},{s'_2})$也是SFR-目标状态.

(2) 假定(s₁,s₂)满足引理,即:对所有$({s_1},{s'_2})$,如果${s'_2} \subseteq {s_2}$,且从(s₁,s₂)出发SFR-目标状态是可达的,则从$({s_1},{s'_2})$出发SFR-目标状态也是可达的.令(x,y)为一个状态,从它出发存在一个到(s₁,s₂)的转移$(x,y)\buildrel e \over \longrightarrow ({s_1},{s_2}).$对所有状态(x,y¢),如果y'⊆y,则从(x,y')出发,一定存在一个转移$(x,y')\buildrel e \over \longrightarrow ({s_1},{s'_2}),$并且${s'_2} \subseteq {s_2}$.因此,(x,y)也满足引理,即:

对所有(x,y'),如果y'⊆y,则从(x,y)出发,SFR-目标状态是可达的.可以推出:从(x,y')出发,SFR-目标状态也是可达的.综合情形(1)、情形(2),该引理成立.

定理2. 当且仅当failures(L₁)⊆failures(L₂)时,算法2返回true.

证明:给定L₁xdet(L₂)中的状态S,将Dist(S)$\in $N$\cup ${¥}定义为从S出发到达SFR-目标状态的最短trace长度(如果SFR-目标状态从S出发是不可达的,则Dist(S)=¥).对于一个状态集合States来说,如果States=∅,则Dist(States)=¥;否则,Dist(States)=min_{S$\in $States}Dist(S).当且仅当States中的所有状态都不是SFR-目标状态时,断言SFR(States)为真.算法2的正确性可以用如下两个表达式来证明:

(1) ⌉SFR(working$\cup $stored)Þ⌉SFR({(i,{s|init₂as})|i$\in $init₁});

(2) ⌉SFR({(i,{s|init₂as})|i$\in $init₁})ÞDist(stored)>Dist(working).

表达式(1)说明:如果集合working和stored中存在SFR-目标状态,则从初始状态出发,SFR-目标状态是可达的.表达式(2)说明:如果从初始状态出发,SFR-目标状态是可达的,则Dist(Stored)一定大于Dist(working).

首先,由于LTS状态数量是有穷的,乘积自动机的状态数量也是有穷的,且算法中每个状态只可能访问1次,因此算法2最终能够停止.然后,只有当(impl,spec)满足条件refusals(impl)不是refusals(spec)的子集(第6行)时,算法2才会返回false.当refusals(impl)不是refusals(spec)的子集时,(impl,spec)是一个SFR-目标状态,因此,断言SFR(working$\cup $stored)是假的.

由表达式(1)可知,断言SFR(working$\cup $stored)为假可推出SFR({(i,{s|init₂as})|i$\in $init₁})为假.即:从初始状态

出发,SFR-目标状态是可达的,因此L₁与L₂的stable failures精化关系不能维持.此外,只有当working为空时,算法2返回true,可推出Dist(Stored)>Dist(working)是错误的,因为此时Dist(Stored)和Dist(working)都为¥.由于表达式(2)的逆反命题同样成立,可以 得出:从初始状态出发,SFR-目标状态是不可达的.因此,L₁与L₂存在stable failures精化关系.

图2的例子说明了算法2对状态空间的消减不会导致反例丢失.

令图中的${X_0} = ({s_1},\{ {s'_1}\} ),{X_1} = ({s_1},\{ {s'_1},{s'_2}\} ),{X_2} = ({s_2},\{ {s'_2}\} ),{X_3} = ({s_2},\{ {s'_1},{s'_2}\} ),{X_4} = ({s_3},\{ {s'_2}\} ),{X_5} = ({s_3},\{ {s'_1},{s'_2}\} )$,从图2左侧的LTS可看出:s₃拒绝事件b,而${s'_1}$和${s'_2}$不拒绝发生任何事件.因此,X₄和X₅为SFR-目标状态.由于X₁<X₀,X₁

以后的状态不再搜索,包括X₅.然而从图上可以看到:即使状态空间被消减,无法访问到SFR-目标状态X₅,从初始状态X₀出发,还是能从另外一条trace访问到SFR-目标状态X₄.因此,反例并不会丢失.此外,由图2可知:搜索顺序虽然具有任意性,但基于模拟关系的算法有可能更快找到较短的反例.

2.2 基于模拟关系的failures-Divergence精化检测

本节首先定义failures-divergence精化关系.设L=(S,init,Act,τ)为LTS.对于任意一个S中的状态s来说,如果s能够无休止地执行τ转移,则称s是diverge的.给定一条trace tr,当且仅当存在该trace的前缀pre或者tr本身,使得$init\mathop \mapsto \limits^{pre} s$并且s是diverge的,则tr是diverge的,用符号div(tr)表示.所有L中发生diverge的traces为集合{tr|div(tr)},用divergences(L)表示.

定义6. 给定两个LTS L₁和L₂,当traces(L₁)⊆traces(L₂)和failures(L₁)⊆failures(L₂)成立时,L₁和L₂之间存在failures-divergence精化关系,当且仅当divergences(L₁)⊆divergences(L₂).

Failures-divergence精化检测算法也是一个可达性算法,见算法3.

算法3. 基于模拟关系的failures-divergence精化检测算法.

1:  Let working={(init₁,{s|init₂as})};stored=∅;

2:  While {working≠∅}

3:  { pop (impl,spec) from working;

4:   stored:=stored$\cup $(impl,spec);

5:   remove all (s₁,s₂) satisfying (s₁,s₂)p(impl,spec) from stored;

6:   If {impl diverges but spec does not diverge} return false;

7:   Forall {(impl,e,impl')$\in $τ₁}

8:   { If {e=τ} spec:=spec';

9:    Else $spec': = \{ s'|\exists s \in spec.s\mathop \mapsto \limits^e s'\} $;

10:     If {there is no $({s'_1},{s'_2}) \in stored$such that $(impl',spec') \prec ({s'_1},{s'_2})$}

11:      push (impl',spec') into working; }

12:  }

给定一个状态集合X,如果存在s$\in $X并且s是diverge的,则X也是diverge的.

在L₁xdet(L₂)中,当traces(L₁)⊆traces(L₂)和failures(L₁)⊆failures(L₂)成立时,failures-divergence精化检测算法需要搜索乘积状态(x,y),满足x是diverge的但y不是diverge的.这样的乘积状态称为FDR-目标状态.算法3中,对于状态(impl,spec),第6行检测impl和spec是否diverge.

引理3. 给定L₁xdet(L₂)中的状态(s₁,s₂),对所有$({s_1},{s'_2})$,如果$({s_1},{s_2}) \prec ({s_1},{s'_2})$,且从(s₁,s₂)出发,FDR-目标状态是可达的,则从$({s_1},{s'_2})$出发,FDR-目标状态也是可达的.

证明:该引理可以用归纳法来证明.

(1) 初始情况为:令(s₁,s₂)为FDR-目标状态,根据定义可以得出,s₁是diverge的但s₂不是.由于引理中假定$({s_1},{s_2}) \prec ({s_1},{s'_2})$,则对于任意$s' \in {s'_2}$,存在s$\in $s₂使得s'ps,如果s'是diverge的,则s也是diverge的.由此可得出:如果${s'_2}$是diverge的,则 s₂也是diverge的.因此,s₂不是diverge可推出${s'_2}$不是diverge,即,$({s_1},{s'_2})$也是FDR-目标状态;

(2) 假定(s₁,s₂)满足引理,即:对所有状态$({s_1},{s'_2})$,如果$({s_1},{s_2}) \prec ({s_1},{s'_2})$,且从(s₁,s₂)出发,FDR-目标状态是可达的,则从$({s_1},{s'_2})$出发,FDR-目标状态也是可达的.令(x,y)为一个状态,存在转移$(x,y)\buildrel e \over \longrightarrow ({s_1},{s_2})$.对所有状态(x,y'),如果(x,y)p(x,y'),则一定存在一个转移$(x,y')\buildrel e \over \longrightarrow ({s_1},{s'_2})$,并且$({s_1},{s_2}) \prec ({s_1},{s'_2})$成立.因此,(x,y)也满足引理.

综合情形(1)、情形(2),该引理成立.

定理3. 当且仅当divergences(L₁)⊆divergences(L₂)时,算法3返回true.

定理3的证明与定理2类似,这里不再赘述.我们使用图3的例子来演示算法3如何工作.

令图中的${X_0} = ({s_1},\{ {s'_1}\} ),{X_1} = ({s_2},\{ {s'_1},{s'_2}\} ),{X_2} = ({s_2},\{ {s'_2}\} ),{X_3} = ({s_2},\{ {s'_1}\} )$,由于X₁pX₂和X₃pX₂,X₁和X₃以后的状态不再搜索,包括X₃.从图3的LTS中可以看到:状态${s'_2}$不是diverge的,其他状态都是diverge的.因此可以得到,X₂为FDR-目标状态.同样地,从图上可以看到:即使状态空间被消减,FDR-目标状态X₂还是能被访问到.

3 . 基于模拟关系的时间自动机精化检测 3.1 时间自动机定义

首先给出时间自动机相关定义^{[8, 21]}.设χ是时间自动机中的时钟集合,F(χ)表示时间约束集合.每一个时间约束定义如下:d:=true|x~n|d₁∧d₂|⌉d₁,其中,~$\in ${=,≤,≥,<,>},x是时钟集合χ中的一个时 钟,n是一个非负整数.由符号~$\in ${≤,<}可以获得下行的时间约束,用F_≤,<(χ)表示.χ上的一个时钟赋值v是指为每个时钟赋予一个实数值.如果v的时钟赋值使得时间约束d的布尔值为真,则称v满足χ上的一个时间约束d.对任意d$\in $Â⁺,令v+d代表时钟赋值v',使得对所有χ$\in $χ都满足v'(χ)=v(χ)+d.令X代表被重置的时钟集合,[Xa0]v表示对所有τ$\in $X都赋值为零,对于所有满足τ$\in $χ且τ$\notin $X的时钟仍与v相同.

定义7. 一个时间自动机是六元组A=(S,Init,S,χ,L,τ),其中,S是有穷状态集合;Init⊆S是初始状态集合;S是一个事件集合,满足τ$\notin $S;χ是有穷时钟集合;L:S→F_≤,<(χ)是函数,在每个状态上添加一个状态不变式;τ⊆SxSxF(χ)x2^CxS是带时间约束的转移关系.

时间自动机A的具体语义为具有无穷状态的状态转移系统,表示为χ(A)=(S_c,Init_c,Â⁺xS,T_c),其中:S_c为A的具体配置集合,具体配置为(s,v),满足s$\in $S并且v是一个时钟值;Init_c={(s,χ=0)|s$\in $Init_c}为初始具体配置集合;T_c为具体转移集合,每个具体转移表示为((s,v),(d,e),(s',v')),满足:存在一个转移(s,e,d,X,s')$\in $τ;v+d$\in $d;v+d$\in $L(s);[Xa0](v+d)=v';v'$\in $L(s').直观地看,系统在s等待d个时间周期,然后执行转移到达状态s'.

给定χ(A)中的一个运行〈(s₀,v₀),(d₁,e₁),(s₁,v₁),(d₂,e₂),…,(s_n,v_n)〉,可获得时间-事件序列á(D₁,e₁),(D₂,e₂),…,(D_n,e_n)ñ,满足对所有1≤i≤n,${D_i} = \sum\nolimits_{j - 1}^i {{d_j}} $.χ(A,(s,v))表示从所有(s,v)出发的运行得到的时间-事件序列集合.A表示的语言用L(A)表示,其为从A中任何初始运行得到的时间-事件序列总和.当两个时间自动机定义相同的语言,则它们是等价的.给定上述χ(A)的一个运行,也可以得到一个不带时间的事件序列〈e₀,e₁,…,e_n〉.所有这些不带时间的事件序列用traces_TA(A)表示.

由于时间点的无穷性,使得χ(A)中状态数量也是无穷的.因此,需要将其转化为有穷状态系统才能进行相关验证.时钟域抽象(zone abstraction)是目前最常用的抽象技术.时间自动机经过时钟域抽象后,得到有穷状态的时钟域图.时钟域是时钟赋值的集合,里面的所有时钟值都满足某个的时间约束.一个时钟域是由定义在χ上的简单线性不等式或线性不等式的合取式结合组成,例如x-y≤5,y>3∧x<7等,其中,x,y$\in $χ.时钟域和时间约束是一致的.给定一个时钟域,用d^­表示从d经过任意时间后得到的时钟域.

定义8. 设A=(S,Init,S,χ,L,τ)为时间自动机,其时钟域图ZG(A)是四元组(S_z,Init_z,S_z,τ_z),其中,

· S_z表示节点集合,每个节点用(s,d)表示,且s$\in $S代表一个状态,d代表一个时间约束(时钟域);

· Init_z={(init,(∧_{c$\in $χ}χ=0)^­∧L(init))|init$\in $Init}是初始节点集合;

· τ_z:S_zxSxS_z代表转移关系,其中,((s₁,d₁),e,(s₂,d₂))$\in $τ_z当且仅当(s₁,e,d,X,s₂)$\in $τ,d₁∧d≠false,[Xa0] (d₁∧d)∧L(s₂)≠false,并且d₂=(N([Xa0](d₁∧d)∧L(s₂)))^­.

上述定义中的N是时钟域标准化(zone normalization)函数.为了保证时钟域图中的节点数量是有限的,标准化过程^[18]是必要的.其基本原理为:时间自动机中的时间约束中,对于每个时钟都存在一个最大数值,当一个时钟域中的时钟值大于该数值时,不需要关心其具体数值,只需要将这个值设为该时钟的最大数值即可.

ZG(A)中的运行是无穷序列p_z=〈(s₀,d₀),e₀,(s₁,d₁),e₁,(s₂,d₂),e₂,…〉,其中,(s₀,d₀)$\in $Init_z,并且对所有i≥0,((s_i,d_i),e_i,(s_i+1,d_i+1))$\in $τ_z.χ(A)的一个运行〈(s₀,v₀),(d₀,e₀),(s₁,v₁),(d₁,e₁),…〉是p_z的一个实例,当且仅当对所有i≥0,v_i>d_i成立.p_z被称为该χ(A)运行的一个抽象.从p_z可以得到不带时间的有穷事件序列〈e₁,e₂,…〉,所有这些不带时间的事件序列用traces_ZG(A)表示.容易看出,traces_ZG(A)和traces_TA(A)是等价的.

3.2 时间自动机的traces精化检测

给定时间自动机A和LTS L,时间自动机traces精化检测目标是验证traces_TA(A)⊆traces(L)是否成立.直观地看,检测目的在于验证A在有时间约束的情况下是否只能执行L中的traces而不存在反例.由从前文可知,traces_ZG(A)和traces_TA(A)是相同的,因此有如下时间自 动机traces精化检测的定义.

定义9. 设A为时间自动机,L为一个LTS.当且仅当traces_ZG(A)⊆traces(L),A和L存在traces精化关系.

定义10. 设A=(S_a,Init_a,S_a,C_a,L_a,T_a)为时间自动机,L=(S_l,Init_l,Act_l,τ_l)为LTS,并且$\det (L) = ({S'_l},ini{t'_l},$ $Ac{t'_l},{T'_l})$>为L的确定化后的LTS.A和L的乘积自动机,即A和det(L)的乘积自动机,是一个时钟域图ZG_AL=(S,Init,S,τ),满足如下条件:

(1) S中的一个元素是抽象配置(s,d,Y),其中s是S_a中的状态,d是C_a上的时钟域,τ是${S'_l}$中的一个状态;

(2) Init={(init_a(C_a=0)^­∧L_a(init_a)),Init_l|init_a$\in $Init_a}是初始抽象配置集合;

(3) S等于S_a;

(4) τ:SxτxS是转移关系,其中,((s₁,d₁,Y₁),e,(s₂,d₂,Y₂))$\in $τ,当且仅当以下条件被满足:1) (s₁,e,d,X,s₂)$\in $τ_a,d₁∧d≠false,[Xa0](d₁∧d)∧L(s₂)≠false,并且d₂=(N([Xa0](d₁∧d)∧L(s₂)))^­;2) $({Y_1},e,{Y_2}) \in {T'_l}$.

对于ZG_AL中的抽象配置ps,其所有的后续抽象配置表示为post(ps,ZG_AL).

定理4. 设A为时间自动机,L为LTS.当且仅当在ZG_AL中,(s,d,∅)是不可达的,traces_ZG(A)⊆traces(L)成立.

证明:首先证明命题当ZG_AL中(s,d,∅)不可达,traces_ZG(A)⊆traces(L)成立.如果traces_ZG(A)⊆traces(L)不成立,则在traces_ZG(A)中一定存在一个运行p_a,使得p_a不在traces(L)中.令|p_a|为p_a的长度.从p_a必然可以得到前缀p_l,使得|p_l|=|p_a|-1,并且p_l既在traces_ZG(A)中又在traces(L)中.令(s,d,Y)为抽象配置,其中是ZG(A)中的抽象配置,并且ZG(A)的运行完全执行p_l且该运行最后的状态是(s,d);Y是det(L)的状态,L的运行也完全执行p_l且该运行的最后状态为Y.此时,Y并不是空集.接下来,(s,d)能够执行某个事件e,并且转移到抽象配置(s',d'),但是对于任何一个Y中的元素均不能执行同样的事件.因此,在这种情况下,(s',d',∅)是可达的,命题得证.对于命题当traces_ZG(A)⊆traces(L)时,ZG_AL中(s,d,∅)是不可达的,其证明方式类似,这里不再赘述.

抽象配置(s,d,∅)被称为TA-目标状态.

3.3 基于模拟关系的时间自动机traces精化检测

两个时钟域之间是可比较的.给定两个在同一个时钟集合上的时钟域d和d',当且仅当对任意v$\in $d,v$\in $d'成立,则d⊆d'.(s,d,Y)µ(s,d',Y')表示d⊆d',并且对任意y'$\in $Y'都存在y$\in $Y,使得y'py(即Y'≤Y).下面的引理说明了如何在算法中利用该模拟关系:

引理4. 设(s,d,Y)和(s,d',Y')为ZG_AL中的两个抽象配置.如果(s,d,Y)µ(s,d',Y'),且从(s,d,Y)出发TA-目标状态是可达的,则从(s,d',Y')出发TA-目标状态也是可达的.

证明:该引理可以用归纳法来证明.

(1) 初始情况为:令(s,d,Y)为TA-目标状态,即Y=∅.由于Y'≤Y,因此Y'=∅,因此,(s,d',Y')也是TA-目标状态;

(2) 假定两个抽象配置满足引理,即(s,d,Y)µ(s,d',Y'),且如果从(s,d,Y)出发,TA-目标状态是可达的,则从(s,d',Y')出发,TA-目标状态也是可达的.设((s₀,d₀,Y₀),e,(s,d,Y))为ZG_AL的一个转移,并且存在$({s_0},{\delta '_0},{Y'_0})$满足${\delta _0} \subseteq {\delta '_0}$以及${Y'_0} \le {Y_0}$(即$({s_0},{\delta _0},{Y_0}) \propto ({s_0},{\delta '_0},{Y'_0})$).由${Y'_0} \le {Y_0}$推出Y'≤Y;${\delta _0} \subseteq {\delta '_0}$推出d⊆d',其原因为,从s₀出发的两个转移其实为同一个转移.因此我们得到:$(({s_0},{\delta '_0},{Y'_0}),e,(s,\delta ',Y'))$是ZG_AL中的一个转移,并且d⊆d',Y'≤Y.

综合情形(1)、情形(2),该引理成立.

基于模拟关系的时间自动机traces精化检测算法见算法4.算法4为一个可达性算法,其采用on-the-fly的方式构建时钟域图ZG_AL.

算法4. 基于模拟关系的时间自动机traces精化检测算法.

1:  Let working=Init;stored=∅;

2:  While {working≠∅}

3:  { pop ps:=(s,d,Y) from working;

4:   stored:=stored$\cup $ps;

5:   remove all ps' satisfying ps'µps from stored;

6:   Forall {(s',d',Y')$\in $post(ps,ZG_AL)}

7:   { If {Y'=∅} return false;

8:    If {there is no ps'$\in $stored such that (s',d',Y')µps'}

9:     push (s',d',Y') into working; }

10:  }

下面的定理说明了算法4的正确性.

定理5. 当且仅当traces_ZG(A)⊆traces(L)时,算法4返回true.

由于时钟域标准化函数,时钟域的数量是有穷的,因此抽象配置的数量也是有穷的且算法是可以终止的.算法4正确性的证明与算法1~算法3的证明过程类似,在此不予赘述.

在图4中,我们展示了一个例子来说明算法4如何工作.在图中,时间自动机A的状态s₂上有一个状态不变式x<5,其含义为:A在s₂上不能一直停留,当时钟值大于或等于5时,A必须进入下一个状态.图中的ZG_AL为时钟域图.令$p{s_0} = ({s_1},\{ {s'_1}\} ,x \ge 0),p{s_1} = ({s_1},\{ {s'_1},{s'_2}\} ,x > 2)$并且$p{s_2} = ({s_1},\{ {s'_1},{s'_2}\} ,x > 3)$.根据模拟关系,ps₁µps₀和ps₂µps₀成立,因此,ps₁和ps₂以后的状态不需要再搜索.由图4可见,状态搜索数量从10个减少为4个.

4 . 实验结果

本文提出的算法都已在形式化建模和验证工具PAT(process analysis toolkit)^[4]中实现.PAT工具的设计目标是,使用当前最先进的精化检测和模型检测技术对分布式/并发系统进行系统化验证.为了衡量算法性能,实验使用一系列实际系统作为基准系统,所有系统都内嵌在PAT中.实验的运行环境为PC机,其处理器为Intel(R) Core(TM) i5-4460 CPU@3.20GHz,内存为8GB.

第1部分实验对基于模拟关系和不使用模拟关系的traces,stable failures和failures-divergence精化检测算法性能进行对比.本实验使用的基准系统^[19]包括:邮箱问题(MB),主要为邮差和收信人之间的同步问题;基于单个或多个读者的多值注册模拟系统(MRO和MRM),核心为分布式计算中的读写问题;基于线性化点或非线性化点的并发堆栈系统(CSWL和CSOL),面向多处理器系统并行编程问题;可扩展非零指示器(SNZI),用于提高事物内存并行程序的性能.基准系统一般具有输入参数(如进程数量、队列长度等).

完整的实验结果见表1.不带#的基准系统实验结果为true,即精化关系成立;带#的基准系统结果为false,即精化关系不成立,存在反例.基准系统中的数字代表系统并发进程数量.表中的倍数为不使用模拟关系算法的检测时间与基于模拟算法的检测时间之间的比值.从表格可知:基准系统不同,则使用基于模拟关系的算法性能提高程度也不同.在大多数情况下,基于模拟关系的算法性能远远好于不使用模拟关系的算法.例如在CSOL*3中,基于模拟关系的stable failures精化检测算法性能提高了8.6倍.然而表格中也存在某些基准系统,基于模拟关系的算法不能发挥明显作用.例如SNZI*11,尽管基于模拟关系的算法消减了一小部分状态,但由于算法中检查状态间是否存在模拟关系的相关操作存在额外开销,算法从模拟关系获得的状态空间的缩减无法抵消模拟操作的额外开销,因此性能提升并不明显.另外,从#MRO*12和#MRM*9的实验结果看出:对于结果为false的验证,基于模拟关系的算法有时能够极大地提高反例的查找速度.

第2部分实验对基于模拟关系和不使用模拟关系的时间自动机traces精化检测算法性能进行对比.本实验使用的基准时间系统^[8]包括Fischer互斥协议(FISCH)、Lynch-Shavit互斥协议(LYNCH)、火车控制系统(RWCS)以及CSMA/CD协议(CSMACD,针对broadcast网络的协议).

实验结果见表2.表中的基准系统包含了时间自动机和LTS的进程数量,例如,FISCH*6(2)表示时间自动机具有6个进程,LTS包含2个进程.从算法运行时间倍数和状态数倍数来看:在大部分的例子中,基于模拟关系的算法要极大地优于不使用模拟关系的算法.这种性能提升包含两个原因:其一为LTS往往是非确定化的,模拟关系的使用能够避免完全的子集构造;其二为时钟域之间包含关系也是一种模拟关系,使得同样的时间值不需要重复搜索.在某些例子中,如FISCH*8(1),模拟关系的使用并不能减少状态数量,反而使得验证时间变长.这是由于LTS是确定化的并且状态间也不存在模拟关系.另外,时钟域之间的包含关系也没有起作用.

5 . 相关工作

抽象和模拟是形式化方法中十分重要的概念.状态转移系统可以在不同的抽象级别上对软硬件系统进行建模.我们往往使用两个系统状态之间的二元关系来比较不同的转移系统,这种二元关系可以定义在在不同的抽象层.最先提出的二元关系为互模拟等价(bisimulation equivalence)关系^[11],并且这种互模拟等价关系已被应用到了NFA等价问题的检测中^[12].然而互模拟等价关系较为严格,并不常常能使状态空间得到明显的缩减,因此引入了模拟(simulation)关系^[13],用来验证一个系统是否正确执行了另一个更抽象的系统行为.互模拟等价和模拟关系相关概念已经被扩展到很多不同的方向,如公理化、精化检测、领域方法等.有很多学者研究了基于模拟关系的抽象方法,并提出了很多算法来计算模拟关系并且得到相应的抽象系统,最新的相关技术包括基于反例的抽象精化^[14]、面向无穷状态的抽象和学习方法等^[15].

文献^[5]提出了基于反链这种模拟关系的非确定型有穷自动机语言通用性和语言包含检测方法,文中的结论表明:基于该模拟关系的方法在某些情况下,其性能可能会高出标准方法几个数量级.他们接下来又研究了基于反链的线性时序逻辑LTL模型检测算法,得出了类似的结论^{[16, 17]}.文献^[19]首次将反链关系引入到了failures/ divergence精化检测算法中.然而上述论文中的反链关系只是一种子集包含关系,其包含在本文定义的模拟关系中,并且本文的模拟关系能够更好地提高failures/divergence精化检测和时间自动机traces精化检测算法的性能.另外,文献^{[6, 20]}中关于树自动机等利用模拟关系的语言通用性和语言包含问题也与本文的工作密切相关.

6 . 结束语

本文提出了基于模拟关系的stable failures和failures-divergence精化检测方法,还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.利用模拟相关原理,本文提出的算法均可有效减少不必要的状态搜索;同时,利用归纳法证明了算法正确性,并说明了在不搜索全部状态空间的情况下,反例并不会丢失.实验结果表明,基于模拟关系的算法效率有很大提高.

关于未来工作,一方面将研究利用更多的模拟关系进一步优化算法,例如在时间自动机精化检测中利用lower/upper bounds的方法或研究时间自动机robustness问题来减少状态空间;另一方面可不断完善时间系统和概率系统的精化检测,例如研究解决时间自动机的non-Zenoness问题、两个概率系统精化关系如何定义等问题.