带有启发式因子的死锁模型检测算法

王 焱，吴 涛，杨 斐

(1.成都信息工程大学 计算机学院， 成都 610225；2.中国核动力研究设计院 核反应堆系统设计技术重点实验室， 成都 610041)

0 引言

系统和软件设计的可靠性非常重要，因此如何构建可靠的软件和系统的相关技术就极为关键。特别是在一些关键领域，如航天航空领域、核领域等等，系统一旦出现故障，其带来的损失往往是不可接受的。由于传统的测试仿真只能寻找系统的错误，而不能证明系统不存在错误，形式化验证就能够解决这个问题。

模型检测是一种自动验证有限状态并发系统的形式化验证技术[1]，它能够通过对所给模型的所有可能状态进行分析，验证其是否满足所给定的规范。如果不满足，则生成相应的反例。系统规范一般是通过线性时序逻辑(LTL)或者分支时序逻辑(CTL)刻画的[2]。

在显式模型检测中，系统的设计模型通常用有向图表示。它表示了并发系统的所有可能的行为，同时还包含了各个状态之间的变迁关系。一般的，模型检测器采用确定性算法和穷尽搜索状态空间来验证是否满足某些性质。当状态空间过大时，就会导致检测效率较低，甚至不能完成检测目标。在核领域的DCS系统中，由于系统较为复杂，这种问题尤为明显。

为了提高模型检测的效率，业界提出了几种通过减少状态空间大小的方法来缓解这个问题，比如符号模型检测、抽象方法、偏序规约等等[3-5]。同时，除了上述的方法，提高在状态空间中搜索算法的效率也是可行的。为了提高确定性算法在状态空间过大的情况下的表现，研究人员进行了相关研究。文献[6]提出了一种基于磁盘的宽度优先搜索算法(BFS)。该方法针对BFS出现的某些层所拥有的状态无法全部存储到内存中而影响模型检测的问题，将每一层的状态进行分区划分，从而提高算法效率。

同时，并行化技术也能够提高确定性算法的表现。文献[7]采用了并行化和分布式的BFS，从而能够发现长度更短的反例。文献[8]采用并行化的BFS，完成了对模型安全性质的检测。

除了以上的确定性算法研究之外，基于启发式算法的模型检测算法也得到了研究人员的关注。通过启发式因子让搜索方向向目标状态靠拢，从而加快搜索。文献[9]提出了一种基于A*算法的模型检测算法。文献[10]也提出了基于粒子群算法的模型检测算法，利用粒子群高效完成了对违反安全性的路径的搜索。同时，粒子群算法在概率模型检测中也有较好的表现。文献[11]提出了一种混合粒子群算法和引力搜索的算法完成了死锁性质的检测。文献[12]提出了一种基于蚁群算法的模型检测算法，同时通过增加目标节点的信息素操作，加快了模型检测的效率。文献[13]提出一种新的蚁群算法ACOhg，通过对搜索深度的动态选择，在状态空间过大时有良好的表现。文献[14]将蒙特卡洛树算法应用到了模型检测算法中，该方法能够有效搜索状态空间从而得到相应的反例。

在以上的文献中，没有考虑到路径长度对所生成反例的影响。因此，探讨了差分进化算法(DE)在针对状态空间数量较大时检测死锁状态的可行性。差分进化算法是一种基于遗传和自然选择的启发式算法。这种启发式算法结合了优胜劣汰和随机性的信息，可以较好地兼顾检测速度和检测质量。同时针对模型检测的具体背景，设计了新的路径生成算法，用以解决状态迁移图中的编码问题。同时在算法原有框架下，增添了模拟退火操作，与关键参数的自适应用以提高算法的表现。最后设计了用于评估路径优劣的适应值函数。

主要内容组织如下：第1节描述了模型检测的相关背景，同时回顾了一些已经提出了的提高检测效率的方案；第2节详细描述了所提出的研究内容；第3节描述的是相关实验，同时分析了实验结果；最后在结语部分，对工作做出了总结，同时分析了存在的不足，并在最后对未来的相关工作做出了展望。

1 死锁检测解决方案

在本节中，形式化了死锁检测问题，同时介绍了标准差分进化算法的过程以及详细描述了基于差分进化算法框架提出的模型检测算法。

1.1 问题形式化

死锁是指2个或者2个以上的进程在执行过程中，由于竞争资源从而造成的一种阻塞的情况。若无外力的情况下，进程将永远无法进行下去，永远处于互相等待的情况，这就是死锁。

