DOI:10.11990/jheu.201509006
, , , , , , , , 模型检测[1]是一种验证有限状态并发系统(模型)是否满足给定规约的方法[1-2]。当验证的模型不满足给定规约时给出反例是模型检测的一个显著特点。反例是证明模型违反给定规约的执行轨迹。调试者可以通过分析反例，理解错误产生的原因，对系统或模型进行修正。然而反例并没有明确指出模型错误的原因，需要调试者根据自己的经验定位错误，这需要花费大量的时间才有可能找到真正的错误，因此使用自动化的方法从反例中获取有用的信息，帮助用户定位错误，是目前的研究热点。许多研究人员致力于研究错误定位的算法，提出了许多经典的算法，如基于路径的语法级最弱前置条件的辅助算法[3]，利用克雷格插值的证明方法[4]，基于因果关系模型的方法[2, 5]，基于可满足性的方法[6-7]，以及基于证例和反例差异的方法[8-11]。本文的方法也是基于证反例的差异，证例是模型的一种迁移路径，并且满足待验证规约。为了获得与反例最接近的证例，本文提出了一种利用遗传算法获取证例的方法。遗传算法 (genetic algorithm,GA)是1975年由John Holland[12]教授提出，在许多研究领域都得以应用，例如自动控制、数据挖掘[13]、机器学习、组合优化[14]等。在软件方面主要用于测试用例的自动生成和优化选择，它从代表问题可能潜在解集的一个种群开始，通过选择、交叉和变异等操作，使种群逐渐集中于搜索空间中越来越好的区域。演化的代数主要取决于代表问题解的收敛状态，末代种群中的最佳个体作为问题的最优近似解。因此本文构建一种基于遗传算法的，具有普适性的求解最近证例的方法。该方法用Kripke结构来刻画系统行为，用线性时态逻辑LTL描述需要验证的规约，针对模型检测中模型的特点初始证例种群，使用两个适应函数对应的最佳个体进行交叉操作，具有指向性的变异操作，最终获得末代种群中的最佳个体，即最近证例。相对于其他的获取证例的方法，本文在证例搜索的过程中引入启发式信息，提高系统状态空间搜索的效率，并且由于遗传算法不依赖于具体问题而直接进行搜索，所以本文的方法适用性更强，应用范围更广。
1 模型检测与GA的基本理论 1.1 模型检测相关定义模型检测中通常使用状态迁移图来描述系统模型，Kripke结构是一种常用的状态迁移图。本文的待验证模型以Kripke结构表示，首先给出Kripke结构的定义。
令V={v1,v2,…,vn}是一个有限布尔变量集，Dv1,Dv2,…,Dvn分别为v1,v2,…,vn的数据域，定义在V上的Kripke结构为：
定义1 Kripke结构是一个四元组K=(S,I,T,L)其中：S⊆Dv1,Dv2,…,Dvn是有限状态集合，I⊆S是初始状态集，T⊆S×S是状态迁移关系，标记函数L:S→2v标记在状态S真变量的集合。
定义2 定义在Kripke结构K上的路径π是一个状态序列π=s0,s1,s2…，其中s0∈I，si∈S ,i∈N,π(i)=si;πi=si,si+1,si+2…。Path(K)表示K中所有路径的集合。
定义3 线性时态逻辑LTL在每一个时刻，只有一个可能的次态，LTL公式的语法定义如下：
$\phi $ ::= ⊥| ┬ | p | ($\neg $ $\phi $) | ($\phi $∧ $\phi $) | ($\phi $∨ $\phi $) | ($\phi $→ $\phi $) | (X$\phi $) | (F$\phi $) |(G$\phi $) | ($\phi $U$\phi $) | ($\phi $W$\phi $) | ($\phi $R$\phi $)
其中p是取自某原子集的任意命题原子。X、F、G、U、W和R为时态连接词。分别表示为“下一个状态”(neXt)，“某未来状态”(Future)，“所有未来状态”(Globally)，“直到”(Until)，“弱-直到”(Weak-until)和“释放”(Release)。
定义4 设M为Kripke结构模型，π=(s0,s1,s2…)是M中的一条路径，π是否满足一个LTL公式，由满足关系=定义如下：
1) π|=p⇔p∈L(s0)
2) π|=$\neg $φ⇔π|≠φ
3) π|=φ1∧φ2⇔π|=φ1且π|=φ2
4) π|=φ1∨φ2⇔π|=φ1或π|=φ2
5) π|=φ1→φ2⇔只要π|=φ1就有π|=φ2
6) π|=Xφ⇔π2|=φ
7) π|=Gφ ⇔ ∀i≥1,πi|=φ
8) π|=Fφ ⇔ ∃i≥1,πi|=φ
9) π|=φUφ ⇔ ∃i≥1,使得πi|=φ并且∀j=1,2,…,i-1，有πj|=φ
10) π|=φWφ ⇔ ∃i≥1，使得πi|=φ并且∀j=1,2,…,i-1，有πj|=φ或者∀k≥1 ，有πk|=φ
11) π|=φRφ⇔或者∃i≥0，使得πi|=φ，并且∀j=1,2,…,i，有πj|=φ；或者∀k≥1，有πk|=φ
Biere等提出的有界模型检测(bounded model checking,BMC)不同于传统的符号模型检测[15]，它在有限长度k(称其为限界)的范围内查找反例。如果在限界k内没有发现反例，则增加k的值直至问题变得难解，或者达到预先设定的上界。
根据LTL语义，BMC问题可以规约为命题可满足问题，若M为Kripke结构的待验证模型，f为BMC要验证规约的否定形式的公式，k为界限，第i个和第i+1个周期的状态为Si和Si+1，状态转换关系为Ti(Si,Si+1)，则BMC转换公式可以表示为：[[M,f]]k。
定义5 (BMC转换公式) 设M为Kripke结构，f为待验证的LTL规约说明否定形式的NNF公式，k为整数，则BMC转换公式为
| ${{\left[ \left[ M,f \right] \right]}_{k}}={{\left[ \left[ M \right] \right]}_{k}}\wedge {{\left[ \left[ f \right] \right]}_{k}}$ | (1) |
式中： [[M]]k=I(s0)∧∧i=0k-1T(si,si+1),[[f]]k=($\neg $Lk∨[[f]]k0)∨∨l=0k(lLk∧l[[f]]k0),lLk=T(sk,sl),Lk=∨l=0lkLk。[[f]]k0和l[[f]]k0的递归定义如表 1所示。
在有界模型检测方法中，将式(1)转换为CNF格式的SAT问题，并用SAT求解器求解，即可验证模型是否满足给定规约。在界限k内，反例的长度为k，基于界限模型检测的路径和反例定义如下：
定义6 反例 在Kripke结构K上，对LTL公式f和界限k，若有π|=k$\neg $f，则称π为f的反例。
定义7 证例 在Kripke结构K上，对LTL公式f和界限k，若有π|=kf，且π∈Path(K)，则称π为f的证例。
1.2 反事实依赖D.Lewis[16]提出的基于反事实的原因定义为通过搜索与反例最近证例定位错误的方法提供了逻辑基础。Lewis认为不同源自于“cause”，如果原因c不发生则所产生的影响e也不会发生，并将原因的定义建立在反事实依赖的基础之上。其中反事实依赖的定义为：
定义8 反事实依赖 设在世界w中有命题e和c，则反事实c↦e为真，当且仅当
1) 世界w中，命题e和c同时为真；(即：$\neg $c(w)∧$\neg $e(w))；
2) 存在世界w’，有$\neg $c(w′)∧$\neg $e(w′)∧(∀w″($\neg $c(w″)∧e(w″))(d(w,w′) ＜d(t,w″)))，其中d为距离度量。
定义9 (原因) 设在世界w中，命题c和e同时为真。则在w中c是e的原因，当且仅当在世界w′中，$\neg $c↦$\neg $e。
定理1 设f是待验证规约，t是反例，w是离t最近的证例，c是t中与w中取值不同的变量的集合，则c是$\neg $f的原因。
证明：根据假设有，在w中有$\neg $c(w)∧f(w)。假设存在某条与w不同的路径w′，有$\neg $c(w′)∧f(w′)，并且d(t,w′)≤d(t,w)。则w′中存在一些其他的与w不同的变量v∉D，那么这些变量v在t中的取值必然与w′中的不同。于是d(t,w′)>d(t,w)，矛盾，因此w′不存在。在t中有c↦$\neg $f，c是$\neg $f的原因。
1.3 遗传算法遗传算法(GA)是模仿自然界生物遗传进化过程中的“物竞天择、适者生存”的思想，是一种全局寻优搜索算法，它首先对问题的可行解进行编码，组成染色体，然后通过模拟自然界的进化过程，对初始种群中的染色体进行选择、交叉和变异，通过一代代进化来找出最优适应值的染色体来解决问题。遗传算法具有很强的全局搜索能力和较强的自适应性，适合解决连续变量函数优化问题和离散变量的优化组合问题。
遗传算法计算简单，具有超高的全局搜索能力[17]。在模型检测中，模型以Kripke结构给出并具有初始状态，在设计遗传算法的初始种群时，每个个体的第一个基因片段必须是模型的初始状态，因此初始种群的个体数相对较小，算法比较容易达到收敛状态。
定义8给出了最近证例需要满足的条件，不仅需要满足待验证规约还应该与反例的距离最近，给遗传算法应用于反例理解提供了适当的适应度函数。因此遗传算法适用于模型检测的中的证例搜索。
| f | [[f]]0k | l[[f]]k0 |
| p | pi | pi |
| $\neg $p | $\neg $pi | $\neg $pi |
| $\phi $∧φ | [[$\phi $]]ki∧[[φ]]ki | l[[$\phi $]]ki∧l[[φ]]ki |
| $\phi $∨φ | [[$\phi $]]ki∨[[φ]]ki | l[[$\phi $]]ki∨l[[φ]]ki |
| X$\phi $ | [[$\phi $]]ki,if i ＜k ⊥, 其他 | l[[$\phi $]]i+1k,if i ＜k l[[$\phi $]]kl, 其他 |
| G$\phi $ | ⊥ | ∧kj=min(i,l)l[[$\phi $]]kj |
| F$\phi $ | ∨kj=i[[$\phi $]]kj | ∨kj=min(i,l)l[[$\phi $]]kj |
| $\phi $Uφ | ∨kj=i([[φ]]kj∧ ∧j-1n=i[[$\phi $]]kj) | ∨kj=i(l[[φ]]kj∧∧j-1n=il[[$\phi $]]kn)∨ ∨i-1j=l(l[[φ]]kj∧∧kn=il[[$\phi $]]kn∧ ∧j-1n=ll[[$\phi $]]kn) |
| $\phi $Rφ | ∨kj=i([[$\phi $]]kj∧ ∧jn=i[[φ]]kj) | ∧kmin(i,l)l[[φ]]kj∨ ∨kj=i(l[[$\phi $]]kj∧∧jn=il[[φ]]kn)∨ ∨i-1j=l(l[[$\phi $]]kj∧∧kn=il[[φ]]kn∧∧jn=ll[[φ]]kn) |
本节讨论利用遗传算法来生成与反例最近的证例的算法。反例是当模型不满足待验证规约时生成的一条状态的序列。证例同样是模型中的一条状态迁移路径，但是它不违反待验证规约。最近证例就是离反例最近的证例。本文利用遗传算法，将最近距离和对于待验证规约的可满足度作为检测最近证例的适应度，而最终求得最近证例，帮助自动的定位错位。
2.1 编码遗传算法中首要问题就是编码问题，也是设计遗传算法时的一个关键步骤。常见的编码方法有字符串表示法和邻接基因位编码法。本文采用的是字符串编码方法。按照路径上状态的顺序进行编码，具体实现方式是：按照路径上状态的出现顺序，以及标签变量的值进行编码。以图 1的Kripke结构为例，有限长度路径π=(s0,s1,s2)，L(s0)={p,q}，L(s1)={q,r}和L(s2)={r}。若状态s0编码为110，s1编码为011，s2为001。则路径π的编码为110011001。
|
| 图1 一个简单的Kripke结构 Figure 1 A simple Kripke structure |
在遗传算法的初始种群中，如果每个个体都具备一定的精度且个体间多样性较强时，则可以提高算法搜索效率，加速算法收敛。在模型检测中，模型被表示成一个Kripke结构，而所求的证例具有特定起始点，也就是从初始状态集的某一个起始状态出发的系统运行路径。因此与随机生成初始群体的方法不同,本文生成初始种群的方法是基于特定起始点的，试图能够快速产生具有一定精度和较强多样性的初始种群。如定义2所示，系统的运行路径是一个状态的无限序列：
π=s0,s1,s2…
本文中模型的验证使用的是有界模型检测，反例的长度为k，需要考虑路径上是否存在循环。路径可以表示为
π=uvω
式中：u和v是有限长度的状态序列，u=s0,s1……,si-1，v=si,si+1……,sk,i ＜k,ω≥1。如果状态序列u和v的长度分别记为i和j，则i+j=k。
给定长度k(k≥1)，考察从初始状态集I单步可达的所有状态的集合S1。依次考察S1中的每一个状态s1，若从s1出发，不存在迁移，则这一状态为死锁状态；若存在不止一条的迁移，则随机选取一条迁移执行，获得路径中的下一个状态。重复以上过程，直至得到第k个状态。
如果考察的模型含有n(n∈N+)个初始状态，从每个初始状态出发的迁移数分别是：x0,x1……,xn，则初始种群的大小为：x0+x1+……+xn。
2.3 适应度为了体现染色体的适应能力，引入了对问题中的每一个染色体都能进行度量的函数，叫适应度函数。通过适应度函数来决定染色体的优、劣程度，它体现了自然进化中的优胜劣汰原则，它是评价新解优劣的唯一标准。
一般而言，适应度函数是直接由目标函数变换而成的，有时也要根据问题的要求，对目标函数进行一定的适应度尺度变换。模型检测中的证例，需要是模型中的路径，并且要满足待验证规约。与此同时要求解与反例最近的证例，证例w与反例t的距离d(w,t)越短越好，因此需要将种群中的个体对于待验证规约的满足度s和d(w,t)共同作为遗传算法的适应度函数。
本文基于有界模型检测，按照定义5和表 1可以得到待验证规约的CNF形式的公式[[f]]k，满足度s即基于式子[[f]]k。例如布尔公式：
| $\begin{align} & \left( {{x}_{1}}\vee {{x}_{3}}\vee \neg {{x}_{4}}\vee \neg {{x}_{7}} \right)\wedge \left( {{x}_{2}}\vee {{x}_{5}}\vee {{x}_{6}}\vee {{x}_{9}} \right)\wedge \\ & \left( \neg {{x}_{2}}\vee {{x}_{5}}\vee \neg {{x}_{6}}\vee {{x}_{8}} \right)\wedge \left( \neg {{x}_{2}}\vee \neg {{x}_{4}}\vee \neg {{x}_{6}}\vee \neg {{x}_{9}} \right)\wedge \\ & \left( {{x}_{1}}\vee {{x}_{3}}\vee \neg {{x}_{5}}\vee \neg {{x}_{6}} \right)\wedge \left( {{x}_{3}}\vee {{x}_{4}}\vee {{x}_{5}}\vee {{x}_{8}} \right)\wedge \\ & \left( {{x}_{2}}\vee {{x}_{6}}\vee \neg {{x}_{8}}\vee \neg {{x}_{9}} \right)\wedge \left( {{x}_{3}}\vee \neg {{x}_{6}}\vee {{x}_{7}}\vee \neg {{x}_{9}} \right)\wedge \\ & \left( \neg {{x}_{4}}\vee {{x}_{7}}\vee {{x}_{8}}\vee \neg {{x}_{9}} \right) \\ \end{align}$ | (2) |
如图 1的路径π=s0,s1,s2={x1=1,x2=1,x3=0,x4=0,x5=1,x6=1,x7=0,x8=0,x9=1}满足布尔公式(2)中的8个子句，不满足子句x3∨$\neg $x6∨x7∨$\neg $x9，因此s=8。
本文中的个体编码采用的是字符串编码方式，因此d(w,t)采用字符串的编辑距离来度量[18]，值得注意的是路径上的每个状态记为一个字符。由于反例中也包含了许多值得遗传给后代的有益信息，在生成初始种群时并没有将反例排除在外，并且一般情况下适应度越高越好，因此在本算法中使用d(w,t)+1的倒数，可使求倒数不出现错误。
定义10 对于给定的规模为n的群体P={π1,π2,…,πn}，t为反例，个体πi∈P(i=1,2,…,n)的适应值为F(πi)，适应度函数为一维二元向量:
| $F({{\pi }_{i}})=\{s,\frac{1}{d{{\pi }_{i}},t+1}\}$ | (3) |
式中：s是个体对待验证规约f的满足度，dπi,t是个体πi与t的字符串编辑距离。
2.4 遗传操作简单遗传算法的遗传操作主要有三种:选择(selection)、杂交(crossover)和变异(mutation)。改进的遗传算法大量扩充了遗传操作，以达到更高的效率。
2.4.1 具有多评价指标的选择操作遗传算法中的选择操作就是用来确定如何从父代种群中按某种方法选取哪些个体遗传到下一代种群中的一种遗传运算。选择操作建立在对个体的适应度进行评价的基础上。使用选择算子(也叫复制算子reproduction operator)来对种群中的个体进行优胜劣汰操作：适应度较高的个体被遗传到下一代的概率较大；适应度较低的个体被遗传到下一代的概率较小。
本文同时用了两个评价种群优劣的指标，如定义10所示。因此本文的选择操作与其他的选择方式不同，需要考虑两个评价指标：s和
含多评价指标的选择操作的具体过程是：分别选择个体中s最优和
在选择算子的作用下，得到了新一代的个体，但是这些个体都是从上一代存活下来的，本质上还是上一代的个体，因此这些个体之间必须经过相互之间的交叉以产生新的个体，通过相互交换优秀的基因，使得整个种群向更优的方向进化。遗传算法中的交叉算子对算法进行全局搜索方面起到了重要的作用。本文采用的是一种通用的算子：“常规交叉法”。该交叉算子的使用非常的直观和简单。
首先是选择两个父代进行交叉，选择的方式是根据个体的适应度来决定的。然后产生一个区间[1，N]的随机数k作为交叉位。基于本文的编码，在选择交叉位时将一个状态作为一个完整的基因片段。也就是说，如图 2所示N=3，当选定的随机数k=2时交换的位置实际是个体编码的位置6(变异和修正的位置计算与此相同)。最后就是产生子代1和子代2，子代1交叉位之前的基因来自父代1交叉位之前的基因，而交叉位之后的基因则从父代2中按顺序选取那些没有出现过的基因，以补充完整整个解。子代2也是进行相似的处理。图 3给出了这种交叉法的一个例子。
|
| 图2 交叉操作 Figure 2 Crossover operation |
在完成交叉操作之后，常规的交叉方法容易产生非法的解，因此要对解进行修正。如图 2中子代1存在两个011(图 1中的s1)状态，为了最大的保持父代和新产生的基因片段，在原父代中删除交换来的基因片段中含有的状态，最终去除了重复状态的父代基因加上交叉来的基因完成了基因的修复。这样做既保留了父代基因也添加了交叉来的基因，对原基因和新基因进行了保持。例如图 2交叉后的子代1，进行的子代修正操作如图 3所示。
|
| 图3 子代基因修正 Figure 3 Gene correction |
从遗传算法的观点来看，解的进化主要靠选择机制和交叉策略来完成，变异只是为选择、交叉过程中可能丢失的某些遗传基因进行修复和补充，变异在遗传算法的全局意义上只是一个背景操作。变异操作产生新的搜索点，扩大搜索空间，避免算法过早收敛到局部最优解，起着提高种群多样性和搜索算子的双重作用。
在使用遗传算法进行证例发现时，交叉操作导致新一代种群生成许多无效的路径。鉴于此，本文提出了具有修正功能的定向变异策略。
例如图 3基因修正后的子代1:110001011，相应的模型是图 1，很明显子代1是一条无效的路径，π=s0,s2,s1∉Path(K)。定向变异策略对基因片段011进行修正，从s2单步可达的状态集s2中随机选择一个状态进行定向的变异，如选择s2则π=s0,s2,s2∈Path(K)，子代1的基因编码为110001001。
具体的定向变异策略具体过程如下：
1) 对每个个体，考察其是否属于Path(K)。
2) 如果存在不属于Path(K)，找到所有的错误迁移的起始状态，并计算其单步可达状态集合。从中随机选择一个状态作为变异后的状态。
3) 如果所有个体都属于Path(K)，则随机选择某个个体的某个基因片段si，如果i=0，从I∩pre∃({s1})(其中pre∃({s1})返回仅1次就迁移进状态集合s1的状态[18])中随机选择一个状态作为变异后的状态；如果0 ＜i≤k计算状态si-1单步可达状态集合，并从中随机选择一个状态作为变异后的si状态。
2.5 算法描述输入：K，f，T /* K表示Kripke结构的模型，f为待验证规约，T为算法的最大迭代次数*/
输出：w，F(w) /* w表示最优证例，F(w)为w的适应值 */
开始
1) 按照基于特定起始点的方法得到初始种群Y。
2) 计算种群Y中个体的适应度，并获得最大适应度向量Fmax。
3) 如果为达到预定最大迭代次数，依据选择策略，对选出的个体进行交叉，并且修正新一代个体。
4) 进行具有指向性的变异操作。
5) 产生新一代种群Y，计算适应度，获得最大适应度向量Ftemp。
6) 如果Ftemp优于Fmax则将Ftemp赋给Fmax，返回3)，如果Ftemp次于Fmax，则结束循环。
7) 从种群中选择所需的最优个体。
结束
3 算法分析与实验结果 3.1 正确性与可终止性基于遗传的证例搜索算法是可终止的，算法有两种结束方式：1)执行的每一代操作都有一个最大的适应度值，若经过遗传操作交叉和变异之后产生的新一代的最大适应度值比其父代的最大值没有增大；2)算法执行完预定的最大迭代次数[19]。因此计算过程最多在T次迭代后结束，T为预先设定的最大迭代次数，即本文的算法满足可终止性。遗传算法的适应度函数保证了所求解最优，选择操作的修正和定向的变异保证所求解是模型中的路径，这也就保证了本文算法满足正确性。
3.2 时间复杂度分析探讨基于遗传算法的证例生成算法的时间复杂度，首先要确定模型的状态数n，迁移数为t，初始状态的迁移数x0,x1…,xm，则种群规模L=x0,x1…,xm，k为路径的最大长度，则初始化种群的时间复杂度为O(Lk)。对种群进行交叉操作的时间复杂度为O(Lk/2)。变异操作中判断一个个体是否是正确路径的时间复杂度为O(kt)，计算单步可达状态集合的时间复杂度为O(t)。而对种群进行适应度计算的时间复杂度为O(Lk)。
通过上述分析可知，基于遗传算法的证例生成算法的最大时间复杂度为O(kt)，k表示最大路径长度是一个常数。
3.3 实验结果为了验证本文的算法，实现了一个java语言的编写的遗传算法的证例生成程序。程序运行环境为双核Intel Core i5-4210U @ 1.70 GHz 2.40 GHz处理器，内存为4 GB，操作系统为64位的Windows 7。
Stefan和Mitra[20]提出了一个评价依靠原因依赖进行错误定位算法的指标，被广泛的应用于评价算法所需要的人工操作程度，简单表示为score=1-distance/counterexample。其中distance是所求证例与反例的差异，本文使用字符串编辑距离；|counterexample|是反例的长度，本文即为k。score值越大算法效率越高，需要的人工操作越少。基于此评价指标，本文在五个模型的八个规约上验证了此算法。分别是两个互斥模型Smutex[15]和Mutex2[18]，微波炉模型MOvn[1]，Andrew文件系统(AFS-1)[21]，以及社保审计的模型Policy，其中Policy验证了四个规约。实验结果如表 2所示，其中SN为状态数量，TN为迁移数量，k为反例长度，GN是最优迭代次数，distance为最优证例与反例的字符串编辑距离，score为评价指标的分值。
| 模型 | SN | TN | k | L | GN | Distance | Score |
| Smutex | 4 | 6 | 2 | 2 | 2 | 1 | 0.5 |
| MOvn | 7 | 11 | 3 | 2 | 3 | 2 | 0.667 |
| AFS-1 | 16 | 21 | 2 | 8 | 2 | 2 | 0 |
| Mutex2 | 17 | 27 | 4 | 4 | 3 | 1 | 0.75 |
| Policy2/φ1 | 82 | 245 | 2 | 7 | 3 | 2 | 0 |
| Policy2/φ2 | 2 | 7 | 1 | 1 | 0.5 | ||
| Policy2/φ3 | 2 | 7 | 1 | 1 | 0.5 | ||
| Policy2/φ4 | 2 | 7 | 1 | 1 | 0.5 |
从表 2中数据可以看出，Mutex2模型验证是生成反例最长，算法生成的最优解与反例相差为1，算法的分值最高需要的人工操作也最少。相反AFS-1与Policy模型的φ1规约的分值为0，是由于反例的长度为2，最优解与反例的距离为2，也就是反例上所有的状态都被认为是错误的，这就需要更多的人工操作来判断结果是否正确。表 2中GN表明算法能在极少的进化步骤内就能找到最优解，本文算法很快能达到收敛状态，效率很高。
4 结论本文将遗传算法引入模型检测中的反例理解，提出了一种利用遗传算法，获取最近证例的算法，充分的利用了反例中的信息和模型的特点，得出如下结论：
1) 使用遗传算法可以快速准确的找到反例的最近证例，对于复杂度很高的模型有很好的鲁棒性；
2) 使用多个评价指标和定向的变异策略，不仅能在极少的进化次数内找到最优解，并且具有很好的收敛性，使得算法的时间复杂度显著降低。
由于遗传算法具有良好的并行性，本文提出的算法可以扩展为相应的并行搜索算法，以加快求解速度。
| [1] | CLARKE E, GRUMBERG O. Model checking[M]. Cambridge: MIT Press, 1999 . |
| [2] | BEER I, BEN-DAVID S, CHOCKLER H, et al. Explaining counterexamples using causality[J]. Formal methods in system design, 2012, 40(1): 20–40. DOI:10.1007/s10703-011-0132-2 |
| [3] | WANG Chao, YANG Zijiang, IVANĈIĈF, et al. Whodunit? Causal analysis for counterexamples[M]//GRAF S, ZHANG Wenhui. Automated technology for verification and analysis. Berlin Heidelberg: Springer, 2006: 82-95. |
| [4] |
黄宏涛, 黄少滨, 陈志远, 等. [J].
基于克雷格插值的反例理解方法, 2013, 51(1): 94–100.
HUANG Hongtao, HUANG Shaobin, CHEN Zhiyuan, et al. [J]. Understanding counterexamples based on Craig interpolation, 2013, 51(1): 94–100. |
| [5] | HALPERN J Y, PEARL J. Causes and explanations: a structural-model approach. Part I: Causes[J]. British journal for the philosophy of science, 2005, 56(4): 843–887. DOI:10.1093/bjps/axi147 |
| [6] | SVLFLOW A, FEY G, BLOEM R, et al. Using unsatisfiable cores to debug multiple design errors[C]//Proceedings of the 18th ACM Great Lakes symposium on VLSI. New York, 2008: 77-82. |
| [7] | CHEN Yibin, SAFARPOUR S, MARQUES-SILVA J, et al. Automated design debugging with maximum satisfiability[J]. IEEE Transactions on computer-aided design of integrated circuits and systems, 2010, 29(11): 1804–1817. DOI:10.1109/TCAD.2010.2061270 |
| [8] | GROCE A, VISSER W. What went wrong: explaining counterexamples[M]//BALL T, RAJAMANI S K. Model Checking Software. Berlin Heidelberg: Springer, 2003, 2648: 121-136. http://cn.bing.com/academic/profile?id=1511405608&encoded=0&v=paper_preview&mkt=zh-cn |
| [9] | GROCE A, CHAKI S, KROENING D, et al. Error explanation with distance metrics[J]. International journal on software tools for technology transfer, 2006, 8(3): 229–247. DOI:10.1007/s10009-005-0202-0 |
| [10] | CHAKI S, GROCE A, STRICHMAN O. Explaining abstract counterexamples[C]//Proceedings of the 12th International Symposium on Foundations of Software Engineering. Newport Beach, 2004: 73-82. http://cn.bing.com/academic/profile?id=2169565104&encoded=0&v=paper_preview&mkt=zh-cn |
| [11] | WANG Tao, ROYCHOUDHURY A. Automated path generation for software fault localization[C]//. Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering. New York, 2005: 347-351. http://cn.bing.com/academic/profile?id=2133074421&encoded=0&v=paper_preview&mkt=zh-cn |
| [12] | HOLLAND J H. Adaptation in Natural and Artificial Systems[M]. Cambridge: MIT Press, 1992 . |
| [13] |
陈国彬, 张广泉. 基于改进遗传算法的快速自动组卷算法研究[J].
计算机应用研究, 2015, 32(10): 2996–2998.
CHEN Guobin, ZHANG Guangquan. New algorithm for intelligent test paper composition based on improved genetic algorithm[J]. Application research of computers, 2015, 32(10): 2996–2998. |
| [14] |
曲志坚, 张先伟, 曹雁锋, 等. 基于自适应机制的遗传算法研究[J].
计算机应用研究, 2015, 32(11): 3222–3225.
QU Zhijian, ZHANG Xianwei, CAO Yanfeng, et al. Research on genetic algorithm based on adaptive mechanism[J]. Application research of computers, 2015, 32(11): 3222–3225. |
| [15] | BIERE A, CIMATTI A, CLARKE E M, et al. Bounded model checking[J]. Advances in computers, 2003, 58: 117–148. DOI:10.1016/S0065-2458(03)58003-2 |
| [16] | LEWIS D. Causation[J]. The journal of philosophy, 1973, 70(17): 556–567. DOI:10.2307/2025310 |
| [17] |
施小纯. 基于反例搜索的启发式模型检测算法的研究[D]. 北京: 中国科学院研究生院(软件研究所), 2004: 49-50.
SHI Xiaochun. A heuristic algorithm for model-checking based on counter example finding[D]. Beijing: Institute of Software Chinese Academy of Sciences, 2004: 49-50. http://cdmd.cnki.com.cn/article/cdmd-80150-2004086600.htm |
| [18] | HUTH M, RYAN M. Logic in Computer Science: Modeling and Reasoning about Systems[M]. London: Cambridge University Press, 2004 . |
| [19] |
张健沛, 李泓波, 杨静, 等. 基于归属不确定性的变规模网络重叠社区识别[J].
电子学报, 2012, 40(12): 2512–2518.
ZHANG Jianpei, LI Hongbo, YANG Jing, et al. Variable scale network overlapping community identification based on identity uncertainty[J]. Acta electronica sinica, 2012, 40(12): 2512–2518. |
| [20] | LEUE S, BEFROUEI M T. Counterexample explanation by anomaly detection[M]//DONALDSON A, PARKER D. Model Checking Software. Berlin Heidelberg: Springer, 2012: 24-42. http://cn.bing.com/academic/profile?id=40911479&encoded=0&v=paper_preview&mkt=zh-cn |
| [21] | WING J M, VAZIRI-FARAHANI M. A case study in model checking software systems[J]. Science of computer programming, 1997, 28(2/3): 273–299. |