非交互式Petri网可覆盖性验证的高效实现*

丁如江, 李国强

(上海交通大学 软件学院,上海 200240)

近年来,基于 Petri网的模型检测技术已经成功地应用于并发程序的验证与分析[1-4]中.Petri网是一种适用于描述并发程序的模型,德国学者Sistla[5]首次提出了使用 Petri网来为程序建模的方法.具体来说,可以用Petri网模型中的位置(place)表示程序的状态,用模型中的迁移(transition)表示程序的执行流,以及每个位置的令牌(token)数表示当前有多少个进程刚好运行到该位置.

并发系统的安全性问题是指系统是否会有可能进入某一错误状态(比如需保证进程互斥的系统发生了多个进程同时运行到某一关键位置),规约到Petri网的可覆盖性问题为:给定一个Petri网和一个状态M(对应到并发系统中的一个错误状态),是否会有一些由初始状态M0可达的状态M′覆盖了M.如果存在可达状态覆盖错误状态M,就表明模型对应的系统不是绝对安全的,系统在理论上会覆盖这个错误状态.现有的验证Petri网可覆盖性的算法大致分为两类:一类是基于Petri网状态空间的遍历,通过搜索Petri网的可达状态空间来判断是否覆盖待验证状态M.然而,由于Petri网的状态空间规模与其位置迁移数是指数级别关系,所以这类算法在面对规模较大的Petri网时都显得力不从心.比如BFC[4]、MIST、IIC[6]等工具都会有超时的问题存在.第2类是基于约束的,从Petri网的模型结构以及待验证状态中提取出约束条件,然后去求解这些约束来验证可覆盖性.然而由于约束的表达能力有限,不可能完美地表达出Petri网的可达状态空间,所以这些约束条件只能成为可覆盖性问题的必要而非充分条件.因此,这类算法在理论上是不完备的,比如Petrinizer[7]工具只能验证那些安全的测试用例,对于不安全的测试用例则无法判定.

本文针对非交互式Petri网(communication-free Petri net),又被称作基本并发进程(basic parallel processes,简称BPP),设计并实现了可以高效验证其可覆盖性的工具(communication-free Petri net coverability verifier,简称CFPCV).BPP在模型上的计算相对简单,其可覆盖性问题是NP完备问题[8],同时,它又能为一类并发程序建模并且进行验证.我们采用基于约束的方法,从非交互式Petri网的模型结构和待验证状态中提取出约束,然后将这些约束交给Z3 SMT求解器求解.如果求解器得出无解,则说明不存在任何可达状态覆盖待验证状态,即待验证状态不可覆盖.而如果求解器有解(可能有多组解),并不能说明待验证状态可覆盖,因为约束条件的表达能力有限,满足约束条件的状态并不一定是该非交互式Petri网的可达状态,需要额外增加子网可标记方法去验证该状态是否可达.如果验证通过,则说明待验证状态可覆盖.如果没有通过,则需要迭代地去验证其他满足约束条件的状态,直到最终得出结论,这样就保证了该工具的算法在理论上是完备的,不存在无法判定的情况.同时,只要对我们的约束条件稍加修改,CFPCV就可以很容易地验证BPP的可达性问题.

我们通过一个实例来说明基于约束验证 BPP可覆盖性问题的方法,图 1展现的是包含两个进程的并发程序及其对应的非交互式Petri网.

假定该并发程序需要维护一个写锁,即同一时刻最多只能有一个进程可以获取锁来写文件,对应到非交互式Petri网为最多只能有1个进程可以处在位置c,所以该非交互式Petri网必须满足c≤1(即位置c内的令牌数量不大于1)的性质,也就是说,满足c≥2的状态都是错误状态.我们通过基于约束的方法来验证该非交互式Petri网是否会覆盖满足c=2的状态.首先根据BPP的模型要求,每个位置内的令牌数以及每个迁移的触发次数都必须大于等于 0,可以得到约束集{lock≥0,not lock≥0,c≥0,t1≥0,t2≥0,t3≥0,t4≥0,t5≥0,t6≥0}.然后根据位置和迁移的转移关系得到约束集{lock=2+t5+t6–t1–t2,not lock=0+t1+t2–t3–t4,c=0+t3+t4–t5–t6}.最后加入待验证状态的约束集{c≥2}.将这些约束集合并作为输入交给Z3 SMT求解器求解,得出一个解{lock=0,not lock=0,c=2,t1=1,t2=1,t3=1,t4=1,t5=0,t6=0}.之后通过子网可标记验证发现这组解确实是合法解,我们就可以判定该非交互式Petri网可以覆盖满足c=2的状态,从而说明对应的并发程序是不安全的,可能会存在两个进程同时得到锁一起写文件的情况.

