模型检测引导的TTCN-3测试套生成技术研究

孙　晶　金晓文

(北方工业大学信息工程学院　北京 100144)



模型检测引导的TTCN-3测试套生成技术研究

孙晶金晓文

(北方工业大学信息工程学院北京 100144)

针对软件测试的不完备性以及软件测试自动化问题，提出在测试过程中将模型检测前置于传统测试，将模型检测与测试相结合。通过分析模型检测中的形式化规约明确测试目的，并转换成TTCN-3(Testing and Test Control Notation) 抽象测试套。进一步利用规约中本身存在的正例，与数据类型描述文件相关联，从而生成测试用例。分析TTCN-3开发模式，基于标签转换系统与TTCN-3行为树的等价性，提出模型检测引导的抽象测试套生成算法，并实现TTCN-3抽象测试套的自动生成。

软件测试模型检测TTCN-3测试套μ演算

0　引　言

近年来，模型检测以其自动化程度高的特点在软件测试领域得到了广泛关注。由于模型检测可以自动执行，并能在系统不满足性质时提供反例路径来说明不满足的原因，因此在工业界比演绎证明更受推崇。而测试是保证软件产品可靠性和正确性的传统手段，相较模型检测而言自动化不高，手动选取测试用例有不完备性。

模型检测是关于自动验证并行或者分布式系统性质的算法和方法，它的基本思想是用状态迁移系统(S)表示系统的行为，用模态逻辑公式(F)描述系统的性质。这样“系统是否具有所期望的性质”就转化为数学问题“状态迁移系统S是否是公式F的一个模型？”，用公式表示为S╞F[1]。对有穷状态系统，这个问题是可判定的，即可以用计算机程序在有限时间内自动确定。而基于模型检测的测试用例自动生成已经有较长的研究历程。由P.Ammann[2]等提出的贯彻始终的基本思想是利用模型检测工具提供的描述语言刻画软件需要满足的性质，并利用工具进行全空间的搜索；当性质不满足的时候，工具会捕捉所有的反例路径，然后再根据反例提供的线索生成测试用例。Cong Tian[3]等也提出了利用模型检测从谓语连词中自动生成测试用例的方法。并且提出了一个算法将测试用例的生成从基于原子谓语表达式的连接转化为模型检测。而韩国釜庆大学Jaeyoun Jung[4]等实现了一种为LTS过程规范而提出的模型检测工具，它可以用来检查死锁，活锁，可达状态以及动作。在国内，苏开乐[5]等提出了一个关于时态逻辑CTL* 的符号化模型检测算法。 该算法通过所谓的tableau 构造方法来判定一个有限状态系统是否满足CTL* 规范。清华大学何恺铎[6]等提出了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法， 并结合自行研发的Jchecker 工具详细介绍了该软件模型检测技术的运作过程和关键算法。而与此同时，TTCN-3作为一种功能强大的基于响应系统的黑箱测试标准，早已发展成为了一种通用的测试规格语言。早在1997年，国内学者郝瑞兵[7]等就已提出了一种形式化的基于TTCN的测试执行方法。其使用了标号变迁系统(LTS)刻画了这一方法的整个执行过程，并给出了具体实现。而蒋凡[8]等在经过多年在TTCN-3领域中的研究之后，其概括地提出了TTCN-3 测试套开发模式并实现了应用。而Niusha Hakimipour[9]等，提出了一个从“需求”中生成测试用例的方法，并使用行为树(BT)来建模系统需求。国防科技大学颜烔[10]等在基于模型的软件测试综述一文，概述了基于模型的软件测试的方法，阐明软件测试模型是对软件行为和软件结构的抽象描述，可以用于生成软件测试例。

可是不论是新兴的模型检测还是传统的软件测试都有其弊端，模型检测会由于值域太泛而导致状态爆炸[11]，而传统测试又有其不完备性[12]。所以本文提出一种模型检测引导的TTCN-3测试套生成技术，该技术通过对将软件的所有状态转化成LTS(Label Transition System)，然后根据测试目的对标签转换系统进行形式化规约，在明确了测试目的之后进行自动化的软件测试。

1　TTCN-3概述

