一种模型检测中异常终止的检测方法

摘要

本发明公开了一种模型检测中异常终止的检测方法，本发明提通过构造E’，对其描述并执行模型检测过程，生成反例路径并记录。反例路径给出了EFSM模型在其对应的变量配置下的详细执行步骤，且其最后部分给出了进入陷阱状态时的可终止状态信息。根据EFSM模型所表达的逻辑，容易确定此变量配置下的终止状态是否应为上述可终止状态。若此变量配置下的终止状态不应为上述可终止状态，则说明在相应变量配置下检测到可终止状态异常终止现象；否则，说明没有检测到可终止状态异常终止现象。从而，通过本发明提供的检测方法实现了异常终止现象的检测。

说明书

技术领域

本发明涉及一种模型检测中异常终止的检测方法，该方法基于时态逻辑模型检测，属于EFSM模型和时态逻辑模型检测领域，其中，ESFM(Extended Finite State Machine)为扩展有限状态自动机。

背景技术

有限状态自动机(Finite State Machine，FSM)模型是计算机领域中的一种重要描述工具，它可以对计算机系统中的很多逻辑结构进行描述。然而，FSM模型只能对系统的控制流进行建模。扩展有限状态自动机(EFSM)对FSM进行了扩展，包含了一些内部变量、操作和定义在内部变量上的判定条件。因此，EFSM模型比FSM模型具有更强的描述能力，特别是在数据流描述方面。目前，EFSM模型被广泛应用于电信、嵌入式系统、软件开发与测试等领域，许多模型验证工具(如UPPAAL和Spin)都支持EFSM模型。总体而言，EFSM模型具有很高的研究和实用价值。

EFSM是一种特殊的Mealy机。在EFSM模型中，内部变量的值域往往是有限的。一个状态迁移t(t∈T)可以定义为元组(s，x，y，g，op，e)，其中：

●s和e分别是t的起始状态和终止状态；

●g为定义在变量上的迁移判定条件；

●x和y分别表示输入和输出符号；

●op是由简单输出或赋值组成的操作序列。

状态迁移执行的一个必要前提是迁移判定条件g为true。其中，一个状态迁移的判定条件是不确定的，即可能有判定条件或没有判定条件。若在一个确定的EFSM模型中，对于任意变量配置，从任意状态出发最多有一个状态迁移可以执行，则称该EFSM模型是确定化的。

说明书附图1给出了一个包含4个状态和8个状态迁移的EFSM模型实例。在EFSM模型图中，状态用圆圈表示，带双圈的状态表示自动机的终止状态，即自动机可以在带双圈的状态处停止。状态迁移的起始状态和终止状态用带箭头的连线表示，箭头所指为该状态迁移的终止状态，箭尾为该状态迁移的起始状态，其它元素标注在带箭头的连线旁边(称为状态迁移的标签)。其中，状态迁移的标签具有“输入符号，判定条件/输出符号，操作”形式，且判定条件和操作均可为空即能被忽略。标签“a，w≤4/x，w：＝w+1”表示当状态s₂在输入符号a且满足“w≤4”(w为内部变量)时将转换到状态s₄，并且输出符号x及执行“w：＝w+1”操作。本发明做如下定义：若某状态可以作为自动机的终止状态，则称该状态为自动机的可终止状态。然而，不同输入序列所对应的终止状态可能是不同的，即自动机在确定变量配置下只能在部分可终止状态下停止。例如，在附图1中，输入序列“a，b”对应的终止状态为s₄，而输入序列“a，b，b”对应的终止状态为s₃。

说明书附图2给出了EFSM模型的另外一种表述形式。其中，该种表述形式不再明确指定输入符号。一般而言，这种表述方法用于对EFSM模型的验证。事实上，在对EFSM模型的验证过程中，给定所有变量的初始值，验证会沿着EFSM模型的相关路径执行。因此，输入符号在这种过程中不具有实际意义。在这种表示方法中，输出符号是可选的，若需要描述则用“printf”语句输出；若判定条件和操作不同时存在，则“/”符号不再存在。应用上述表示形式的一个具体实例为模型检测工具Spin。

EFSM模型引入了变量及定义在变量上的操作，使得其描述能力增强。然而，状态迁移的行为与变量相互关联，状态迁移之间通过迁移上的操作产生交互作用。因此，描述某种系统的EFSM模型中可能存在一些条件冲突、操作冲突。

操作冲突：设在EFSM模型M中，s_i和s_j是M中的两个状态，且从s_i到s_j存在一条有向路径。如果因该路径上某状态迁移的操作导致路径中的某状态迁移判定条件为假，则称该路径存在操作冲突。