本文第1节介绍所用到的背景知识,包括传统Petri网、非交互式Petri网、可达性和可覆盖性问题的数学定义,以及本文所使用到的Z3 SMT求解器介绍.第2节介绍验证非交互式Petri网可覆盖性的安全性方法以及子网可标记验证技术.第3节介绍CFPCV的总体技术框架以及使用的算法细节.第4节主要介绍实验及实验结果的分析.第5节介绍Petri网可覆盖性研究的一些相关工作.第6节总结全文,并展望未来的工作.

1 预备知识

1.1 Petri网

Petri网可以用一个四元组N=(P,T,F,M0)来表示,其中,P是Petri网中所有位置的有限集合,T是Petri网中所有迁移的有限集合,F:(P×T)∪(T×F)→{0,1}称为Petri网的流函数,它表示位置和迁移之间的连接关系.而M0表示该 Petri网的初始状态.对于x∈P∪T,·x={y∈P∪T|F(y,x)=1},x·={y∈P∪T|F(x,y)=1}.·x记为x的前集或者输入集,x·记为x的后集或者输出集.Petri网的状态M是一个从位置集合P映射到自然数的向量:P→ℕ,该向量内的元素M(p)表示当前状态下位置p内的令牌数.

Petri网的可达性问题是指给定一个Petri网N=(P,T,F,M0)和一个状态M,判断M∈R(M0)是否成立,即判断状态M是否由M0到达;可覆盖性问题是指给定一个Petri网N=(P,T,F,M0)和一个状态M,判断是否存在一个状态M′∈R(M0),满足∀p∈P,M′(p)≥M(p).如果存在,则称该 Petri网覆盖状态M.

1.2 非交互式Petri网

非交互式Petri网是指满足∀t∈T,|·t|=1,即每个迁移的输入位置数量为1的Petri网[8].它的可覆盖性问题复杂度从Petri网的EXPSPACE完备降低到了NP完备.

1.3 SMT求解器

SAT问题被证明是第一个NP完备问题.作为SAT问题的扩展,SMT问题[9]处理的对象是一阶逻辑公式,相比于命题逻辑,增加了谓词和量词,很大程度上增强了SMT公式的表达能力.用以求解SMT问题的自动化工具称为SMT求解器.SMT求解技术在有界模型检测、基于符号执行的程序分析、线性规划和调度、测试用例生成以及电路设计和验证等领域有非常广泛的应用.很多科研机构以及公司都在致力研发正确率高、性能优异的SMT求解器,并且已经成功应用到了具体的领域.目前流行的SMT求解器有:Barcelogic[10]、Beaver[11]、Yices[12]以及Z3[13]等.其中,由微软公司主导开发的Z3 SMT求解器所支持的理论最多,性能也最好,因此本文使用了Z3 SMT求解器作为我们的求解引擎.

2 安全性方法与子网可标记验证

本节主要介绍验证非交互式 Petri网可覆盖性所用到的安全性方法以及子网可标记验证技术,在介绍安全性方法之前,我们首先介绍其核心——状态方程的概念,最后介绍两个加速剪枝的技巧.

2.1 状态方程

对于一个给定的非交互式Petri网N=(P,T,F,M0),用一个大小为|P|的列向量M表示N的当前状态,用一个大小为|T|的列向量X代表迁移序列σ中每个迁移触发的次数,那么状态方程表示为

其中,C称作关联矩阵,它是一个|P|×|T|大小的矩阵,它的每一项的值按如下方法计算:

显然,关联矩阵记录了该非交互式Petri网中每一个位置与迁移之间的连接关系.而X是迁移序列σ中每个迁移触发的次数.可以用Parikh映射(Parikh mapping)来表示它们之间的关系:

其中,ω(ti)代表迁移ti在迁移序列σ触发的次数.

比如对于图3给定的非交互式Petri网和一个迁移序列σ=t1t2t1t3t2t1,就可以根据状态方程计算出σ触发后的新状态M=[5,3,3,1,–1]T,其中,

2.2 安全性方法

安全性方法(safety method)是验证非交互式 Petri网可覆盖性的基本方法,顾名思义,其目的就是为了验证非交互式Petri网对应的并发系统是否安全.其基本思想是给定一个非交互式Petri网N和一个性质φ,如果根据状态方程M=M0+CX得出的所有状态都不会违反¬φ,则该非交互式Petri网一定满足性质φ.值得注意的是,如果状态方程得出的某一个状态M′满足了¬φ,并不能说明该非交互式 Petri网违反性质φ.因为前文有提到,状态方程得出的状态空间Set(M)是可达状态空间R(M0)的超集,所以违反性质φ的状态M′不一定是该非交互式Petri网的可达状态.因此,安全性方法在理论上是不完备的,它只能在一个方向进行验证,这也是安全性方法的局限所在.

本文只讨论满足如下条件的非交互式Petri网.

1) 在任何合法的状态下,每个位置的令牌数必须大于等于0.

2) 在任何合法的迁移序列中,每个迁移的触发次数必须大于等于0.

结合状态方程可以用如下约束条件表示[7]:

安全性方法用约束条件来表达就是将C(N)约束与待验证性质φ的取反结合,表示为

约束(1)可以表示成多元一次等式和不等式的组合,而 SMT求解器可以很快地求解这些等式与不等式的组合.将约束(1)作为输入交给SMT求解器求解,得出:

1) 无解,则说明状态方程得出的状态都不会违反性质φ,即Set(M)|=φ,又因为R(M0)⊆Set(M),所以R(M0)|=φ,继而推出该非交互式Petri网N|=φ.也就说明对应的并发系统是安全的.

2) 有解,则说明存在某状态M′违反性质φ,但由于Set(M)⊇R(M0),所以M′不一定是该非交互式Petri网N的可达状态,因此无法判定N是否满足性质φ,这也是安全性方法的局限所在.下一小节提出的子网可标记验证方法,可以有效地判定候选状态M′是否是N的可达状态,从而弥补了安全性方法的不足.

2.3 子网可标记验证

前文介绍了验证非交互式Petri网可覆盖性的安全性方法,虽然该算法借助于SMT求解器可以很高效地运行,但是该算法在理论上却不完备,只能验证非交互式Petri网N满足性质φ,却无法得出N不满足性质φ的结论.原因是安全性方法依赖于状态方程,对于状态方程得出的候选状态M′,我们无法判断M′是否是N的可达状态.

而子网可标记验证可以严谨地判定某个状态M′是否是非交互式Petri网的可达状态,从而可以弥补安全性方法的不足,在验证非交互式Petri网可覆盖性时达到理论完备.

在介绍如何使用子网可标记验证判定状态M′是否为非交互式Petri网的可达状态之前,需要引入如下的定义、引理与定理[8].

定义 1.给定一个 Petri网N=(P,T,F)和一个迁移集合T的子集S,那么由S构成的N的子网NS=(PS,S,FS).

定义2.给定一个Petri网N=(P,T,F,M0)和一个状态M:

· 如果存在一个状态M′,使得M′由M可达,且M′(p)>0(其中,p∈P),则称位置p由状态M可标记.

· 对于N的子网N′=(P′,T′,F′,M0′),如果N上的状态M在N′上的投影为M′,且位置p(其中,p∈P′)由状态M′可标记,则称位置p在N′上由M可标记.

引理1.给定一个非交互式Petri网N和它的一个状态M,一个位置p由状态M可标记当且仅当N中存在一条从p′到p的路径,其中,p′满足M(p′)>0.

引理1给出了一个在非交互式Petri网N上,快速判定位置p是否由状态M可标记的方法,即如果在M状态下内部令牌数大于0的某个位置p′,存在一条到位置p的路径,那么就可以说明位置p在N上由M可标记.也就是说,对于M状态下内部令牌数大于 0的位置,从这些位置经过迁移可以到达的位置都是由状态M可标记的.