在显式模型检测中，死锁状态对应的是系统状态图中只有入边而没有出边的节点。因此死锁检测问题可以形式化为有向图中从初始状态开始到目标状态结束的路径搜索问题。将这个问题形式化如下：

设G=(S,T)为一个有向图，其中S表示图中的节点的集合，T表示有向图的边的集合。设q为图的初始节点，F是图中所有目标节点的集合。设有向图中的一条有限路径Π=S1,S2,S3,…,Sn，Si∈S，i=(1,2,3,…,n)。|Π|表示该条路径的长度。T(S)表示当前节点的后继节点。

现给定一个有向图G，死锁检测问题可以形式化为找到一个从起始节点开始且结束于目标节点的路径Π。Π需要满足以下约束：

S1=q，Sn∈F

(1)

1.2 差分进化算法

差分进化算法[15]是一种基于群体的启发式算法，最早由Storn和Price于1995年首次提出，其优化的核心是基于群体个体之间的相互合作和相互竞争从而引导搜索的方向，达到加快搜索的目的。其主要由差分、交叉变异、选择策略3个部分组成。具体算法流程如图1所示。

图1 标准差分进化算法流程框图

作为一种基于群体的进化算法，差分进化算法中每一个个体都代表了一个可能解，这些个体称为染色体，通过特定的操作生成子代个体，再从子代个体中选择出相对较优的个体组成下一代种群，从而推动算法的进行。差分进化算法的基本步骤如下：

步骤1设置算法初始参数，初始化种群。

步骤2对种群中的每一个个体进行差分操作，产生变异个体Vi。具体差分操作是随机选择种群中两个不同的个体，将其向量缩放之后与待变异个体进行向量合成生成变异向量Vi。公式如下:

Vi=X1+F(X2-X1)

(2)

步骤3对于个体向量Xi和变异向量Vi进行交叉操作，生成实验个体向量Ui。具体交叉操作是设定一个初始值CR，CR具体值参考后文。该值决定了哪些维度是应该采用变异向量的维度，哪些向量保持不变。公式如下：

(3)

步骤4根据选择策略选择出合适的下一代解，作为下一代种群。

步骤5判断当前解是否满足终止条件。若满足则输出最优结果；否则转至步骤2。

因此，当把死锁检测问题看作一个优化问题时，就可以考虑将有向图看作一个状态空间，然后通过染色体的个体行为联合整个种群的群体行为共同寻解，而寻到的解就是检测到的反例。

1.3 应用于死锁检测的改进差分进化算法

基于原有的差分进化算法框架，提出了以下的在模型检测背景下的改进差分进化算法。与原算法相比，提出了新的路径生成算法：模拟退火算子用以提高算法表现，Cr自适应参数以及针对路径的适应值函数。

1.3.1粒子编码以及路径生成

传统的差分进化算法由于用于解决优化问题，采取的是随机编码的方式。但是这种方式在模型检测的背景下是不合适的。因此编码方式也是相当关键的。

传统的编码方式主要有2种：直接编码和间接编码。

直接编码：直接按照节点的标识号顺序进行编码。这些标识号随机分配给状态图中所有的节点。这种编码方式中，由于节点序列是随机的，可能会产生大量的无效路径(即编码顺序和迁移关系不匹配)。

间接编码：随机序列在有向图中的路径生成不是一个好的选择，间接编码相比而来会是一个更好的选择，且解决了直接编码在迁移关系不匹配的问题。提出的间接编码方式具体如下：随机初始化一定长度的字符串，然后依次扩展状态，直到达到最大的路径长度到达目标节点。在每一次扩展路径，且有多个迁移可以选择时，通过当前编码的字符去选择相应的节点。

通过这种方式依次扩展路径，直到结束路径找到目标状态或者达到最大搜索深度。同时，这种编码可以在每一次扩展完一个状态的时候，判断当前状态是否是目标状态，如果是的话就停止状态的扩展，减少了模型检测的耗时，同时因为后续的所有差分进化算法都通过对字符串的编码进行操作从而间接影响路径生成，可以避免产生大量的无效路径。这也是为什么选择的是差分进化算法的一个原因，差分进化算法的优化过程是不会跟随最优解的，而是采用随机的方法。这样通过改变字符的编码间接改变状态节点的选择，对于整个优化过程不会带来影响。

路径生成算法见算法1。

算法1路径生成算法

1.设置当前路径的开始节点为初始节点S0，Π1=S0