例如，在附图1中，包含e(s₁，s₂)到e(s₂，s₄)的路径存在操作冲突。从一个状态到另一个状态可能存在多条边(即状态迁移)，但在不引起歧义的情况下，可用e(s，e)表示从状态s到状态e的一条边。

条件冲突：设在EFSM模型M中，s_i和s_j是M中的两个状态，且从s_i到s_j存在一条有向路径。如果因该路径上存在冲突的状态迁移判定条件，则称该路径存在条件冲突。

本发明不再给出条件冲突的实例。条件冲突和操作冲突统称为冲突，存在冲突的路径称为冲突路径。冲突路径的最主要体现是EFSM模型在某变量配置下不能按照既定的执行路径进行状态转换。

模型检测是一种最早由Clark等人提出的形式化验证方法，它能够以较小的代价对系统进行有效验证。模型检测的基本思想是通过(扩展)有限状态自动机模型表示系统行为H，用逻辑公式F描述系统性质，然后通过形式化方法验证H是否满足F。若系统性质得不到满足，则返回相应信息并提供违反相应性质的反例路径(即测试例)。由此可见，除了对系统进行自动化验证和分析外，模型检测的另一个重要应用是提供高自动化程度的测试例生成。在这种测试例生成过程中，首先利用逻辑公式描述测试需求，这种描述可称为陷阱属性。陷阱属性与指定的期望属性相反，例如，若期望模型能到达某个状态，则陷阱属性可表示该状态是不可达的。在上述基础上，诱使模型检测产生反例路径，即得到满足测试需求的测试例。

目前，最常用的模型检测技术是时态逻辑模型检测。根据时态逻辑类型的不同，可将时态逻辑模型检测分为基于线性时态逻辑(Linear-timeTemporal Logic，TLT)的模型检测(也称为线性时态逻辑模型检测)和基于计算树逻辑(Computation Tree Logic，CTL)的模型检测。模型检测技术已在全球范围内被应用到通信协议、并行系统和航空设计等领域，具有重要的研究和应用价值。典型的基于LTL的模型检测工具包括NuSMV和Spin等，典型的基于CTL的模型检测工具包括UPPAAL等。

发明内容

因此本发明针对可终止状态异常终止现象无法被模型检测工具发现的问题，提供一种对模型检测中异常终止能够进行检测的方法。

本发明采用以下技术方案：

该发明模型检测中异常终止的检测方法，该检测方法基于时态逻辑模型检测方法，且其特征在于其包括以下步骤：

1)给定一个待检测的ESFM模型，记为E，及采用的时态逻辑模型检测工具，记为M；

2)在E中增加两个陷阱状态及一个与该增加的两个陷阱状态相对应的陷阱迁移，增加陷阱状态和陷阱迁移后的模型记为E′；

3)根据M所提供的描述语言对E′进行描述，并在描述中添加陷阱布尔变量和陷阱属性，生成检测描述；

4)列出E′中所有待验证的变量配置情况，然后依次在各待验证的变量配置情况下执行模型检测，并记录输出的反例路径及其相应的变量配置情况；

5)根据步骤4)所记录的反例路径及其相应的变量配置情况验证在此变量配置下是否发生可终止状态异常中止现象：依据反例路径最后的部分给出的进入陷阱状态时的可终止状态信息，察看此变量配置下的终止状态是否不应为上述可终止状态，若是则说明在相应变量配置下检测到了可终止状态异常终止现象；否则，说明没有检测到可终止状态异常终止现象。

依据本发明技术方案的模型检测中异常终止的检测方法，首先说明一下模型检测过程实际上是在执行描述模型的程序过程中实现的。通常情况下，如果上述程序无法执行到最后，则说明待检测模型存在非正常的终止错误。然而，上述程序的某些非最后部分也可能是正常的终止部分。为了表示非执行到最后的正常终止，模型检测程序需要在相应部分附加“结束”标签，该标签与可终止状态相对应。当在某种变量配置情况下的模型检测过程中，经过一个不该在此终止的可终止状态时，存在如下可能的异常终止现象：由于描述模型时存在冲突路径等原因，导致从该可终止状态出发无法进行预期的状态转换，从而导致在该可终止状态停止。称上述异常终止为可终止状态异常终止。然而，根据模型检测程序已有的技术，在上述可终止状态附加了“结束”标签后，上述所述异常终止现象将无法被检测到。

