模型检测空间分解分布式算法的优化与研究

潘怀宇，龙士工，郑　涵

(贵州大学 计算机科学与技术学院，贵州 贵阳 550025)



模型检测空间分解分布式算法的优化与研究

潘怀宇，龙士工*，郑涵

(贵州大学 计算机科学与技术学院，贵州 贵阳 550025)

模型检测对于系统的校验有着适用范围广、自动化验证程度高、验证速度快等优势。但是其状态爆炸问题制约了其应用，使用分布式技术缓解状态爆炸问题引来了新的问题——如何对状态空间进行分解。本文介绍了分布式SCC分解的两个算法：FB与MP-MS算法，并在其基础上，引入了OWCTY技术，对算法进行优化。通过实验，证明优化后的算法有着更高的效率和更小的时间开销，对于缓解状态爆炸问题有着重要的意义。

模型检测;状态爆炸;OWCTY;分布式技术

日常生活中，人们对于ICT系统(Information and Communication Technology)的依赖正在迅速增长。随着需求的增长，这些系统的结构与分层也越来越复杂，类似的复杂系统我们随处可见，比如智能卡、个人PC、手机和智能家居等。对于此类系统的可靠性、正确性与安全性保障，是系统在设计过程中的一个关键问题。模型检测[1](Model Checking)作为形式化验证方法的主要技术之一，其实质是基于时序逻辑(LTL，CTL)的计算机自动化形式验证的方法，利用穷举搜索状态空间来检验既有模型与一个时序逻辑公式，验证该系统模型是否满足此时序逻辑公式描述的具体性质。模型检测技术适用范围广、自动化验证程度高、验证速度快，只要计算机有足够的处理能力，最终总能终止并给出验证结果，当验证属性不满足时，还可以给出反例(Counterexample)，便于发现错误并进行修改。

模型检测方法的严重缺陷是“状态爆炸(state explosion)问题”。如图1所示，随着检测的系统规模增大，其状态空间由mn变大为mn1，模型检测算法需要的时间、空间开销呈指数增长，当一个系统的并发分量非常多时，对其状态空间进行直接穷举搜索在实际上是不可行的。

图1　状态爆炸问题

分布式作为计算机科学当前的热门技术，主要研究如何把一个需要巨大计算能力才能解决的问题分成若干部分，然后把这些部分单独处理，最后综合以得到最终结果。其为解决状态爆炸提供了良好的思路。可以将全局状态空间分解，多处理单元对各个子空间单独验证，最后得出验证结果，理论上可以节约时间开销。该思路的难点是全局状态空间的分解。

本文中将系统有向图的强连通分量(SCC)作为子状态空间进行划分，在整个空间状态图中寻找强连通分量。关于该问题的一个有效算法是基于深度优先算法(DFS)的Tarjan算法，给定一个含有n个顶点，m条边的图，该算法能够在O(n+m)的时间和O(n)的空间内，识别并列出所有的强连通图。但是，Tarjan算法所使用的DFS算法的并行化已经被证明是困难问题，所以想要使用Tarjan算法来实现分布式的目的就非常困难。

本文中，我们将列出了两种已有的分布式SCC分解算法：FB与MP-MS算法，给出算法思想与伪代码，以及相关技术。并在其基础上进行改进，引入OWCTY技术，提出改进算法O-BF算法。进行实验，来比较各算法在时间开销上的效率，比较的对象是Tarjan算法。

1　准备知识

在介绍算法和相关技术之前，我们需要先了解一下分布式算法所涉及到的相关知识。

1.1分布式算法

分布式计算研究把一个大的问题分割成若干部分，使用多个处理单元分别处理，最后获得结果。表1给出了分布式求π的例子来说明分布式算法的应用，同时给出了使用单线程串行求解与多线程并行求解的时间开销对比。