例如,针对图3所示的Petri网,给定向量X=[1,0,0]T,则子网NX如图4所示,包含p1,p2,p3,p4这4个位置,t1一个迁移以及它们之间的流关系.在子网NX中,显然,p1,p2,p3,p4都由状态M0可标记,因为M0状态下,p4内的令牌数大于0,且p1,p2,p3都由p4可达.

2) 子网NX内的任一位置都能在NX上由M0可标记.

定理 1给出了判定一个迁移触发次数的向量X是否合法的充要条件,即在向量X的作用下,该非交互式Petri网的每个位置内的令牌数必须大于等于0,而且子网NX内的所有位置都必须由M0可标记.结合定义2和引理 1,则定理 1的条件 2)可以表述为:NX内的所有位置都必须由M0X可标记,即∀p∈PX,NX中都存在一条从p′(p′∈PX)到p的路径,其中,p′满足M0X(p′)＞0.如果X满足定理1的两个条件,则可以说明X合法,那么X作用下的状态M就是可达状态,因为M可以由M0通过σ到达.这样一来,我们就将判定非交互式Petri网上某个状态是否可达规约到其对应的迁移触发次数向量X是否合法,使得问题变得更加具体,更加便于操作.

对于传统的 Petri网,我们很难判定某个状态是否是可达状态.而对于非交互式 Petri网,结合状态方程与定理 1,可以有效地判定某个状态是否可达.我们可以通过状态方程M′=M0+CX′求得M′对应的解X′(可能有多个解),然后再去验证X′是否合法,如果合法,就可以得出M′可达的结论.而如果不合法,则可以迭代地去验证其余解,如果所有的解都不合法,就可以断定M′不可达.

在安全性方法中,任何非交互式Petri网N=(P,T,F,M0)都必须满足C(N)约束,规定了在任何状态下每个位置内的令牌数都必须大于等于0,所以,定理1的第1个条件天然满足.至于第2个条件,在安全性方法中,如果约束(1)有解(可能有多组解),即∃M′∈Set(M),¬φ(M′)成立.我们可以通过定理 1 来判定M′是否可达,即判定其对应的X′是否合法.这样就可以严格地去验证非交互式Petri网是否覆盖某个错误状态,使得算法在理论上达到完备.

结合安全性方法与子网可标记验证,验证非交互式Petri网可覆盖性的方法可以表述如下.

以太网INTERNET模块程序主要包括通过Xbee协调器对Xbee终端数据的接收与发送，以太网模块W5100数据上传与服务器控制命令的接收，其流程图如图4所示.以太网模块程序首先配置网络IP地址、DNS服务器等数据，再利用LEWEI50云平台TCP通讯协议库＜LeweiTcpClient.h＞实现数据上传、远程开关的反向控制.

从非交互式Petri网N和待验证性质φ中获取约束条件C(P,T,F,M0)^¬φ,作为SMT求解器的输入进行求解.

1) 无解,即约束条件不满足,说明该非交互式Petri网的所有状态都满足性质φ,N不会覆盖满足性质¬φ的错误状态.

2) 有解,即∃M′∈Set(M),¬φ(M′)成立.我们需要去验证M′对应的X′是否满足定理 1 的第 2 个条件.

a) 若满足,说明¬φ会被一个可达状态满足,表明N不满足性质φ,N会覆盖满足性质¬φ的错误状态.

b) 若不满足,说明满足¬φ的状态M′不可达.由于满足约束C(P,T,F,M0)^¬φ的状态可能有多个,所以需要加上新的约束条件剔除状态M′,继续交给SMT求解器求解,进行下一次迭代(注:由于约束(1)中等式的数量可能少于变量的个数,且约束中存在不等式,所以约束(1)的解的数量可能是无限的,而且可能存在需要无数次迭代的极端情况.不过,从之后的测试发现,多次迭代的情况非常少.当然,约束(1)解的数量并不等于迭代的次数,因为每次迭代并不一定只排除一个解,也可能是一组甚至无数解,可以参考第 3.3节中的实例,而排除解的数量在不同的模型中也互不相同,所以约束(1)解的数量和迭代次数之间的关系并不能用确切的表达式来表达.甚至可能存在约束(1)解的数量无限,但是只需要几次迭代即可成功验证的情况).

