[1]梁陈良,聂长海,徐宝文,等.一种基于模型检验的类测试用例生成方法[J].东南大学学报(自然科学版),2007,37(5):776-781.[doi:10.3969/j.issn.1001-0505.2007.05.008]
 Liang Chenliang,Nie Changhai,Xu Baowen,et al.Using model checking to generate test cases for class testing[J].Journal of Southeast University (Natural Science Edition),2007,37(5):776-781.[doi:10.3969/j.issn.1001-0505.2007.05.008]
点击复制

一种基于模型检验的类测试用例生成方法()
分享到:

《东南大学学报(自然科学版)》[ISSN:1001-0505/CN:32-1178/N]

卷:
37
期数:
2007年第5期
页码:
776-781
栏目:
计算机科学与工程
出版日期:
2007-09-20

文章信息/Info

Title:
Using model checking to generate test cases for class testing
作者:
梁陈良 聂长海 徐宝文 陈振宇
东南大学计算机科学与工程学院, 南京 210096; 江苏省软件质量研究所, 南京 210096
Author(s):
Liang Chenliang Nie Changhai Xu Baowen Chen Zhenyu
School of Computer Science and Engineering, Southeast University, Nanjing 210096, China
Jiangsu Institute of Software Quality, Nanjing 210096, China
关键词:
软件测试 模型检验 时序逻辑 测试用例
Keywords:
software testing model checking temporal logic test case
分类号:
TP311
DOI:
10.3969/j.issn.1001-0505.2007.05.008
摘要:
提出一种新的自动生成类测试用例的方法.使用符号执行从类源代码抽取对象的状态和行为,以一个四元组抽象描述类,并转化成等价的Kripke结构.使用CTL公式描述测试覆盖标准,然后把这组CTL公式和描述类状态行为的Kripke结构输入模型检验工具,并利用模型检验工具自动生成相应的证据路径,最后将路径转化成满足相应覆盖标准的类测试用例.该方法直接从源代码生成测试用例,并使用贪心法约减冗余用例以降低测试成本.实验表明该方法生成的测试用例具有较高的覆盖率.
Abstract:
A novel approach is presented to generate test cases for class testing. The states and the behaviors of the object are extracted from the source code. Then the class under testing is characterized abstractly with a 4-tuple, which can be converted into an equivalent Kripke model. The coverage criteria are expressed by computer tree logic(CTL)formulae. Model checker generates witnesses automatically when verifying CTL formulae on that Kripke model. The witnesses can be converted into a test suite which satisfies the corresponding coverage criteria. Test cases are generated from source code directly, and the greedy method is used to reduce redundant test cases in order to save the cost of software testing. The experimental results show that test cases generated by the proposed approach can achieve high rate of coverage.

参考文献/References:

[1] Clarke E M,Grumberg O,Peled D. Model checking [M].Cambridge,Massachusetts:MIT Press,1999:61-87.
[2] 林惠民,张文辉.模型检测:理论、方法与应用[J].电子学报,2002,30(12A):1907-1912.
  Lin Huimin,Zhang Wenhui.Model checking:theories,techniques and applications[J]. Acta Electronica Sinica,2002,30(12A):1907-1912.(in Chinese)
[3] Ammann P,Black P,Majurski W.Using model checking to generate tests from specifications [C] //Proceedings of the Second IEEE International Conference on Formal Engineering Methods.Brisbane,Queensland,Australia,1998:46-54.
[4] Gargantini A,Heitmeyer C.Using model checking to generate tests from requirements specifications[C] //Proceedings of the 7th European Engineering Conference Held Jointly with the 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering.Toulouse,FR,1999:146-162.
[5] Rayadurgam S,Heimdahl M P.Coverage based test case generation using model checkers[C] //Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems.Washington,USA,2001:83-91.
[6] Hong H S,Lee I,Sokolsky O,et al.A temporal logic based theory of test coverage and generation[C] //Proceedings of the International Conference on Tools and Algorithms for Construction and Analysis of Systems.Grenoble,FR,2002:327-341.
[7] Kung D C,Suchak N,Gao J,et al.On object state testing[C] //Proceedings of the 19th International Computer Software and Applications Conference.Taipei,1994:222-227.
[8] Clarke L.Symstra:a system to generate test data and symbolically execute programs [J]. IEEE Transactions on Software Engineering,1976,2(3):215-222.
[9] Xie T,Marinov D,Schulte W,et al.A framework for generating object-oriented unit tests using symbolic execution [C] //Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Edinburgh,UK,2005:365-381.
[10] Visser W,Pasareanu C S,Khurshid S.Test input generation with java PathFinder [C] //Proceedings of 2004 ACM SIGSOFT International Symposium on Software Testing and Analysis.Boston,MA,USA,2004:97-107.
[11] Harrold M J,Gupta R,Soffa M L.A methodology for controlling the size of a test suite [J]. ACM Transactions on Software Engineering and Methodology,1993,2(3):270-285.
[12] 聂长海,徐宝文.一种最小测试用例集生成方法[J].计算机学报,2003,26(12):1690-1696.
  Nie Changhai,Xu Baowen.A minimal test suite generation method [J].Chinese Journal of Computers,2003,26(12):1690-1696.(in Chinese)

相似文献/References:

[1]李磊芳,徐宝文,陈振宇,等.一种新的布尔规格测试用例生成算法[J].东南大学学报(自然科学版),2010,40(2):291.[doi:10.3969/j.issn.1001-0505.2010.02.014]
 Li Leifang,Xu Baowen,Chen Zhenyu,et al.A novel approach of test case generation for Boolean specification[J].Journal of Southeast University (Natural Science Edition),2010,40(5):291.[doi:10.3969/j.issn.1001-0505.2010.02.014]
[2]聂长海,徐宝文,史亮.一种基于组合测试的软件故障诊断方法[J].东南大学学报(自然科学版),2003,33(6):681.[doi:10.3969/j.issn.1001-0505.2003.06.001]
 Nie Changhai,Xu Baowen,Shi Liang.Software fault diagnosis method based on combinatorial testing[J].Journal of Southeast University (Natural Science Edition),2003,33(5):681.[doi:10.3969/j.issn.1001-0505.2003.06.001]
[3]张德平,查日军.基于Markov链使用模型的加速统计测试方法[J].东南大学学报(自然科学版),2011,41(5):949.[doi:10.3969/j.issn.1001-0505.2011.05.011]
 Zhang Deping,Zha Rijun.Acceleration statistical testing method based on Markov chain usage model[J].Journal of Southeast University (Natural Science Edition),2011,41(5):949.[doi:10.3969/j.issn.1001-0505.2011.05.011]
[4]万晓民,张德平,聂长海,等.统计测试中操作剖面的一种优化设计方法[J].东南大学学报(自然科学版),2008,38(2):233.[doi:10.3969/j.issn.1001-0505.2008.02.010]
 Wan Xiaomin,Zhang Deping,Nie Changhai,et al.Optimizing design method of operational profile in statistical testing[J].Journal of Southeast University (Natural Science Edition),2008,38(5):233.[doi:10.3969/j.issn.1001-0505.2008.02.010]

备注/Memo

备注/Memo:
基金项目: 国家杰出青年科学基金资助项目(60425206)、国家自然科学基金资助项目(60403016)、江苏省自然科学基金资助项目(BK2005060)、东南大学优秀青年教师教学科研资助项目.
作者简介: 梁陈良(1982—),男,硕士生; 徐宝文(联系人),男,博士,教授,博士生导师, bwxu@seu.edu.cn.
更新日期/Last Update: 2007-09-20