用数值积分法计算π，要求出在区间[0，1]内函数曲线4/(1+x2)下的面积，此面积是π的近似值，为此先将区间[0，1]划分成N个等间隔的子区间，每个子区间的宽度为1/N；然后计算出各子区间中点处的函数值；再将各个子区间面积相加就可得出π的近似值。其计算公式为：

表1　数值计分法求π，单线程串行与 多线程并行时间开销对比

1.2有向图

对于SCC的分解，首先要了解有向图的相关定义。一个有向图可以表示为一个二元集合(V，E)，其中V是图中顶点的集合，而E∈V×V，是有向边的集合。如果(u，v)∈E，则称u是v的直接前驱，v是u的直接后继。对于顶点v，它的直接前驱u的数目称为顶点的入度。对于图G=(V，E)，将它所有的有向边反转，得到它的换位图(transposed graph)GT=(V，ET)，其中ET={(u，v)|(v，u)∈E}。

假设E*为有向图G=(V，E)的传递和自反闭包，s，t∈V是图中的两个顶点。如果(s，t)∈E*，则称顶点t是自顶点s可达，如果有一顶点序列：s0，s1......sk，s.t.(si，si+1)∈E，如果sk是自s0可达的，则这一顶点序列称为一条路径。如果路径上不包含重复的顶点，则称该路径是一条简单路径，其长度为k，即边的数目。

在有向图中，顶点集合C满足C∈V，如果任意两个顶点u，v∈C，满足顶点v都是自顶点u可达，则称C是有向图中的一个强连通分量(SCC)，如果有向图任意强连通分量C*，满足C⊄C*⊆V，则称该C为一个最大强连通分量。

v∈W∈V、Ew={(x，y)∈E∧x，y∈W}，图(V，Ew)中所有可达顶点v的顶点集合称为顶点v的向前闭合(forward closure)，同理顶点的向后闭合(backward closure)指的是自顶点可达的所有顶点集合。

对于一个显示的有向图，在计算机中通过邻接表或邻接矩阵来描述。对于一个隐式图(隐式图指的是它有一个初始顶点和一个限定函数返回任意顶点的直接后继)，比如说对于一个系统，它的有向图描述不能直接描述，需要通过算法将其转化为一个有向图，文献[2]中就提到了两种隐式图的描述算法，在本文中使用工具Divine，直接将系统转化为有向图。

1.3可达性关系

可达性关系的计算是SCC分解算法中的核心，主要是查找从一个给定的顶点可以到达的所有顶点，即计算其向前闭包。图的标准广度优先搜索或深度优先搜索都可以实现这样的效果，其空间复杂度为O(n)，时间复杂度O(m+n)。

可达性程序是SCC分解算法的第一步，该部分的算法的并行化经过多年研究已经成为了一种标准技术[3-5]。可达性程序的并行化技术中，一个分区函数将顶点分配给多个处理器。每个处理器负责搜索由分区函数分配给它的顶点，包含一组已访问的顶点和一个待访问顶点的列表。

本文描述的算法中既提到了向前可达性，也使用到向后可达性的概念。一个向后可达性程序的功能就是确定所有自给定顶点可达的顶点。

1.4中值点选择

无论是向前可达点的搜索，还是向后可达点的搜索，都需要算法从某个指定的点开始，这个给定的点，称之为中值点。中值点的选取对于算法的复杂度有很大的影响。如果我们选择的中值点所向前向后可达性遍历的顶点集合中没有已经被分解出来的点，那么相应的所有顶点，可以只使用在中值点发起的单个向前可达性来鉴定。可是挑选满足上述条件的中值点，需要使用到深度优先搜索后顺序。本文算法中是随机选择中值点，中值点选取的并行化仍是一个很好的研究方向。

2　算法

介绍了相关知识之后，我们接下来会首先介绍两个基本的分布式SCC分解算法，再提出一个基于此算法的改进算法，并分析其可行性。

2.1FB算法