2.4 剪枝技巧

因为对于 SMT求解器的每组解,我们都需要验证其是否符合定理 1的条件 2),为了减少算法的迭代次数,我们可以增加两种剪枝加速的方法.

1) 在给定的非交互Petri网N=(P,T,F,M0)中,对于那些满足M0(p)>0的位置,它们的输出迁移必须至少有一个触发次数大于0.约束化为Constraints1.

因为我们要验证每组解是否符合定理1的条件2),也就是子网内的每个位置都要由M0可标记.由引理1可知,该子网内至少有一个位置p满足M0(p)>0.因此,如果Constraint1无法满足,也就是说,满足M0(p)>0的位置p根本没有路径“出去”,则子网内的其他位置p′都无法由M0可标记.

2) 在给定的非交互Petri网N=(P,T,F,M0)中,如果存在这样的位置,InitPlace集合中的任意一个位置都不存在一条到它的路径,那么它的输入和输出迁移发生的次数都为0.约束化为Constraints2.

因为对于这些无法从InitTransition中的位置到达的位置,它们在任何状态子网上都是无法由M0可标记的,如果它们的输入或者输出迁移发生的次数大于 0,那么子网就必须将这些位置包含进去,那么该子网就不可能满足定理1的条件2).

使用上述两种剪枝技巧,可以有效地减少算法的迭代次数,使得验证更加高效、实用.

3 CFPCV工具技术框架

我们采用基于约束的方法,实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV,它在安全性方法的基础上,加上子网可标记验证,从而使得该算法在理论上完备.本节主要介绍 CFPCV工具的技术架构以及使用到的具体算法.

3.1 技术架构

本文的技术方案如图5所示.主要分为约束提取、约束求解、候选解验证、增加约束进行迭代这4个部分.具体内容如下.

1) 首先根据给定的非交互Petri网模型N=(P,T,F,M0)得到一些模型的基本约束,例如每个位置内的令牌数必须大于等于 0,每个迁移发生的次数必须大于等于 0,再根据需要验证的状态M得到状态约束,例如待验证性质为p1=1&p2=1,则约束p1≥1&p2≥1可以覆盖满足此性质的状态.

2) 将步骤1)得到的约束条件和剪枝技巧合并为约束文件,作为输入交给SMT求解器求解.

3) 如果无解,则表明不存在满足这些约束条件的状态,也就是说,N不能覆盖状态M′;如果有解并不能代表N覆盖状态M,只能代表M′满足这些约束条件,还必须验证M′由M0可达,即需要将状态M′从状态方程的状态空间压缩到该非交互式Petri网的可达状态空间内.

4) 如果验证出M′状态确实由M0可达,则可以表明N覆盖M;如果不可达,说明SMT求解器求出的这组解(基于约束条件可能有很多组解,求解器每次只给出一组解)不满足要求.需要将状态M′代表的这一类状态剔除,即生成新的约束加入到约束文件中,重复步骤3)和步骤4),直到程序得到解退出为止.

3.2 算法实现

CFPCV工具使用到的核心算法伪代码如下.

关于算法的逻辑,前文已经解释清楚,主要分为约束提取、约束求解、候选解验证、增加约束进行迭代这4个部分,这里不再赘述.其中,第 8行的代码表示提取新约束来剔除子网SN所代表的一系列解.比如,T={t1,t2,t3,t4},X={1,0,3,1}.那么,SN就是根据t1,t3,t4这3个迁移构成的子网,如果子网SN不满足定理1的条件2),则在下一次迭代中,必须增加约束将SN所代表的一系列解剔除,即新约束δ为not(t1>0 &t2=0 &t3>0 &t4>0).

3.3 算法求解示例

我们可以通过一个实例再进一步更加直观、清晰地认识这一算法,对于图8给定的非交互式Petri网和带验证性质φ(p1+p3<3),安全性约束C(P,T,F,M0)^¬φ为

p1,p2,p3,p4≥0

