基于切片技术的复杂模型验证方法

纪明宇 于明霞 么一诺 毕曦文

(东北林业大学信息与计算机工程学院 黑龙江 哈尔滨 150040)

0 引 言

随着科技发展的日新月异，计算机软硬件系统趋于复杂化和抽象化使得其优劣性质验证成为极为重要的内容。模型检测作为一种能够自动验证并提出反例路径的形式化验证技术，已被广泛应用于系统验证。其基本思想是利用模型描述语言对已有系统进行建模，之后对该模型进行既定性质验证，若满足性质则进行下一项验证，否则提出反例路径。常用的形式化方法主要有线性时序逻辑(LTL)和计算树逻辑(CTL)等[1]。典型的模型检测工具有NuSMV[2]、SPIN[3]等。互模拟的引入使得LTL模型检测能够在验证混合自动机时具有可判定性[4]。广义CTL逻辑的讨论能够引发对模型检测的更广泛应用的思考[5]。目前在模型检测领域，验证技术已越来越成熟，其使用的手段如基于时序逻辑的规范化语言、自动机和不动点逻辑已为模型检测领域的发展作出极大贡献[6]。

状态空间爆炸问题始终是模型检测技术中需要解决的一大难点。在建立模型时所需考虑的状态数量往往呈指数增长，最终难以控制模型的大小以致增大系统验证的复杂度，解决该问题的思想包括状态空间压缩[7-8]、存储空间压缩的Hash Compact方法[9]、并行和分布式计算[10]、随机化和启发式搜索算法[11]等。近年来逐渐得到发展的限界模型检测和切片技术等多种约减方法能够在一定程度上解决有限马尔可夫链的状态爆炸问题。如：基于线性方程组求解的限界模型检测算法在反例较短的情况下能够快速完成检测过程并避免空间爆炸[12]；基于懒惰切片提出的状态空间搜索方法，在截断状态基础上进行多次细化迭代，有效避免基于CEGAR的切片方法导致的重复计算[13]；基于状态约减的信息攻防图生成算法在实现目标网络中主机覆盖的基础上描述了控制状态空间组合爆炸问题的过程[14]；冗余路径的点约减方法探究了有效简化和优化USV在线路径的相关问题[15]等。

然而，上述性质验证和约减方法很少涉及对带资源消耗的复杂迁移系统进行性质验证。本文将在已有研究工作的基础上，结合改进的图的深度遍历算法和概率矩阵的迭代运算，提出针对复杂模型的性质检验方法。首先利用栈的概念对系统进行初始的步数约束检验，对系统完成约减以避免冗余状态和迁移的影响，再计算得出约减后的状态间概率和资源消耗反例路径，从而完成满足带资源消耗约束的直到性质验证过程。

1 背 景

迁移系统在复杂系统的模型性质验证领域，常用来作为模型来描述系统行为。

定义1迁移系统(TS)。迁移系统是基本的有向图，其中点表示状态，边模仿迁移，即状态变化。状态描述了某个确定时间的系统行为的信息。迁移系统TS可以表示为元组T=(S,Act,→,AP,L),其中：S是状态集合；Act是动作集合；→是迁移关系；AP是原子命题集合；标签函数为L:S→2AP。

如果S、Act、AP有限，那么TS被称为有限的迁移系统。由于基本的迁移系统模型在随机性和确定性的表达能力上存在不足，所以出现了连续型和离散型的不同马尔可夫模型用以描述待验证的复杂随机系统[16]。两种模型分别具备描述在离散时间和连续任意时间的状态迁移的能力,本文针对具有离散时间特征的系统模型展开研究。

例1DTMC举例。

图1为包含9个状态的双骰子投掷模型对应的不带资源消耗的离散时间马尔可夫模型。该模型描述了以下情形：投掷结果骰子数字和为7或11时为获胜，系统迁移到达won状态，骰子数字和在{2,3,12}中时到达last状态，骰子数字和为其他结果时则记为“points”，并继续投掷直到和为7时达到last状态或和为“points”时达到won状态。图1模型忽略了各状态所满足的原子命题。

图1 DTMC举例

本文以DTMC为基础,针对带迁移资源消耗的离散时间马尔可夫回报模型(DTMRC)展开研究。

