多值可能性模型检测器的设计与实现

0 引 言

模型检测[1-3]作为一种形式化验证工具，主要包含三个步骤：建立模型，描述系统性质，使用模型检测算法验证系统是否满足这些性质。系统模型通常使用布尔传递系统模型或者Kripke结构，系统性质则通过时序逻辑进行刻画，最终验证结果会给出一个布尔结果，满足性质给出是，不满足性质系统会给出否，并且给出反例。模型检测广泛应用于许多重要的系统，例如SPIN[4]，NuSMV[5]。

模型检测器受制于经典逻辑，有许多问题在经典逻辑上无法解决，例如现实生活当中的不确定性[6]。当处理这些信息的时候，传统的模型检测器便失去了作用。其中非经典多值逻辑提供了一种很好的解决方法来处理信息的不确定性和不完备性，例如文献[7]提出的用三值逻辑去解释模型检测的结果，文献[8]使用四值逻辑对门级电路的抽象模型进行推理验证。

文献[9]提出基于多值可能性测度的多值计算树逻辑的模型检测，解决了在系统中存在“是”和“否”之间状态的逻辑问题，其采用两种方式：第一，将系统中状态解释为多值的；第二，将系统中状态之间的转移关系也设置为多值的。

基于文献[10]，文中设计了自动化验证的多值模型检测器。首先，对构建的多值模型Kripke结构，从计算机存储的方面进行数据结构上的设计，并且分析了时间复杂度，尽量用最优化的结构对状态和转移函数进行存储，使模型检测器能够计算更多的状态；其次，设计了模型检测器的框架，从输入的模型以及性质，如何转换模型和性质，如何对性质进行计算，到完成模型检测后如何输出检测结果，并对时间复杂度进行了分析。

1 多值可能性测度下的模型检测

1.1 多值可能性Kripke结构

定义1[11]：设(l，≤)是偏序集，若l中任意两个元素都存在上确界以及下确界，则称(l，≤)是格，为了方便，这样的格称为偏序格。

定义2[12]：一个多值Kripke结构是一个五元组M=(S,P,I,AP,L)，其中:

S是一个可数、非空的状态集合；

P:S×S→l表示多值传递关系；

I:S→l是初始分布函数；

AP是原子命题的集合；

L:S×AP→l是一个标签函数。

注：多值传递函数P:S×S→l可以通过l格值表示，将这个矩阵表示为P。矩阵P传递闭包，表示为P+。矩阵P的自反和传递闭包用P*表示，P*=P0∨P+。Paths(M)表示M中所有路径的集合。

定义3[13]：一个多值Kripke结构M，其函数PoM:Paths(M)→l定义如下：

对任意π=s0s1…∈Paths(M)，有如下定义函数：

PoM:2Paths(M)→l

PoM称为在Ω=2Paths(M)上的广义可能性测度。

定义4[14]：对于一个多值Kripke结构M，定义一个函数rP:S→l，表示在M上从初始状态s出发的最大可能性路径：

rP(s)=∨{P(s,s1)∧P(s1,s2)∧…|s1,

s2,…∈S}

其中计算rP(s)的方法依据定理1。

定理1[15]：一个有限多值Kripke结构M，M中的一个状态s，有：

rP(s)=∨{P+(s,t)∧P+(t,t)|t∈S}

使用矩阵表示为：

rP(s)=P+∘D

其中，符号“∘”表示sup-inf合成运算。

1.2 基于多值可能性测度的多值计算树逻辑

引入一种新的定量时序逻辑对性质进行描述，即可能性测度上的多值计算树逻辑。

定义5[16](MvCTL语构)：多值CTL(简称MvCTL)关于原子命题AP的状态公式：

Φ::r|α|Φ1∧Φ2|Φ|Po(φ)

其中，α∈AP,r∈l，φ是MvCTL路径公式，如下：

φ::=OΦ|Φ1∪Φ2|Φ1∪≤nΦ2|□Φ

其中Φ,Φ1和Φ2是状态公式并且n∈N。

定义6(MvCTL语义)：多值Kriple结构M=(S,P,I,AP,L)，a∈AP是原子命题，s∈S表示状态，Φ,Ψ是MvCTL状态公式，φ是MvCTL路径公式。对公式Φ，其语义是格值模糊集‖Φ‖:S→l，对任意s∈S，r∈l，其定义如下：

‖r‖(s)=r

‖a‖(s)=L(s,a)

‖Φ∧Ψ‖(s)=‖Φ‖(s)∧‖Ψ‖(s)

‖Φ‖(s)=‖Φ‖(s)

‖Po(φ)‖(s)=Po(s|=φ)

对于路径公式φ，其语义是一个格值模糊集‖φ‖:Paths(M)→l，其定义如下：

‖OΦ‖(π)=‖Φ‖(π[1])

‖Φ∪Ψ‖(π)=∨j≥0∧k<j‖Φ‖(π[k])∧‖Ψ‖(π[j])‖;

Φ∪≤nΨ‖(π)=∨j≤n∧k<j‖Φ‖(π[k])∧ ‖Ψ‖(π[j]);

‖□

路径公式◇Φ(最终的)有如下语义：

‖◇

2 多值可能性模型检测算法

MvCTL模型检测的问题可以描述如下：

给一个有限广义的多值Kripke结构M，状态s和一个MvCTL状态公式Φ，计算‖Φ‖(s)的值。其计算采用递归的方法。

给出模型检测的算法[17]如下：

输入：GPKSM和MvCTL公式Φ

输出：s满足公式φ的可能性，即‖Φ‖(s)

1：Procedure MvCTLCheck(Φ)

2：CaseΦ

3：rreturn (r)s∈S