t1,t2,t3,t4,t5≥0

p1=0+t5

p2=1+t3+t4

p3=0+t3+t4+t5

p4=0+t1+t2+t3+t4–t5

p1+p3≥3

两种剪枝约束Constraint1(2)和Constraint2(3).

t2>0

将上述约束作为输入交给SMT求解器求解,有解,解ModelA1为

p1=0,p2=3,p3=3,p4=4

t1=0,t2=1,t3=0,t4=3,t5=0

所以X1=(0,1,0,3,0),构成的子网NX1如图6所示.

显然,该子网中只有p2,p4由M0可标记,因此需要增加新约束δnot(t1=0 &t2>0 &t3=0 &t4>0 &t5=0),剔除该子网进行下一次迭代,下一次迭代的约束即为

p1,p2,p3,p4≥0

t1,t2,t3,t4,t5≥0

p1=0+t5

p2=1+t3+t4

p3=0+t3+t4+t5

p4=0+t1+t2+t3+t4–t5

p1+p3≥3

t2>0

not(t1=0 &t2>0 &t3=0 &t4>0 &t5=0)

将新的约束文件作为输入交给SMT求解器求解,依然有解,解ModelA2为

p1=1

p2,p2,p3=3

t1,t2,t3,t4,t5=1

所以X2=(1,1,1,1,1),而由NX2构成的子网如图7所示.

4 实验及结果分析

由于现有的验证可覆盖性问题的工具都是针对传统 Petri网的,它们所使用到的标准测试集也都是传统Petri网,所以这些测试集对于CFPCV工具的测试不再适用.因此,针对非交互式Petri网,我们随机生成了3组非交互式Petri网的测试用例,它们的位置和迁移数规模分别是1～10、1～100、1～1000.我们主要从成功率、迭代次数、性能比这3个方面对CFPCV进行了评测.我们主要与Petrinizer、MIST这两个工具进行了比较,Petrinizer工具是通过提取约束并求解的方法来验证传统 Petri网的可覆盖性问题,与 CFPCV一样,它也是采用安全性方法来获得约束.不过,正如前文所述,安全性方法在理论上是不完备的,其只能验证那些覆盖的用例,对于不覆盖的用例则无能为力.但从文献[7]中的实验结果来看,Petrinizer在应对一些特定的测试集时仍然有不错的成功率.而 MIST工具是采用状态空间探索的方法,其内部集成了多种验证算法,包括从待验证状态反向探索状态空间的backward[14]算法,以及先对原Petri网模型进行抽象精化(abstraction refinement)来缩小模型规模,然后再结合前驱和反向探索状态空间来进行验证的 ic4pn[15]算法、tsi[15]算法和 eec[16]算法.尽管增加了抽象精化的过程来缩小模型的规模,但是对于随机模型这个过程的效果甚微,依然会有状态爆炸(state explosion)的问题存在.

4.1 成功率

我们将随机生成的3组测试用例作为输入交给CFPCV、Petrinizer、MIST工具求解,后两种工具都是验证传统Petri网可覆盖性的工具,所以它们肯定也可以验证非交互式Petri网的可覆盖性问题.我们分别比较了这3种工具在每组测试用例下的成功率,见表1～表3(注:Positive表示满足性质φ,Negative表示不满足,Timeout表示超时,Don’t know表示无法判定,Success rate表示成功率).

从3张表可以发现,Petrinizer工具的成功率最低,因为Petrinizer使用到的方法也是安全性方法,但因其针对传统Petri网,并没有子网可标记验证来保证候选解是正确解,所以该工具使用到的算法在理论上不完备,可能存在其无法判定的情况,所以对于随机生成的测试用例,有大量的测试用例其无法判定,因此成功率在 3种工具中最低,在第3组测试用例上只有4.6%的成功率.而MIST工具是基于Petri网可达状态空间的搜索,由于Petri网的可达状态空间可能很大,所以该工具经常发生超时情况,对于规模较大的输入,超时情况更加严重.所以,对于随机生成的测试用例,MIST工具超时最多,而且随着测试用例规模的扩大,其超时情况变得非常严重,成功率直接从100%下降到了46.9%.显然,CFPCV工具的成功率最为优异,对于3组测试用例成功率都在99%以上.