2. fori=1->MaxLength

3.统计当前路径的最后一个节点的后继节点集合T，并得到集合长度size

4.计算ID=chromesome(i)%size，并且通过ID选择集合中的第ID个后继节点，即T(ID)

5.将选择的节点作为当前路径的最后一个节点，Πi=T(ID)

6.ifΠi==goal

7.停止循环，算法结束

8.end if

9. end while

算法1中，Π表示当前的路径节点序列，MaxLength为状态空间中搜索的最大深度，chromesome表示随机的字符串，S0表示状态搜索的初始节点，goal表示状态搜索的目标节点。

1.3.2模拟退火操作

该操作是在差分进化算法已经生成了所有交叉个体之后的操作。为了防止当前种群中较优的部分个体依然没有找到目标节点或者找到了目标节点但是路径的适应值较差，即路径较差。因此通过此处的变异操作在当前适应值最优的个体进行模拟退火操作，按照模拟退火中的Metropolis准则，以一定的概率接收次优解从而去寻找更优的路径。其中，每一次对原始最优解进行高斯扰动来生成新解。模拟退火算法见算法2。

算法2模拟退火算法

1.oldchromesome=chromesome;oldroad=

Bestroad

2. whileTem>Tmin

3. for 马尔科夫链长度

4.newchromesome=oldchromesome*g;

//对最优路劲对应的字符串进行高斯扰动

5. 根据算法1生成当前字符串对应的路径newroad

6.Fitness(newroad);

//计算newroad的适应值

7.ifFitness(newroad)-Fitness(oldroad)<0

8.oldroad=newroad

9.oldchromesome=newchromesome

10. else

11. 按照Metropolis准则判断当前新解是否要取代旧解

12. end for

13.Tem=Tem*alpha;//温度衰减

14. end while

算法2中，Tem表示初始温度，Tmin表示最低温度，alpha表示温度衰减率，oldchromesome和oldroad分别代表旧的字符串编码和旧路径，newchromesome和newroad分别代表新的字符串编码和新路径。

Metropolis准则就是以一定的概率选择接受或者不接受新解。避免了算法每次都选择适应值较高的路径，从而局限了在状态空间中的搜索范围。

1.3.3Cr自适应参数

在搜索后期，对于路径的搜索已经达到了一个稳定的状态。为了让差分进化算法的变异的概率Cr随着迭代的过程依次增加，在后期提高其寻找更优路径能力，同时增强跳出局部最优的能力。主要采用的是根据迭代的次数，逐渐增加变异的概率。基于这样一个直觉，随着迭代过程的进行，优化的过程是—个逐渐趋近于更优的过程，同时也是一个趋向于更稳定的一个过程。在算法进行的后期，种群会保持相对稳定。因此，这种方法可以在后期增大变异概率，让算法在后期依然保持较好的寻优能力。对于Cr的求值公式如下：

Cr=Crmin+(Crmax-Crmin)×iter/MaxEva

(4)

式中：Crmin表示最小变异概率，Crmax表示最大变异概率，iter表示当前迭代次数，MaxEva表示最大迭代次数。

1.3.4适应值函数

针对死锁的模型检测，其目标是在有向图中找到一条从初始节点开始，且结束于目标节点的一条路径，即反例。且如果反例的长度越短，就更有利于分析出问题。基于这个认识，对于都找到了目标节点的2个路径，其中，路径长度越短，其适应值就越小，代表了其更优。同时，针对处理的关于死锁的模型检测问题，特别设置了—个启发式量，即状态可迁移量。统计一条完整路径的状态可迁移量的和，这是基于对于找到了死锁的路径，其可迁移量总和相比长度相当的未找到死锁状态的路径，其可迁移量较少。对于没有结束于目标节点的路径，处理如下，添加一个较大的惩罚值，同时，以上的对于找到目标节点的路径在该处同样适用。根据以上的认识，对于具体适应值长度的计算公式如下：

(5)

1.3.5选择策略

选择的是锦标赛选择算法。通过以上的过程，生成的路径包括初始种群所生成的路径N条，变异、交叉过程生成的路径N条与模拟退火算法生成的路径1条，共计2N+1条。将其中适应值最佳的路径对应的字符串直接放入下一代种群，然后将剩下的2N条路径分为N-1组，其中每组的路径数为L=2N/N-1，通常L是除不尽的，采取的是向下取整的方式。

