用模型检验产生约简测试集

计算机工程与应用 ›› 2012, Vol. 48 ›› Issue (17): 93-98.

用模型检验产生约简测试集

田野，曾红卫

上海大学计算机工程与科学学院，上海 200072

出版日期:2012-06-11 发布日期:2012-06-20

Reduction of test set generation using model-checking

TIAN Ye, ZENG Hongwei

School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China

Online:2012-06-11 Published:2012-06-20

摘要/Abstract

摘要： 基于模型检验的自动化测试技术已经得到普遍应用，由于测试用例自动化生成过程中会产生巨大的资源消耗，优化问题越来越受到软件测试行业的广泛关注。提出一种基于节点权重的性质覆盖度计算方法，在模型检验器自动化生成测试用例之前对测试目标排序，能够更有效地检测到冗余性质，从而减少模型检验器被调用执行次数并且避免大规模的测试用例生成。

关键词: 模型检验, 测试生成, 性质排序, 性质集约简

Abstract: Automated testing based on model checking has gained a great popularity in the field of software testing. Consequently, the optimization during the process of test case generation has also drawn a big attention. This paper introduces an efficient method based on node weight to calculate the property coverage value. It sorts the property purposes before test case generation to obtain the maximum reduction to avoid calling redundant executives of model-
checker and generating scaled test suite.

Key words: model checking, test generation, property sorting, property set reduction

田野，曾红卫. 用模型检验产生约简测试集[J]. 计算机工程与应用, 2012, 48(17): 93-98.

TIAN Ye, ZENG Hongwei. Reduction of test set generation using model-checking[J]. Computer Engineering and Applications, 2012, 48(17): 93-98.

[1]	董玲玲1，关永1，李晓娟1，施智平1，张杰2，华伟1. 用LTL模型检验的方法验证SpaceWire检错机制[J]. 计算机工程与应用, 2012, 48(22): 88-94.
[2]	李仁见，王昭飞. 命令式程序终止性验证方法综述[J]. 计算机工程与应用, 2011, 47(28): 1-6.
[3]	蒋凡，章磊，陈军成，王建学. 基于程序分析的通信软件模型驱动测试研究[J]. 计算机工程与应用, 2009, 45(31): 66-68.
[4]	谭亮,曾红卫. 基于接口自动机的Web应用验证[J]. 计算机工程与应用, 2009, 45(3): 70-73.
[5]	刘恩军. 基于线性带权值的广义表的模型检验方法[J]. 计算机工程与应用, 2008, 44(29): 88-91.
[6]	曾琼¹,黄健^2,3,魏乐^2,3. 基于吴方法的符号模型检验[J]. 计算机工程与应用, 2008, 44(27): 46-48.
[7]	高新岩¹,吴尽昭¹,闫炜¹,周宁². 非经典切片技术及其在形式验证中的应用综述[J]. 计算机工程与应用, 2007, 43(36): 43-47.
[8]	屈婉霞,李暾,郭阳,杨晓东. 模型检验中抽象技术研究综述[J]. 计算机工程与应用, 2006, 42(33期): 15-19.