Table 1 Success rate of the 3 tools in test cases which scales of place and transition are between 1 to 10表1 测试用例位置迁移数规模1～10之间3种工具的成功率

Table 2 Success rate of the 3 tools in test cases which scales of place and transition are between 1 to 100表2 测试用例位置迁移数规模1～100之间3种工具的成功率

Table 3 Success rate of the 3 tools in test cases which scales of place and transition are between 1 to 1000表3 测试用例位置迁移数规模1～1000之间3种工具的成功率

4.2 迭代次数

因为 CFPCV 使用到的算法是基于迭代的,需要在每次迭代中验证候选解是否是正确解,如果不是,则需要增加约束继续迭代求解,所以算法的迭代次数直接决定了算法的运行效率.如果迭代次数过多,就可能发生超时的情况.我们记录了每组测试用例算法的迭代次数,见表4.

由表 4可以发现,对于绝大多数(2587+397)测试用例,只需要 1～2次迭代即可得解,只有极个别的测试用例需要10次以上的迭代(12次2个,16次1个,超时10个).因为只需要很少的迭代次数即可得解,所以CFPCV工具的运行效率理应很高.

Table 4 Iteration time of CFPCV表4 CFPCV运行迭代次数

4.3 性能比

因为CFPCV和Petrinizer都用到了安全性方法,且Petrinizer的性能也非常高,只不过其成功率较低,所以我们比较了3组测试用例下这两种工具的性能(未比较MIST是因为MIST超时情况严重,所以其性能自然较低),性能比如图9～图11所示,单位为s.

由图9～图11可知,Petrinizer和CFPCV性能相当,大部分测试用例两种工具在20s内得解.图中箭头标注的点分为两类,一类是CFPCV需要的较多的迭代才可得解,因此这些点代表的测试用例CFPCV运行较慢.另一类是两种工具都超时(图11右上角的8个点),原因是因为SMT求解器求解约束超时,这种情况是合理的,因为有些约束求解问题(比如SAT问题)就是NP完备问题,可能存在一些测试用例SMT求解器根本无法求解,因此两种工具都发生了超时的情况.因为Petrinizer没有验证候选解的迭代过程,所以Petrinizer的性能理应比CFPCV要好.但是由第 4.2节迭代次数的记录来看,对于绝大多数测试用例,CFPCV只需要一两次迭代即可得解,因此CFPCV的性能和Petrinizerx相差无几.考虑到第4.1节提到的CFPCV极高的成功率,这样的性能是非常令人欣慰的.

5 相关工作

Petri网的可覆盖性问题虽然已被证明是EXPSPACE完备问题[17,18],BPP的可达性以及可覆盖性问题也都被证明是NP完备问题[3],但是近年来学术界依然提出了很多解决该问题的算法,它们可以大致分为两类:第1类就是基于状态空间的探索.由Karp和Miller(简称KM)提出的Karp and Miller procedure[17]是第一个可以验证Petri网可覆盖性的完备算法,它的主要思想是从Petri网的初始状态前驱探索(forward exploration)状态空间,不断加入可以覆盖前一状态的新状态来构造 Petri网的覆盖树,然后判断待验证状态是否在该覆盖树上来进行验证.但是,由于 Petri网的可达状态可以无限制地增长,导致覆盖树的规模可能非常之大,所以这个构造过程通常比较低效,它具有非原始递归最坏情况的复杂度.这项技术已在 TINA-KM[19]工具上实现,可想而知,该工具在处理状态空间较大的模型时效率很低.另外,这项技术的一种优化方法就是构造 Petri网的最小覆盖集(minimal coverability sets)[20]而非覆盖树,最小覆盖集已被证明是存在且有限的[21],而且其规模要远小于覆盖树的规模,所以其构造效率有了较大的提升,这项技术已在 Pep[22]工具上实现.另外,还有反向探索(backward exploration)[23]状态空间的算法,就是从待验证状态反向探索状态空间,直到到达初始状态为止,这项技术已在工具 IST-BC和PETR-BC[24]上实现,不过,反向探索和前驱探索本质上没有太大的区别,所以算法效率并没有显著的提升.当然,还有将前驱探索和反向探索结合[25,26]的算法,分别从初始状态前驱探索状态空间和从待验证状态反向探索状态空间,直到两条探索路径触碰为止,这项技术已在工具BFC上实现,性能得到了较大的提升.文献[16]中提出的‘Expand, Enlarge and Check’方法通过并发地构造两个Petri网的近似序列来验证可覆盖性,第1个序列是系统的向下近似,它可以用来判定覆盖的实例,另外一个序列是系统的向上近似,用来判定那些不覆盖的实例.这项技术已在工具 MIST上实现.MIST内部集成了多种算法,不过,它们的思路大体一致,都是先对原模型进行一层抽象来缩小模型的规模,然后对抽象后的模型通过前驱探索和反向探索结合的方法来加以验证.另外一类是基于约束的方法.其主要思想与本文的算法类似,都是用约束条件来表达Petri网的性质,通过求解约束来验证可覆盖性.然而,由于约束的表达能力有限,不可能准确表述出 Petri网的可达状态空间,所以这些约束条件只能成为可覆盖性问题的必要条件而非充分条件.因此这类算法在理论上是不完备的,比如 Petrinizer[7]工具,它是通过安全性方法来提取约束并求解来进行验证,不过,由于安全性方法在理论上不完备,所以它只能验证那些不覆盖的测试用例,对于覆盖的测试用例则无法验证.