定义3离散时间马尔可夫回报模型(DTMRC)。DTMRC为五元组M=(S,P,L,AP,N,v)，其中：S、P、L、AP、v在定义2中已有说明；N:S×S→R≥0为迁移回报矩阵结构(R为迁移回报集合)，描述了从初始到各状态的迁移资源；Ps1,n,s2=0.6表示从S1迁移到S2，发生迁移时所消耗的资源为n的概率为0.6。

例2DTMRC举例。

图2为带有资源消耗的马尔可夫模型,其包含8个状态以及12个迁移过程。S0为初始状态，包含原子命题{a,c}。对于状态S0来说，在满足原子命题a和c的条件下，下一步可迁移状态集为{S1,S2,U}，发生迁移的概率分别为0.5、0.3和0.2，消耗的资源分别为10、10和15。

图2 DTMRC举例

DTMC模型一般可通过概率计算树逻辑(PCTL)来描述验证的性质。

定义4概率计算树逻辑(PCTL)。基于原子命题集合AP的PCTL状态公式根据以下语法被形式化：φ::=true|a|φ1∧φ2|PJ(φ)。其中：a∈AP，φ是路径公式；J⊆[0,1]是有理数界的中间值；PJ(φ)表示当前状态满足公式φ的概率值为J。

PCTL路径公式可以根据以下语法被形式化：φ::=Oφ|φ1∪φ2|φ1∪≤nφ2，其中φ、φ1、φ2是状态公式，Oφ表示最终进入满足状态公式φ，n∈N。

由于PCTL模型检测的语法并不能描述迁移系统中资源消耗情况，所以对于DTMRC模型的性质，一些学者提出了改进的概率回报计算树逻辑PRCTL[17]，它与PCTL的区别在于路径公式的语义表达方式有所不同。

PRCTL的路径公式表示为：

式中：n=[n1,n2]⊆R≥0和r=[r1,r2]⊆R≥0分别代表迁移步数和迁移资源消耗约束，U代表直到算子。

2 验证过程

对于待验证步数约束条件的DTMRC模型，可以将其看作带有冗余的状态和迁移的复杂系统。(1) 利用改进的图的深度遍历算法，得出符合步数的路径集。针对进行模型检测时反复出现的状态爆炸问题，通过基于切片技术的约减方法来进行系统的缩减。首先将超过步数约束的迁移完全省去，实现一次约减；再检查剩余的状态是否包含在满足直到条件的路径中，若不包含则将这样的状态同时省去，实现二次约减，得到一个较为简单的迁移系统。(2) 对于新的迁移系统构造各状态间的迁移概率矩阵，进而通过概率迭代运算，计算出n步内a∪e的概率和。

定义5迁移系统概率矩阵迭代计算公式为：

X(i+1)=AX(i)+b0≤i≤n

X(0)=0i=0

式中：A表示为迁移系统的各状态间初始概率矩阵；b表示为系统状态到结束状态的一步可达概率矩阵；X(i)表示为第i步的迭代后的概率矩阵。

例3n步可达概率计算举例。

以图1中的DTMRC模型为例，计算从状态start到状态won的n步内可达概率：

首先得出初始概率矩阵：

系统状态到结束状态won的一步可达概率矩阵：

然后对一步可达矩阵进行迭代，求解出两步可达矩阵为：

三步可达矩阵为：

最后，基于资源消耗反例路径的思想，根据每个迁移上所带的资源数量，对已满足概率条件和步数条件的迁移路径，通过遍历计算出各路径的资源消耗以寻找反例集。若某路径集的资源消耗和超过约束值，表示其为一个反例。

3 算法描述

本节对上节涉及的2个算法进行详细说明：

算法1基于图的路径寻找算法getPaths

输入：DTMRC模型M和步数约束m， 当前的起始节点cNode，当前起始节点的上一节点pNode，最初的起始节点sNode，中间节点需要满足的原子命题a，最终节点需要满足的原子命题e。

输出：DTMRC模型M中所有满足步数约束的路径集。