TTCN是一个由ETSI(European Telecommunications Standards Institute)维护的全球适用的标准测试语言。在第三代标准中，TTCN-3是一个现代的且灵活的语言，其广泛的接口机制，被用于描述许多类型的系统测试。典型的应用领域为系统测试、交互性测试、协议测试、业务测试、模块测试等。

TTCN-3作为标准测试语言，其不仅囊括了普通程序设计语言的简单明了，易于人机交互。而且其拥有便于测试的功能支持，如动态测试配置、测试判决处理、定时器机制、通信机制等。

TTCN-3连接是端口到端口和端口到测试系统接口的连接。其测试配置如图1所示。所以从某一方面而言，TTCN-3所描述的测试系统就是根据测试目的进行动态测试配置，并通过定时器机制、通信机制等进行测试并最后进行测试判决处理。

图1　动态测试配置

用TTCN-3描述测试系统，就是抽象测试套的生成。目前的方式还只是限于手动编写文本格式的TTCN-3文件，或用GFT图形化标准进行转化。但上述两种方式是人为的，比较被动。由于TTCN-3的层次结构和基本作用域范围的控制[13]，手动书写TTCN-3测试套还是存在一定的错误和风险。

对于TTCN-3的执行环境，目前在国内外已有研究和应用。如Elvior、OpenTTCN Tester、Testing Technologies公司开发的TTworkbench都是TTCN-3官网上公布的很权威的TTCN-3的编译、运行环境。而国内， 中国科学技术大学也已开发了协议测试工具——LoongTesting，且兼容了Windows及Linux平台。

2　TTCN-3测试套的自动生成

2.1模型检测引导

模型检测的基本步骤为：建模、规范和验证。

在建模过程中，需要对系统功能进行描述，常用的一种描述形式是标签转换系统LTS。规范是根据测试目的(系统期望满足的性质)进行形式化描述，之后通过模型检测工具进行验证。

例如一个LTS描述的被测系统，状态S={0,1,2}， 初态I={0}，转移动作→={<0,1>, <1,1>*,<1,2>}，活动A={a0,a1,a2…,a9}，谓词P={True,False}。LLTS={, *, }表达了一个活动a0,a1执行的实例，如图2所示。对于系统的某个功能进行描述，即对标签转换系统的某一个性质进行断言描述，则可描述为：[a0.a1*]true。

图2　被测系统的LTS描述

本实验项目组分为三部分，第一部分是对软件行为和软件结构的抽象描述，将被测系统用LTS的形式(控制流图)描述出来，并转化成为服务描述语言bpel和wsdl进行物理存储. 第二部分涉及测试目的引导的模型检测，即通过明确测试目的，转化为模态逻辑公式μ演算。并与LTS描述的被测系统相结合，进行模型检测。本文是第三部分，通过分析模型检测中的形式化规约(μ演算)明确测试目的，自动化转换成TTCN-3 抽象测试套。可以看出，经过本项目组其他工作之后，我们已得到了一个构造完整的测试模型。

2.2测试套生成

对TTCN-3测试系统而言，针对特定的被测系统，用户自定义部分有两个方面：(1) 根据被测系统测试要求编写 TTCN-3 测试例；(2) 根据TTCN-3测试例和被测系统编写或者重用可执行测试套(适配器)[8]。

对于黑盒测试语言TTCN-3而言，首先要明确其测试目的。在项目组第二部分的工作中，已将形式化规约描述的活动序列转化为μ演算来描述，这就帮助明确了测试目的。因为其只描述了关键活动，为了方便理解，可以将其看做是“简化的LTS”。而基于LTS与TTCN-3行为树的等价性[14]，提出了抽象测试套生成算法。

算法1抽象测试套生成算法

Input: the μ-calculus

Output: TTCN-3 behavior tree

BEGIN

Read the μ-calculus, extract LTS sequence in the μ-calculus

FOR each LTS sequence DO

IF sequence=a THEN rewrite to s replace True with pass and False with fail.

IF sequence=R1 ″.″ R2, THEN rewrite to {s1, {s2⊆s1}}

//顺序结构