针对可终止状态异常终止现象无法被模型检测工具发现的问题，本发明提供的检测可终止状态异常现象的方法通过构造E′，对其描述并执行模型检测过程，生成反例路径并记录。反例路径给出了EFSM模型在其对应的变量配置下的详细执行步骤，且其最后部分给出了进入陷阱状态时的可终止状态信息。根据EFSM模型所表达的逻辑，容易确定此变量配置下的终止状态是否应为上述可终止状态。若此变量配置下的终止状态不应为上述可终止状态，则说明在相应变量配置下检测到可终止状态异常终止现象；否则，说明没有检测到可终止状态异常终止现象。从而，通过本发明提供的检测方法实现了异常终止现象的检测。

上述模型检测中异常终止的检测方法，所述待检测的ESFM模型为使用所采用的检测工具验证过且没有发现任何错误的模型。

上述模型检测中异常终止的检测方法，所述检测工具优选为Spin。

优选地，所述增加的两个陷阱状态中的一个是E的可终止状态，称为终止陷阱状态，另一个是E的非终止状态，称为非终止陷阱状态。从非终止陷阱状态到终止陷阱状态的存在一条状态迁移，该状态迁移不设判定条件，且其操作对陷阱布尔变量赋假值。

优选地，在增加两个陷阱状态及一个与该增加的两个陷阱状态相对应的陷阱迁移后，要找到E中所有同时满足如下条件的自动机可终止状态：a)存在从该状态出发的状态迁移；b)从该状态出发的迁移判定条件合式不为永真。进而把找到的所有自动机可终止状态组成集合A，并对A中的各状态a作如下处理：从状态a向非终止陷阱状态添加一条具有状态迁移判定条件标签的状态迁移，且该判定条件为从a出发的迁移判定条件合式的否定。新增的状态迁移称为陷阱迁移。

优选地，所述陷阱布尔变量为一不同于E中所有变量的新增全局变量，记为p，其初始值为true，且“p：＝false”标签标注在从两个陷阱状态之间的陷阱迁移上，表示该迁移进行时用false对p赋值。

优选地，在一种变量配置情况下的模型检测过程完成后要给出该变量配置情况下模型检测完成的标识。

优选地，当E′中的变量配置空间包括大于1个的变量配置时，使用一个文件对变量配置加以存储。

优选地，在使用所述文件存储时，每行为一个变量配置，各行中的变量用空格分开，且各行按照预定次序存储各变量。

优选地，当某个变量配置下检测模型过程输出反例路径时，中断检测并输出该变量配置在存储变量配置的文件中的行号，以便记录反例路径及其对应的变量配置；并在继续执行检测时将所述行号以前的变量配置删除。

附图说明

下面结合说明书附图对本发明的技术方案作进一步的阐述，其中：

图1为带输入/输出符号的EFSM模型示例。

图2为不带输入符号的EFSM模型示例。

图3为时态逻辑模型检测中的可终止状态异常终止检测方法框架。

图4为与图2对应的陷阱状态和陷阱迁移示例。

具体实施方式

下面将结合实例对本发明加以详细说明。

说明书附图3给出了一种在模型检测过程中检测可终止状态异常终止的方法框架，具体步骤如下：

步骤一：给定一个待检测的扩展有限状态自动机模型(ESFM)，记为E，及采用的时态逻辑模型检测工具，记为M。

该步骤所指待检测的扩展有限状态自动机模型指已经通过正常模型检测的模型，即在使用采用的模型检测工具进行验证时，没有发现任何错误。典型的基于时态逻辑的模型检测工具包括Spin、UPPAAL和NuSMV等。其中，Spin是最早由Bell实验室开发的一款开源产品。2002年，该软件被授予2001年度ACM“Software System Awards”(获此殊荣的软件均具有很高的影响力，如Java)。Spin具有结构简洁、自动化程度高等特点，从而备受相关行业人员关注。因此，Spin是本方案优先采用的一种时态逻辑模型检测工具。

步骤二：在E中增加两个陷阱状态及一个与该增加的两个陷阱状态相对应的陷阱迁移，增加陷阱状态和陷阱迁移后的模型记为E′。

下面介绍一些该部分涉及到的术语。若存在从一个状态(设为s)出发的状态迁移，且这些状态迁移记为“t₁，t₂，…，t_m”(m为从s出发的所有状态迁移数量)，t_i对应的判定条件为c_i(1≤i≤m)，则称这些判定条件的合取“c₁∨c₂∨…∨c_m”为从s出发的迁移判定条件合式。本方案在此基础上进一步引入陷阱状态和陷阱迁移概念。在本方案所提出的方法中，为发现EFSM模型中可能存在的冲突路径，新增两个状态，称这两个状态为陷阱状态。在上述两个陷阱状态中，一个为自动机的可终止状态，称为终止陷阱状态；另一个为非终止状态，称为非终止陷阱状态。此外，为发现EFSM模型中可能存在的冲突路径，本发明引入陷阱迁移概念。

