基于SPIN的功能测试用例生成方法研究

李建 杨晋吉

摘要摘要：提出了一种自动生成系统功能测试用例的新方法。该方法使用Promela语言对软件系统的状态和行为进行描述建模，使用LTL公式描述测试覆盖标准，然后将该组LTL公式和描述状态行为的Promela模型输入SPIN模型检测工具，并利用模型检测工具自动生成相应的证据路径，最后结合正例将路径转化成满足相应覆盖标准的系统功能测试用例，并以电梯系统模型对该方法作出了诠释。

关键词关键词：功能测试用例；SPIN；模型检测；Promela建模

DOIDOI：10.11907/rjdk.161463

中图分类号：TP306文献标识码：A文章编号文章编号：16727800（2016）007000103

0引言

软件测试是指新开发出来的软件运用于实际生产前，对其需求的分析、设计规格的说明以及最终编码的复核审查，它是保证软件质量的关键步骤。利用最少的时间和测试用例来找到软件开发过程中各阶段潜在的错误以保证该开发软件的质量，是软件测试的最终目的和终极目标。

为改变近年来人们对软件测试用例生成全靠手工完成的状况，同时满足自动化生成测试用例的需求，本文提出一种基于SPIN工具的系统功能测试用例自动化生成方法。首先，将待测系统的行为及状态基于符号的执行从源代码中抽取出来；然后，使用一组线性时态逻辑（LTL）公式描述特定的覆盖标准；最后，将建立好的Promela模型与代表系统属性的LTL公式一起输入到SPIN中进行检测。如此，就将模型检测工具的自动化验证过程转化成了测试用例生成过程，即SPIN生成的与LTL公式相对应的证据路径。图1为基于SPIN的自动生成测试用例技术框架。

1基于SPIN的测试用例生成基本思路

SPIN是由美国贝尔实验室开发出来的模型检测器，它主要用来对非实时系统模型进行检测，即验证某个有穷状态的系统是否满足利用LTL公式描述的属性。本文将系统功能测试用例生成的问题转化为一个模型检测问题，将生成测试用例的问题变换成验证模型检测中“状态不可达”、“不存在此条路径”等性质的问题。通过建立SUT行为模型，将一个测试覆盖标准构建为模型检测器的验证条件，并将模型检测得到的反例变换成测试用例集。由于模型检测工具能够利用生成的反例来解释违反了应满足系统性质的情况，因而此种反例很适合作为功能测试的路径。

为了利用模型检测过程得到的反例来生成测试用例集，需要取反用时序逻辑公式描述的测试覆盖标准，即假设测试覆盖标准永不为真，对原有的时序逻辑描述特性进行否定。检测时，若检测到系统与某个时序逻辑描述不一致，就会生成反例，说明模型不满足性质的原因，这是可能的一个测试用例的序列。当反复验证所有性质时，可以得到一系列能实现测试覆盖标准的测试用例的序列。2系统建模与模型检测

采用模型检测技术对被测系统和测试覆盖标准进行形式化描述，本文采用Promela描述被测系统，用 LTL 描述测试覆盖标准。2.1Promela建模

不是一般的程序语言，而是一款专用来描述并发系统的模型语言，用来建模有限状态系统。它类似于C语言的语法结构，能够动态地创建并行进程，进程间的通讯通过消息通道来实现，通讯方式有2种：异步、同步。由Promela建立的模型组成包括进程、消息通道、对象和变量等，如图3所示。

2.2LTL公式逻辑描述

与CTL相比较，LTL更适合对并发程序的性质进行验证，所以本文使用的是LTL逻辑公式。在SPIN中，LTL算子包含有&&、||、→、！和3种时序算子：① <> p：表示p在未来的某个状态点成立；② p：表示p在未来的所有状态点都成立；③ p∪q：表示p在所有状态点都成立直到遇到第一个状态点使q成立。在iSpin中，必须对每一个用到的LTL符号增加一个宏定义，即声明p、q所代表的等式。 2.3SPIN检测

SPIN由贝尔实验室用ANSI C开发，可在所有UNIX操作系统版本中使用，也可在安装了Windows 95以上版本、Linux等操作系统中使用。 SPIN工具的思想是求两个自动机的交集，如果为空集，则安全特性得到验证，否则输出不满足该安全特性的行为轨迹。

采用形式化公式来表达，即证明M╞是否成立，其中，M表示模型，表示时态逻辑公式。分别将转换成自动机A，将M转换成AM，即相当于证明：

2.4反例分析

SPIN采用双重深度优先搜索方式进行状态搜索，遇到反例路径后就退出搜索，并将路径打印到一个后缀名为“.trail”的文件里。这种方法的优点是完全自动化，系统若不满足给定的性质，检验结果就给出反例，生成的反例反映一个状态变换的路径，该路径包括一序列步骤，相应状态的取值在每一步骤中都会被给出。可以用系统简化的模型来反例跟踪，再结合正例来比较就可总结得出所需要的系统功能测试用例。3实验验证

3.1电梯系统

电梯在运行时分为如下3种状态：①空闲状态：电梯没有发出目的层呼叫信号和呼叫电梯信号；②等待状态：开始响应某一个呼叫电梯的信号，或有乘客正进、出电梯；③运行状态：正在响应某一个呼叫电梯信号。电梯系统运行模型如图5所示。

3.2建模与LTL

3.2.1模型的Promela描述

为了举例描述本文提出的方法，本次建模只是选取了1个人、上下4层楼电梯的模型作为例子，涉及3个进程Person（）、Servis（）、Elevator（）以及3个通道：

3.2.2LTL性质描述

以下性质以乘客去3楼为例，建立检验规约，去其它楼层同理可行。

（（going_to==3）-><>（at_floor==3）），此条性质说明乘客将要去3楼，则在以后的运行状态中该电梯必须有一个状态为到达并停在3楼的情况。

（（going_to==3）-><>！（at_floor==3）），此性质为实验的缺陷性质，即将原本成立的性质全部或部分取反，如果验证工具给出反例，则说明该性质是不满足的。从反例给出的路径可以分析得到想要的功能测试用例。

3.2.3验证与结果

首先在官网下载cygwin软件（用于虚拟Linux环境），点击下载安装所有安装包，以免出错；然后启动XWin server服务器（用于生成iSpin界面）；最后启用iSpin，导入已完成系统建模的Promela描述。

进行语法检验，Syntax Check，得到结果显示无语法错误，并且提示有用到2个ltl公式分别为e1、e2。

点击Verification，选择use claim，验证性质e1，点击run。从结果可看到State-vector 68 byte， depth reached 1162， errors：0，还可以在最后一行看到No errors found -- did you verify all claims？由此可知e1性质满足该系统正常运行。

同理，可以验证e2。从e2的结果图中可看到State-vector 68 byte， depth reached 164， errors：1，可知该性质不支持该验证系统的正常运行，并且由最后一行提示：To replay the error-trail， goto Simulate/Replay and select“run”可知已经自动生成了反例。最后可以切换到Simulate/Replay 选择Guided，with trail：Elevator_protocol.pml.trail browse 点击“（Re）Run”，得到反例结果路径。

由e2这一陷阱性质可以知，该性质是不满足该电梯系统的，即说明存在乘客将要去3楼，则在以后的运行状态中该电梯必须有一个状态为到达并停在3楼的情况。根据检验LTL描述的属性出现的反例路径，如图6所示。

根据反例路径结合无错误路径给出的LTL性质可知该系统的一个可用测试用例为：该乘客发出去3楼的信号，最终电梯会停留在3楼，因此得到测试用例如表1所示。