IF sequence= R1 ″|″ R2, THEN rewrite to {{s1⊆s}, {s2⊆s}}

//分支结构

IF sequence= R1 ″*″R2, THEN rewrite to {{s1}*,{s2⊆s1}}

//循环结构

IF sequence=R1″+″ R2, THEN rewrite to {{s1}+,{s2⊆s1}}

//至少执行一次的循环结构

END

END

在提出了算法后，就可以将其进行自动化的转化，实现可执行测试套的自动生成。我们先从左至右扫描μ演算文件，分离存储事件(event)和逻辑部分(logic)，并解析相关的bpel文件，根据μ演算与TTCN-3的映射关系，依次生成TTCN-3抽象测试套的主体部分。

do_module();

do_component();

do_function();

do_testcase();

由于μ演算中正则公式的逻辑表达形如R1.R2、R1|R2、R1*R2、R1+R2， 所以要借用编译原理的中回溯技术，来完成μ演算的扫描与解析，并将μ演算中对应的逻辑部分翻译成TTCN-3的逻辑表达。

TTCN-3与μ演算的重要映射关系如表1所示， 其余未在表中列出的关系，如测试套、定时器、主测试成分等的名字，采用了自动化命名的方式，形如TC_0()。

表1　TTCN-3与μ演算的重要映射关系