在EFSM模型E中增加陷阱状态和陷阱迁移的详细步骤如下：

1)增加两个陷阱状态(记为T₁和T₂)和一个从T₁到T₂的状态迁移(该状态迁移是一个陷阱迁移)，该状态迁移没有判定条件，且其操作为对p进行赋假值操作，即p：＝false，或p：＝0；

2)找到EFSM模型中所有同时满足如下条件的自动机可终止状态：a)存在从该状态出发的状态迁移；b)从该状态出发的迁移判定条件合式不为永真；

3)设2)中找到的所有状态组成集合A，则对A中的各状态(设为a，a∈A)作如下处理：从状态a向陷阱状态T₁添加一条状态迁移(该状态迁移是一个陷阱迁移)，其状态迁移标签具有判定条件，且该判定条件为从a出发的迁移判定条件合式(设为c)的否定(即)。

接下来对上述步骤做进一步的解释。在1)步中，T₂为可终止状态，T₁为非终止状态。在2)中，迁移判定条件合式不为永真表示存在一些变量赋值使得该逻辑公式为假。附图4给出了与附图2对应的该部分结构图。

步骤三：根据时态逻辑模型检测工具所提供的描述语言对模型E′进行描述，并在描述中添加陷阱布尔变量和陷阱属性。生成检测描述。

不同的模型检测工具可能提供不同的EFSM模型描述方法。NuSMV使用SMV程序对模型进行描述，一个SMV程序由一个或多个模块构成。在Spin中，EFSM模型使用promela语言加以描述。promela语言的主要设计目标是提供对系统模型的描述，因此其语法相对简单。对EFSM模型进行描述是指将EFSM模型表达的逻辑用模型检测工具所提供的语言加以描述。为方便用户识别一些必要信息，在描述中需要加入一些附加提示信息，这类附加的描述对EFSM模型的正确性不构成影响。作为一个实例，下面代码段1给出图2所示EFSM模型所对应的promela语言描述代码段。需要指出的是，检测描述不包括代码段1中的黑体部分。

代码段1

             //p为陷阱布尔变量

proctype efsm(int u，v，w，z)