除此之外,并发程序的性质也可以通过基于 Petri网的模型检测技术来分析,使用 TCTL(时间计算树逻辑)[27]来描述待验证性质,通过检测 Petri网的迁移发生序列来验证模型是否满足这些性质.其具体思路是先构造包含待验证性质取反语义序列的Büchi自动机,然后再计算Petri网可达图和自动机的乘积图.若将乘积图看成一个有向图,则模型检测的问题等价于检测乘积图中是否包含一个从初始状态可达的最大强连通分量,且在该强连通分量中包含了一个接受状态.对于安全性一类的性质来说,等价于检测乘积图中是否存在一条从初始节点到接受节点的路径.对于活性一类的性质来说,等价于检测乘积图中是否存在由初始节点可达的包含接受节点的环.但是,基于 Petri网的模型检测技术也会受到状态爆炸问题的困扰,因为 Petri网模型的状态空间通常非常之大,甚至无界,所以 Petri网的模型检测问题难度非常之大,其上的很多逻辑算子都不存在多项式时间算法.比如EG/AF(即我们通常所说的活性)逻辑在Petri网和BPP上都是不可判定的,EF逻辑在Petri网同样不可判定,在BPP上虽然可判定,但也拥有PSPACE完备的复杂度[28].所以,传统的基于Petri网的模型检测技术在验证并发程序的性质时存在较大的局限性.

6 总结及未来的工作

本文设计并实现了可以高效验证非交互式Petri网可覆盖性的工具CFPCV,它在验证传统Petri网可覆盖性使用到的安全性方法的基础上,增加了只对非交互式Petri网适用的子网可标记验证,从而保证了其解的正确性,并且通过实验验证了该工具具有较高的成功率以及不错的性能.

由于业界缺乏针对非交互 Petri网可覆盖性验证的标准测试集,所以本文测试所使用测试集都是随机产生的.未来会使用数量更多以及质量更高的测试集进行测试,以验证 CFPCV的表现是否依然优秀.另外,其实除了本文所提的剪枝方法以外,还有一种叫作阱(trap)约束[29]的技巧可以进行加速,不过我们通过测试发现,阱约束的表现却不尽人意,可能和我们测试集的随机性有关.未来业界若有质量较高的测试集公开,我们会在算法上增加阱约束进行测试,如果性能得到提升,则将加以改进.

未来,我们也会在BPP上做模型检测,虽然第5节提到BPP上的模型检测问题难度很大,但是我们如果做有界模型检测,比如将某个性质在无限的转移序列上都要成立限定为在k(k为大于0的自然数)步转移内成立,同时也保证这样的性质具有一定的实际意义,那么问题的复杂度将大幅下降.同样通过提取约束,使用 SMT求解器求解约束的方法,BPP上的有界模型检测问题可能会有很高效的解决方案.