getPaths(M,m,cNode,pNode,sNode,a,e){

1 nNode<-null;

2 n<-stack length;

/*找到路径上的节点数*/

3 sNode╞a;

4 if(cNode !=null and pNode !=null and cNode==pNode)

/*出现环路*/

5 return false;

6 if(cNode !=null){

7 i<-0;

/*起始节点入栈*/

8 if(cNode╞e)

9 {if(n<=m+1)

10 showAndSavePath;

/*满足步数的路径转储并打印输出*/ }

11 else{If(cNode╞a){

12 nNode<-cNode.getRelationNodes

/*从与cNode有连接关系的节点集中得到一个节点作为

下一次递归寻路时的起始节点*/

13 while(nNode !=null and nNode╞a){

14 if(pNode !=null and (nNode==sNode or nNode==pNode or isNodeInStack))

/*产生环路，重新寻找与cNode有连接关系的节点*/

15 {i++;

16 if(i>=cNode.getRelationNodes size)

17 nNode<-null;

18 else nNode<-cNode.getRelationNodes of i;

19 continue; }

20 if(getPaths(M,m,nNode,cNode,sNode,a,e))

/*递归调用*/

21 stack.pop();

/*找到路径弹出栈顶节点*/

22 i++;

23 if(i>=cNode.getRelationNodes size)

24 nNode<-null;

25 else nNode<-cNode.getRelationNodes of I;

}}

26 stack pop;

27 return false; }}}

/*以cNode为起始节点到终点的路径已经全部找到*/

28 else return false;}

/*算法结束*/

算法2面向资源消耗的反例路径寻找算法getCE

输入：PR[n]为存储满足步数约束和概率约束的路径及其消耗资源数的结构体数组，R为资源消耗限制数。结构体为：

structlujing{

String P;

//把路径上的状态节点看成字符串

int r;}

//路径消耗的资源数

输出：反例路径集及其消耗的资源和。

getCE(PR[n],R){

1 unsigned int sta=1;

2 inti,i1,i2,j,m=0,A[1000]={-1};

3 for(j=1;j<=(int)pow(2,n+1)-1;j++)

4 {for(i=0;i

5 {if((j&sta)!=0)

/*一条路径与一个二进制位相对应，二进制位不为0对应

的路径存在*/

6 {m=m+PR[i].r;

7 A[i1]=i;

/*记录路径在结构体数组的位置*/

8 i1++;}

9 sta=sta<<1;

/*sta对应的二进制加一*/}

10 if(m>=R)

11 {i1=0;

12 while(i1

13 {if(A[i1]!=-1)

14 {i2=A[i1];

15 printf(“%s”,PR[i2].P);}

16 i1++;}

17 printf(“%d”,m);}

18 m=0;i1=0;

19 A[1000]={-1};

20 sta=1;}

21 return 0;}

/*算法结束*/

算法1的时间复杂度主要与待验证公式中的步数约束m有关，而算法2的时间复杂度主要与PR[n]结构体数组的大小有关。算法1为算法2提供了满足步数约束的反例集。

4 实例分析

首先利用算法1进行步数条件的检验。得出满足步数约束的路径集{S0S2T1T4,S0S2T2T4,S0S1T1T4}。一步、两步和三步遍历过程如图3、图4和图5所示。然后进行冗余状态和迁移的二次约减，图6为满足步数约束的迁移图，图7为完成三步约减后的迁移系统。

图3 一步遍历过程

图4 二步遍历过程

图6 满足约束的迁移图

图7 三步约减后的迁移系统

针对新的迁移系统进行矩阵运算，求出从状态S0到T4的3步之内可达且满足a∪e的路径概率。经计算可得S0到T4的3步可达概率为0.113，由此可知路径集满足概率小于等于0.2的条件。最后，利用算法2对图7所示新的迁移系统进行资源消耗路径集求解，把符合步数条件和概率条件的路径集{S0S2T1T4,S0S2T2T4,S0S1T1T4}输入，求得所消耗的路径资源和为145。此时不满足小于等于140的资源约束条件，则该路径集为一个反例集合。

本文采用实验对相应的方法进行了有效性验证，实验硬件环境为Intel(R) Core(TM) i5-7200U CPU @ 2.50 GHz 2.70 GHz，内存为8 GB。软件环境包括操作系统为64位的Windows 7，编程软件用MyEclipse 10.7。本文提出的方法可一定程度用于随机分布式算法、安全协议分析等多个领域，用于以数学分析的角度进行可达性分析验证。

5 结 语

本文对带迁移资源消耗的复杂概率模型分步进行了可达性检验、概率检验和资源消耗检验，最终证明了基于带资源消耗的复杂概率迁移系统的性质验证方法的合理性和有效性。分析表明其能够在一定程度上缓解状态和迁移冗余的问题。未来的主要工作是面向更为庞大的迁移系统和更为复杂的性质检验，在状态缩减和路径压缩等方法上展开进一步的研究。