{

         if

         ::(u＞2)-＞printf(″1″)；

         ::(u＜2)-＞end：w＝u；z＝3

         ::(u＝＝2)-＞goto L2

         fi；

L1：if

         ::(w＜＝1)-＞printf(″end")；goto L4

         ::(w＞1)-＞goto L3//陷阱迁移

         fi；

L2：if

         ::(w＜＝1)-＞printf(″1″)；goto L1

         ::(w＞1)-＞goto L3//陷阱迁移

        fi；

L3：p＝0；

L4：

    printf(″the procedure ends″)//附加的提示信息

}

init{//变量配置在此init{}内进行

  int v1，v2，v3，v4＝0；

        run efsm(v 1，v2，v3，v4)；

}

//由命令“spin-f”生成

该部分新增加一个全局布尔变量，记为p，使得该变量不同于所有EFSM模型中存在的全局变量和局部变量，该变量的初始值为真，记为：p：＝true，或p：＝1。上述布尔变量称为陷阱布尔变量，它将在待检测描述中的开始部分定义。

当使用基于线性时态逻辑的模型检测工具时，陷阱属性可用公式表示。“□p”表示p总为真，而则表示p不总是为真，即存在p为假的情况。由于模型检测使用状态穷尽算法搜索状态空间，当且仅当终止于终止陷阱状态T2的陷阱迁移被执行至少一次时，p为假。当使用基于CTL的模型检测工具时，陷阱属性可用公式表示，其表示的意义与相同，均表示“p并不是总为真”。

在上述代码段1中，除init{}语句块之外的黑体部分为该步骤所得到的描述。其中，可用Spin工具的命令转换为如下代码：

步骤四：列出E′中所有待验证的变量配置情况，并依次在各待验证的变量配置情况下执行模型检测过程，并记录输出的反例路径及其相应的变量配置情况。

在EFSM模型中，存在若干变量配置。设EFSM模型中的变量表示为“v₁，v₂，…，v_k”，变量vi的值域为V_i，一个变量配置可用(v′₁，v′₂，…，v′_k)表示，其中v′_i∈V_i，变量配置空间大小为在本发明所提出的方法中，要对变量配置空间中的待验证的变量配置空间进行访问，并在该配置下进行EFSM模型的模型检测过程。需要指出的是待验证的变量配置空间可以是变量配置空间本身，也可以是变量配置空间的一部分。

若在某变量配置下，模型检测过程没有输出反例路径，则说明EFSM模型在该变量配置下没有可终止状态异常终止现象。若在一个可终止状态下不能沿着已有的带判定条件的迁移转换，步骤二中的陷阱迁移会将自动机带到陷阱状态，并能通过陷阱属性的帮助检测到该现象。因此，若EFSM模型包括可终止状态异常终止现象，则模型检测输出反例路径。

需要指出的是，为了区分各变量配置下的模型检测情况，在一种变量配置下的模型检测过程完成后给出该变量配置模型检测完成的信息，如：可以用printf语句输出“变量配置X已完成验证”这样的提示信息。

在步骤三给出的代码段1中，变量配置在init{}内进行。为简单起见，在代码段1中，仅给出了一种变量配置的情况。作为实例，下面给出使用模型检测工具Spin时，对步骤三中给出的代码段1进行模型检测的检测过程。相应的模型检测过程执行及其结果如下：

                                                                  

   [zhangxc@localhost～]$ spin-a exam

   [zhangxc@localhost～]$ cc-o pan pan.c

   [zhangxc@localhost～]$./pan-a

   warning：for p.o.reduction to be valid the never claim mustbe stutter-invariant

   (never claims generated from LTL formulae arestutter-invariant)

   pan：acceptance cycle(at depth 16)

   pan：wrote exam.trail

   (Spin Version 5.2.4--2 December 2009)

   Warning：Search not completed

     +Partial Order Reduction

   Full statespace search for：

     never claim+

     assertion Vio1ations+(if within scope of claim)

     acceptance cycles+(fairness disabled)

     invalid end states-(disabled by never claim)

  State-Vector 56 byte，depth reached 17，

…

                                                         

注意上述执行结果中被加黑的部分表示检测到一个错误。这个错误产生的反例路径可用如下命令加以查看：

反例路径查看

                                                               

[zhangxc@localhost～]$ spin-t-p exam

Starting：init：with pid 0

Starting：never：witth pid 1

Never claim moves to line 34[(p)]

Starting efsm with pid 2

2：proc 0(：init：)line 26″exam″(state 1)

4：proc 1(efsm)line  8″exam″(state 3)

6：proc 1(efsm)line  8″exam″(state 4)<valid end state>

8：proc 1(efsm)line  8″exam″(state 5)

10：proc 1(efsm)line 12″exam″(state 10)

             end 10：proc 1(efsm)line  12″exam″(state

11)[printf(’end’)]

             the procedure ends 12：proc 1(efsm)line 21

″exam″(state 25)[printf(’the procedure ends’)]

14：proc 1terminates

16：proc 0terminates

…

                                                               

在上面的反例路径查看结果中，加黑部分给出了导致的错误产生的一系列步骤。

当待验证的变量配置空间包括大于1个的变量配置时，使用一个文件对变量配置加以存储，以备在下次检测时能够将已经检测过的变量配置删除，同时保留未验证过的变量配置。上述文件记为待验证配置文件。在使用待验证配置文件存储时，每行为一个变量配置，各行中的变量用空格分开，且各行按照一定次序存储各变量。在本发明中，待验证的变量配置空间记为C。下面给出该部分的具体执行算法：

1.在待验证配置空间文件中读取数据，并用数组conf[l][n]存储尚未完成验证的变量配置空间C，其中，l为本次模型检测待验证的变量配置数量，n为变量数量；

2.初始化一个变量i，i＝0；

3.While(i＜k){

4.在conf[i][n]所存储的变量配置下执行模型检测过程；

5.if(无反例路径产生){

6.i：＝i+1；

7.}else{

8.printf(“current configuration：”，i+1)；

9.break；

10.}

11.}

在上述算法中，待验证配置空间用二维矩阵表示。当在某个变量配置下模型检测过程输出反例路径时，中断检测并输出该变量配置在待验证变量配置文件的行号，以便记录反例路径及其对应的变量配置。若需要继续执行，则在待验证变量配置文件中将输出行号以前的变量配置删除，然后执行步骤四。

步骤五：根据步骤四所记录产生反例路径及其相应的变量配置情况，验证在此变量配置下是否发生可终止状态异常终止现象。

反例路径给出了EFSM模型在其对应的变量配置下的详细执行步骤，且其最后部分给出了进入陷阱状态时的可终止状态信息。根据EFSM模型所表达的逻辑，容易确定此变量配置下的终止状态是否应为上述可终止状态。若此变量配置下的终止状态不应为上述可终止状态，则说明在相应变量配置下检测到可终止状态异常终止现象；否则，说明没有检测到可终止状态异常终止现象。