μ演算相同的事件门操作(event)会抽象成同一组件的行为，会在同一个函数中来实现。例如，一个μ演算是这样描述一个系统的["op_1 !Request_1″.″op_1 ?Response_1″]true.系统首先会产生一个主测试成分mtcType,然后根据对应系统描述会产生op_1function(),然后在测试例testcase中根据逻辑生成调用function的关系。

又例如，一个复杂一些的μ演["op_1 !Request_1″.″op_1 ?Response_1″.″op_2 !Request_2″.″op_2 ?Response_2″]true，则会对应俩个函数function,分别为op_1function() 和op_2function()，测试套中表现了函数之间的调用关系。可以看出对于上述μ演算样例而言，逻辑关系是顺序的，且对应描述如下：

testcase TC_0() runs on mtcType{

op_1function();

op_2function();

}

3　测试例的自动生成

在构造完测试模型之后，我们的任务就是生成和执行测试例[10]。由于传统测试中的不完备性，对于测试例的选取有局限性。模型检测自动化全部遍历所有空间状态，可以对所有的活动序列的属性进行形式化规约，并检测出不符合形式化规约的反例路径，这就借鉴了传统的基于模型检测的测试用例自动生成的方法，而与此同时应该注意到形式化规约中，是存在正例路径的，所以拓展这一部分，并将得到的模型检测的结果与相关的数据类型描述文件(bpel组合中的wsdl)进行关联，解析bpel中名称空间里wsdl的位置(lns)，同时根据需要获取数据类型的消息名称来提取测试用例。

例如，一个μ演算是这样描述一个系统[″op_1 !Request_1″.″op_1 ?Response_1″]true. 我们可以通过这样的形式化规约获得发送和接受的消息名称Request_1和Response_1，然后检索相关的数据类型描述文件，就可以得到一个精确的测试用例的类型。具体提取的信息截取如下：

[org.dom4j.Namespace@6f2c2097 [Namespace: prefix mapped to URI ″http://docs.oasis-open.org/wsbpel/2.0/process/executable″], org.dom4j.Namespace@1d3b6455 [Namespace: prefix lns mapped to URI ″C:/Users/Administrator/Desktop/常用文档/P0/wsdl″]]

Request_1

Retrieving document at ′C:/Users/Administrator/Desktop/常用文档/P0/wsdl/1.wsdl′.

Service Name:

1

Port Name:

(1)验证了水是TSR反应发生的必要条件，在无水条件下 ，CaSO4不能引发TSR反应生成H 2 S。

PortType_1

Operation Name:

op_1

Messages:

Request_1

parameter name:i parameter type:integer

可以看出根据wsdl提取出了变量的数据类型，最后依照传统测试中等价类划分的方法提取测试用例，嵌入到之前已经生成好的抽象测试套的逻辑框架中。对于复杂数据类型如record等，提供了数据模板模块，用户可以根据测试需求与模板格式进行手动加载。

4　案例研究与评估

4.1案例研究

图3　八皇后主程序程序流图

八皇后问题是一个以国际象棋为背景的问题：如何能够在8×8的国际象棋棋盘上放置八个皇后，使得任何一个皇后都无法直接吃掉其他的皇后。为了达到此目的，任两个皇后都不能处于同一条横行、纵行或斜线上。

如果针对主程序进行完整测试，则对应μ演算描述为：

[″op_1 !Request_1″.″op_1 ?Response_1″.(″op_2 !Request_2″.″op_2 ?Response_2″.″op_3 !Request_3″.″op_3 ?Response_3″.(″op_4 !Request_4″.″op_4 ?Response_4″.″op_5 !Request_5″.″op_5 ?Response_5″)*.″op_6 !Request_6″.″op_6 ?Response_6″)*.″op_7 !Request_7″.″op_7 ?Response_7″.″op_P1 !Request_P1″.″op_P1 ?Response_P1″]true

通过分析上述形式化规约，和前期已经生成好的被测系统的形式化描述文件bpel和wsdl，自动生成测试套。由于测试套庞大复杂，在此只列出测试套的数据类型定义如图4及测试例如图5所示。

图4　数据类型定义　　　　　　　图5　测试例

将生成的测试套加载在TTCN-3编译运行环境中进行验证，并根据被测系统编写配套的编解码器和适配器。得到运行结果如图6所示，可以看到定时器启用了164次符合逻辑预期。

4.2评估

在经过大量的学习和助教工作之后，我们发现手动编写TTCN-3测试套是需要大量的前期投入的，这包括对于人员的技术培训、实验环境的搭建等等。

图7　手动/自动效率对比图

在明确测试目的的前提下，对手动编写TTCN-3测试套(在保证准确的情况下)和本文中提到的自动生成TTCN-3测试套(包括配置路径的时间)进行了效率对比，如图7针对同一源代码，生成同一测试套，然后对比其所用时间。可以看出手动编写测试套的方法所用的时间会随着被测系统规模的增长呈几近指数型增长，而自动生成的时间增长并不明显。

5　结　语

关于TTCN-3测试套自动生成以及测试例生成的研究有许多。兰毓华等人[15]提出了一种基于 Z 规格说明的软件测试用例自动生成方法， 通过对软件Z规格说明的分析，找出描述软件输入、 输出约束的线性谓词，经过线性谓词转换， 线性谓词到线性不等式组的转换， 找出区域边界顶点和边界附近的测试点等过程自动生成测试用例。陈萍等[16]提出了根据 TTCN-3标准的第三部分GFT与TTCN-3核心语言的内在关联以及标准中的语法规定的一种TTCN-3测试套生成方法，并设计开发了一套由图形表示格式自动生成用核心语言描述的测试套的转换工具。赵玉兰等[17]介绍一个在GE-LOTOS的基础上自动产生TTCN测试套的工具， 该工具是基于由形式描述技术语言E-LOTOS转换成的GE-LOTOS。 并对 Internet上的一个标准路由信息协议(RIP协议)进行了TTCN测试套的应用。

与上述研究工作不同， 我们既不是基于Z规格说明，也不基于图形。与基于E-LOTOS有异曲同工之妙，都是形式化描述为根基的。本文主要研究模型检测引导的TTCN-3测试套自动生成方法。虽然测试套包含测试用例选择内容，但本文的重点在测试逻辑执行部分， 而在测试用例的选择方面， 采用的是提取模态逻辑描述中存在的正例，与相关的数据描述文件关联，从而提取测试用例。本文基于 LTS 到行为树转换的理论方法[14]， 提出了模型检测引导的TTCN-3抽象测试套生成算法，并给出了TTCN测试套自动生成的技术方案，且实际检验了该方案的可行性。

本文的不足之处在于只能生成简单数据类型的测试用例。但也基本上规避了颜烔[10]等在基于模型的软件测试综述一文中提到的基于模型的软件测试的缺点，即状态空间爆炸问题。而传统的手动编写TTCN-3测试套的模式效率不高，本文中提出的自动化生成的模式一定程度上提高了测试套生成的效率。

[1] 林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(12A):1907-1912.

[2] Ammann P,Black P E,Ding W.Model checkers in software testing[R].Technical Reprot NIST-IR 677,Naltional Institute of Standards and Technology,2002.

[3] Cong Tian,Shaoying Liu,Nakajima S.Utilizing Model Checking for Automatic Test Case Generation from Conjunctions of Predicates[C]//Berlin:Software Testing, Verification and Validation Workshops (ICSTW),2011 IEEE Fourth International Conference on,2011:304-309.

[4] Jaeyoun Jung,Youngeung Kim,Yeondae Chung,et al.A Study on Implementation of Model Checking Tool for Verifying LTS Specifications[C]//Toyko:Information Networking,1998.(ICOIN-12) Proceedings,Twelfth International Conference on,1998:539-543.

[5] 苏开乐,骆翔宇,吕关锋.符号化模型检测CTL[J].计算机学报,2005,28(11):1798-1806.

[6] 何恺铎,顾明,宋晓宇,等.面向源代码的软件模型检测及其实现[J].计算机科学,2009,36(1):267-272.

[7] 郝瑞兵,吴建平,史美林.一种形式化的基于TTCN的测试执行方法[J].软件学报,1997,8(5):367-375.

[8] 刘小勇,蒋凡.TTCN-3测试套开发模式及其应用[J].计算机辅助工程,2005,14(2):21-25.

[9] Niusha Hakimipour,Paul Strooper.Exploring an approach to model-based testing from Behavior Trees[C]//Hong Kong:Software Engineering Conference (APSEC),2012 19th Asia-Pacific (Volume:2),2012:80-86.

[10] 颜炯,王戟,陈火旺.基于模型的软件测试综述[J].计算机科学,2004,31(2):184-187.

[11] Gerard J Holzmann,Rajeev Joshi,Alex Groce.New Challenges in Model Checking[M].25 Years of Model Checking,2008:65-76.

[12] Mary Jean Harrold.Testing: a roadmap[C]//ICSE - Future of SE Track,2000:61-72.

[13] 蒋凡,谈刚.TTCN-3语言编译器符号表的设计和实现[J].中国科学技术大学学报,2007,37(7):803-806.

[14] 赵会群,孙晶,张爆,等.嵌入式API测试套生成方法和技术[J/OL].软件学报,2014,25(2):373-385.http://www.jos.org.cn/1000-9825/4541.htm.

[15] 兰毓华,毛法尧,曹化工.基于Z规格说明的软件测试用例自动生成[J].计算机学报,1999,22(9):963-969.

[16] 陈萍,赵会群,尚思超.一种TTCN测试套自动生成方法研究[J].北京化工大学学报,2007,34(S1):64-67.

[17] 赵玉兰,曾敏,叶新铭.自动产生TTCN测试套以及对RIP协议的应用[J].内蒙古大学学报:自然科学版,2004,25(6):682-687.

RESEARCH ON MODEL CHECKING-GUIDED TTCN-3 TEST SUITE GENERATION TECHNOLOGY

Sun JingJin Xiaowen

(AcademyofInformationEngineering,NorthChinaUniversityofTechnology,Beijing100144,China)

To address the problems of incompleteness and automation of software testing, we proposed to put the model checking in ahead of the customary test in testing process, this combines the model checking with test. Through analysing the formal specification of model checking we cleared the test purpose, and converted it to TTCN-3 (testing and test control notation) abstract test suite. Further, we used the example existing in the specification to associate it with a data type description file, so as to generate test cases. By analysing the TTCN-3 development mode and based on the equivalence of a labelled transition system and TTCN-3 behaviour trees, we put forward a generation algorithm of abstract test suite guided by model checking, and implemented the automatic generation of TTCN-3 abstract test suite.

Software testingModel checkingTTCN-3 test suiteμ-calculus

2014-10-13。

国家自然科学基金项目(61070030，6137 0051)；北京市教委人才创新团队计划项目(4062012)。

孙晶，副教授，主研领域：软件测试。金晓文，硕士生。

TP3

A

10.3969/j.issn.1000-386x.2016.03.003