FB算法是SCC分布式分解的基础算法，图2给出了算法的基本步骤：首先，在图中随机选择中值点，然后从中值点开始向前、向后进行遍历，此过程将图分成四个独立的子图。图中顶点分别是：在向前遍历区域不在向后遍历区域、在向后遍历区域不在向前遍历区域、既在向前遍历区域又在向后遍历区域以及既不在向前遍历区域又不在向后遍历区域。既在向前遍历区域又在向后遍历区域中的点所组成的子图就是一个SCC，不需要再进行分解。而其他三种子图，则需要进行进一步分解。图3中给出了该算法的伪代码：

图2　FB算法步骤

图3FB算法伪代码

算法包括中值点选取PIVOT、向前向后遍历。向前向后两个可达性遍历过程有两个参数：中值点和状态集(顶点集合)。该算法的复杂度为O(n·(n+m))。

2.2MP-MS算法

算法MP-MS[6]是FB算法的改进版本，使用了最大前驱和最大后继的概念。相比于FB算法，主要的不同是在图的遍历过程，为了计算出顶点的最大前驱和后继(文献[7]中给出了一个算法来计算最大前驱与后继)，使用并行程序FWD-MAXPRED和BWDMAXSUCC替换FWD和BWD程序。除了遍历向前向后可达性关系以外，新的程序还可以根据前驱和后继的最大值来划分子图，图4给出了其子图划分，并返回子图中的顶点，得到前驱列表及后继列表，可以被用于对划分的子图进行递归调用。图5给出了算法的伪代码：

图4　使用最大前驱与最大后继来划分子图

图5MP-MS算法

2.3O-BF算法

在使用FB算法或者MP-MS算法之前，我们观察到，给定一个有向图，对其进行SCC分解，有很多不需要考虑的状态点。一个SCC中的任何顶点都需要满足至少有一个前驱和后继，也就是说，一个没有任何前驱或后继的点必然不属于SCC，基于此思考，可以在使用上述FB、MP-MS之前对图进行约减。

在这样的思想上，本文引入了OWCTY技术[4](单项约减消除技术)来对图进行处理，图6是对 OWCTY技术的代码描述。

图6OWCTY技术

OWCTY算法有三个参数，G表示待分解的图，F表示可接受状态集，init_state表示初始状态点，reachability(S∩F)遍历出所有自初始状态点可达顶点集合。elimination(S)查找出的顶点集合满足：顶点属于S中某个环或自S中某个环中任意顶点可达。

以图2为例， LT和TT顶点可以被OWCTY识别，其没有前驱或后继将被消除，消除这样的顶点会产生新的顶点，这些顶点中也会有顶点没有前驱或后继，递归使用OWCTY消除。随着无用顶点的消除，图的规模越来越小，图中的平凡组件可能会成为图中的头或尾节点。图2中包括三种平凡组件(Trivial components)：LT、TT以及既不是头也不是尾的平凡组件(T)。

O-BF算法的核心思想就是将OWCTY技术与FB算法相结合，先使用OWCTY将图中无用的顶点消除，再使用FB算法进行SCC分解。

该算法将重复使用OWCTY技术对图进行无用点的消除，每次迭代将会得出一个OBF子图，然后对每一个OBF子图进行FB分解。图7与图8分别给出了OBF算法的伪代码和步骤描述:

图7OBF算法

图8　OBF算法的两个步骤

程序从初始顶点开始(图中没有直接前驱的节点)。OWCTY消除过程遍历所有初始顶点的直接后继，消除所有没有前驱的顶点，图中有叉的顶点是OWCTY消除过程不可消除的顶点。从这些点进行一次向后可达性遍历，得到一个OBF切片(顶点集合B)。伪代码第8行开始使用FB算法并行执行，对OBF切片进行分解，得出一个SCC。将当前SCC中顶点的直接后继(不属于该SCC中的顶点)作为新的初始顶点，递归调用OBF算法，最终可以在O(n·(n+m))时间内得到所有的SCC。

3　实验与结果