4：areturn (L(s,a))s∈S

5：Φreturn (‖Φ‖(s))s∈S

6：Φ1∧Φ2return (‖Φ1‖(s)∧‖Φ2‖(s))s∈S

7：Po(ΟΦ) returnP∘Dψ∘rp

9：Po(Φ1∪Φ2) return (DΦ∘P)*∘DΨ∘rp

10：Po(◇Φ) returnP*∘DΦ∘rp

11：Po(□Φ) return Fixpoint((1)s∈S,fΦ)

End Case

End Procedure

3 模型检测器的设计与实现

3.1 模型检测器的架构设计

模型检测的基本运行原理如图1所示，主要分为三个部分：系统建模、性质的形式化描述、模型检测算法。所以模型检测器的结构设计也主要依据这三个部分来进行。

图1 模型检测流程

模型检测器分为三层。第一层为模型构建层，主要完成对多值Kripke结构中的数据进行建模，用计算机中的数据结构进行存取；第二层为计算层，主要根据用户输入的性质进行计算；第三层为性质验证层，主要对计算出的结果进行验证，得出用户输入的性质是否满足系统的结果。模型检测器的系统架构如图2所示。

图2 模型检测器架构

3.2 格值转换器设计

与经典的模型检测器的输入不同时，由于采用了格值的建模方式，因此在验证之前，设计一个格值转换器，主要方式是将格值映射到[0,1]区间上，例如三值逻辑，则将[T,M,F]映射为[0,0.5,1]的三值状态进行计算。

3.3 模型构建层设计

需要保存Kripke结构的节点信息以及传递信息，使用数据结构中的图[18]结构。由于有向图中有两种存储方式，一种是邻接矩阵，一种是邻接表，其相关的时间复杂度分别为Ο(n2)和Ο(E+V)(E为边数，V为节点数)，所以采用时间复杂度更低的邻接表的方式进行存储。

根据用户输入的Kripke结构，分别将节点和边刻画为Node类和Edge类，其中Node保存了节点的状态信息，Edge类保存了传递信息。其实现为从用户的输入当中生成所有的节点，然后依次遍历每个节点信息，判断节点与节点之间是否有边，如有，则将边的信息添加到邻接表中，代码如下：

public void addEdge(Node v,Node w){

if(hasEdge(v,w)){

Return;//如有边，则返回

}

g.get(v.id).add(w);//g为list实例

}

3.4 计算层设计

这一层主要设计的问题是模型检测算法的输入和计算函数的定义。将模型检测算法封装在一个函数当中，接收用户输入的性质，然后进行判断，判断完成后，需要遍历之前存储的邻接表，拿出状态和传递的数据，最后调用计算函数进行计算，将输出的结果进行保存。判断函数的部分代码如下：

//返回每一性质计算所需要的公式类

publicFomule[] choiceFomule(String[] s){

//循环遍历用户的每一个输入

for(int i=0;i<s.length;i++){

String s=s[i];

//match函数用于找到匹配的公式

Fomule[i] fomule=match(s);

}

returnfomule; //返回公式类

}

匹配公式之后，根据模型检测算法进行计算，需要定义圈乘“∘”运算，交运算“∧”，并运算“∨”的计算函数，圈乘函数代码如下：

public double[n][n]calculateCircle(

double[n][n]a,double[n][n] b){

double[n][n] c=new double[n][n];

//遍历a矩阵的行，遍历b矩阵的列

for(int i=0;i<n;i++){

for(int j=0;j<i;j++){

if(a[i][j]<b[j][i]) //取小

c[i][j]=a[i][j];

c[i][j]=b[j][i];

}

}

return c;//返回计算结果

}

对于并运算函数和交运算函数，由于和圈乘运算类似，只是改变了取大和取小操作，这里省略了代码。由于采用了双层循环的遍历，可以看出每个函数的时间复杂度为Ο(n2)。

3.5 验证层设计

这部分主要完成函数逻辑的调用，并计算出结果。由于在计算层封装了各种算法公式，在验证层，需要拿出计算层给出的结果，加以判断之后，输出是或者否。将传入计算层封装的结果类ResultData，调用函数进行判断，返回一个boolean数组，最后遍历这个数组可得到计算结果。

4 模型检测器的验证

4.1 模型检测器时间测试实验

对设计出来的模型检测器做一个时间性能的测试。结果如表1所示，其中n表示状态的个数，true表示正确完成了计算，false表示计算失败，time表示运行时间。

表1 运行时间测试结果

模型检测器在状态数小于10 000的情况下，时间性能还不错，当大于100 000时，由于时间复杂度是指数级增长，时间性能上就差了一些。

4.2 恒温器性质验证实验

有一个三值恒温器模型，如图3所示。

接下来验证如下几个性质：

性质1：系统是否可以从任何状态转移到IDLE1状态；

性质2：当温度低于某个值时加热器是否可以启动；

性质3：在任何情况下系统是否可以关闭；

性质4：是否只有在空调关闭的状态下才能加热；

图3 恒温器模型

性质5：当温度高于某个温度时加热器能否启动。

将这些性质转化为MvCTL公式后，输入的结果如表2所示。

表2 性质验证结果

通过表2可以得到一些结论，比如系统可以从状态OFF转移到状态IDLE1的可能性为T,转移到IDLE2的可能性为M，转移到AC状态的可能性为T。

5 结束语

根据基于多值可能性测度的多值可能性计算树逻辑的模型检测理论，设计能够自动化验证的多值模型检测器MvChecker。根据模型检测流程，设计了三层模型检测器的框架，对每一层架构进行了详细设计，并使用Java语言进行了实现，用户可以自己构建系统和需要验证的性质，输入MvChecker进行系统的验证。