通过这种方法，在每一次的迭代过程中，既保证了最佳的路径进入了下一代种群，同时也保证了其在状态迁移图中的搜索不会过于集中，影响搜索的效果。算法过程见算法3，其中N表示种群的大小。

算法3选择策略

1.将当前路径集合中最佳的路径对应的字符串放入下一代种群

2.从集合中删除该路径

3.fori=1∶2->(N-1)

4.从剩余集合中随机选择L条路径

5.将L条路径中适应值最佳的路径对应的字符串放入下一代种群中。

6.从集合中删除已经选择过的路径

7.end for

基于以上内容，提出的算法具体流程如图2所示。

图2 死锁检测流程框图

3 实验与分析

采用Matlab实现了所设计的算法。采用随机构造了多组含有死锁节点的状态空间图并与多种算法相比，进行了下述实验。分别是在不同状态空间大小下2种算法所生成迁移数量的变化和所生成反例长度之间的变化。

在以上的搜索中，限定的最大迭代次数为100次。

图3表明了算法迭代次数与状态空间大小的关系。

图3 迭代次数与状态空间大小的关系曲线

从图3中可以看出，算法在寻找目标路径的过程中，随着状态空间的增大，迭代次数并不是一直保持线性增加，当状态空间达到一定的大小时，迭代次数的增加会减缓。即表明该算法在状态空间一直增大的情况下，依然可以保证一定的寻找目标路径的速度。

同时比较了在采用Cr自适应参数和固定Cr的情况下，算法的收敛情况。可以看出，在前期状态空间较小的情况下，两者的收敛速度相差不大，随着状态空间的扩大，设置了自适应Cr参数的算法能够拥有更快的收敛速度。

图4表明随着状态空间的变化，4种模型检测算法所生成反例长度的变化，其中包含了3种不确定算法和一种确定性算法。

从图4中可以看出，基于启发式因子选择下一步节点的不确定算法与盲目搜索确定性算法相比，可以更快地找到目标节点，从而得到更短的反例。随着状态空间的增加，差距也会越来越大。

而与其他2种带有启发式因子的算法相比，由于在引导搜索方向上的优化，提出的算法在寻找最短反例上的表现也是更优的。

图5表明了4种算法在进行检测时，在状态图中所生成的迁移数量的关系。可以看出，启发式算法在生成更少的迁移，即在搜索相对较少状态空间的情况下能够找到死锁节点，且在状态空间增大的情况下，其生成迁移数量的增大幅度也小于传统的确定性算法。从而证明了该带有启发式因子的算法在检测时有更高的效率，在搜索较少的状态节点的情况下，就能够完成对于死锁的检测。

图5 生成迁移数与状态空间大小的关系曲线

同时对于3种不确定算法，提出的算法在搜索状态空间的表现上仍然优于其他2种算法。这也是通过引导搜索方向和加速收敛带来的优势。

图6表明了随着状态空间的增大，4种算法检测用时的变化。可以看出，在状态空间较小时，4种算法检测用时差距不大，但是在状态空间过大时，BFS由于是盲目搜索，与3种带有启发式因子的算法相比，其检测用时极大，且增大幅度也是。相比于3种不确定算法，由于提出的算法优化了引导搜索的环节和加速收敛的方法，其检测用时也均小于其他2种。

图6 检测用时与状态空间大小的关系曲线

分析上述多个实验可知，设计的基于差分进化算法的模型检测算法，对比传统的确定性算法BFS，其生成的反例长度和探索的迁移关系都远小于BFS。同时，与其余不确定性算法相比，也优于其余2种算法。证明了在检测死锁方面，该算法能够在搜索较少状态空间的前提下，生成较短的反例，更有利于分析错误。

4 结论

1) 提出了一种新的启发式模型检测搜索算法，经过实验证明，可以有效提高死锁检测的效率。

2) 针对路径的特殊性，提出一种路径生成算法，有效减少了不确定算法框架带来的后续操作的复杂性。

3) 在差分进化算法原有框架下，增加额外的模拟退火操作，跟随迭代次数自适应的Cr值，用以提高算法表现，加速算法的收敛。同时根据死锁检测的具体背景，设计了新的适应值函数用以评估路径的优劣性。

未来的工作中，将扩展所提出算法的适用场景，使其能够检测更多的性质。同时将该算法与其他技术相结合，如偏序规约、抽象技术等，进一步降低搜索所需要的内存空间，即减少所生成的状态图大小。最后，基于以上的设想，开发出实际的模型检测器。