下面将在算法基础上进行编程实验，实验环境为：机器A:8G Rom，2.60 GHz Cpu，4 Cores。机器B:6G rom、2.80 GHz、2Cores。

本文实验中使用的系统(电梯调度算法、Peterson算法和Rether9_2)都来自DiVine[8]工具库。在表2中列出其相关参数，包括：名称、顶点与边数目、平凡以及非平凡强连通图的数目、使用Tarjan算法所需要的时间。

表2　系统参数

实验得出表3中的结果，其算法时间开销对比如图9所示：

表3　实验结果(n.a表示2个小时内得不出结果)

图9　算法时间开销对比(min)

对于结果进行分析，发现：

(1)当前实验环境下，对于MP-MS算法，基于最大前驱与后继的改进算法实际效果并不是很好，其所花费的时间开销远远大于其他算法。

(2)在处理单元数目不是很多的情况下，分布式SCC基础算法FB的效果并没有串行算法Tarjan效果好。

(3)实验结果表面，使用OWCTY技术的OBF算法对于时间开销上的优化非常明显，即便是处理器数目不是很多的情况下，时间上也提高了10%以上。

最后，根据我们的实验，改进后的OBF算法对于图的SCCs分解在时间开销上要优于串行的Tarjan算法。

4　结语

对于模型检测的状态爆炸问题，可以使用分布式技术一定程度上缓解。而对于其全局状态空间的划分，可以使用相应的算法改进效率。

本文详细介绍了相关的分布式SCC分解算法，并对其进行优化，实验结果表明，优化后的O-BF算法效果明显，算法的效率有了显著的提高。

本文仅使用了简单的多线程编程来进行实验，线程间的通信问题有欠考虑，时间开销还有进一步优化的空间，另外，在中值点的选取方面都有可以优化的空间。

[1] Baier C， Katoen J P. Principles of model checking[M]. Cambridge: MIT press， 2008.

[2] Garavel H， Mateescu R， Smarandache I. Parallel state space construction for model-checking[M]. Berlin Heidelberg: Springer-Verlag， 2001: 217-234.

[3] Blom S， Calamé J R， Lisser B， et al. Distributed analysis with μCRL: a compendium of case studies[M]. Berlin Heidelberg: Springer-Verlag， 2007: 683-689.

[4] Fisler K， Fraer R， Kamhi G， et al. Is there a best symbolic cycle-detection algorithm?[M]. Berlin Heidelberg: Springer-Verlag， 2001: 420-434.

[5] Lerda F， Sisto R. Distributed-memory model checking with SPIN[M]. Berlin Heidelberg: Springer-Verlag， 1999: 22-39.

[6] Sminia T， Orzan S M. On distributed verification and verified distribution[D]. Amsterdam: Vrije Universiteit， 2004.

(责任编辑：曾晶)

Optimization and Research of Distributed Algorithm for Model Checking Space Decomposition

PAN Huaiyu，LONG Shigong*，ZHENG Han

(College of Computer Science and Technology， Guizhou University， Guiyang 550025， China)

Model Checking has many advantages in system verification: wide range of applications， high degree of automation and high speed. But its state explosion problem restricts its application. Using the distributed technology to mitigate state explosion leads to a new problem -- how to decompose the state space? Two algorithms about distributed SCC decomposition were described: FB and MP-MS algorithm. Then the OWCTY technology was applied in optimizing these two algorithms. Through the experiment， the results show that the optimization algorithm has a higher efficiency and less time cost. It has important significance to alleviating the problem of state explosion.

model checking;state explosion; OWCTY; distributed technology

A

1000-5269(2016)03-0086-05

10.15958/j.cnki.gdxbzrb.2016.03.21

2015-12-07

国家自然科学基金(61163001

潘怀宇(1991-)，男，在读硕士，研究方向：密码学与可信计算，Email：578943277@qq.com.

龙士工，Email：526796467@qq.com.

TP301