抽象精化和可满足性结合的EFSM模型测试用例优化生成  

Optimized Test Cases Generation for EFSM Model Combining Abstraction Refinement and Satisfiability

作　　者：陆公正[1,2] 缪淮扣[2,3] 

机构地区：[1]苏州市职业大学计算机工程学院,江苏苏州215104 [2]上海大学计算机工程与科学学院,上海200072 [3]上海市计算机软件测评重点实验室,上海201112

出　　处：《计算机学报》2016年第11期2236-2252,共17页Chinese Journal of Computers

基　　金：国家自然科学基金(61170044;61572306);上海市重点学科建设项目基金(J50153);苏州市职业大学预研基金(SVU2015YY01)资助~~

摘　　要：基于模型的测试是测试自动化的重要手段,通常采用模型检验技术从系统模型自动生成测试用例集,但生成的测试用例集往往存在冗余,这将影响测试用例执行的性能和成本.该文以扩展有限状态机(Extended Finite Machine,EFSM)为建模工具,根据公式簇建立状态等价关系,构建抽象模型,采用模型检验技术生成抽象反例(测试用例);给出了判定生成的抽象反例是否为伪反例的方法;采用反例引导的方法精化抽象模型,删除伪反例;最后,使用我们之前提出的基于可满足性的测试用例生成方法在抽象模型上生成约简的测试用例集.实验表明:该方法的测试用例数目约简比例最高达76%(警报侦测组件EFSM),总长度约简比例最高达68%(ATM EFSM),同时不会影响测试用例集的迁移覆盖率和查错能力.Model based testing is an important means of test automation.Usually,Test Suite can be generated automatically from system model using model checking technique.It generates one test case for each test goal,and the final test suite usually has redundancy which will affect the performance and cost of the test execution.Moreover,the cost of calling model checker is expensive.In this paper,Extended Finite State Machine(EFSM)was used to model the system,then equivalence relation was defined according to formula clusters consist of the variables occurring in the predicates,then an abstraction model can be built,and the counterexamples(test cases)were generated from the abstraction model using model checking.The method deciding whether a counterexample is a spurious counterexample was proposed.If it is a spurious counterexample,a counterexample-guided abstraction refinement framework was used to refine the abstraction model.Finally,we got the optimized test suite using the test case generation method based on satisfiability we proposed before,which reduced the redundant test cases during test case generation.This method can not only optimize the test case generation,it also decreases the number of calling model checker.The experimental results show that the method proposed in this paper can reduce the number of test suite up to 76%(Alarm Detection EFSM)and its total length up to 68%(ATM EFSM).Meanwhile,it will not affect the transition coverage rate and error detection ability.

关 键 词：测试用例约简 扩展有穷状态机 公式簇 抽象 反例引导的精化 可满足性 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]