摘要： 通过设置陷阱性质，用时序逻辑公式表示数据流测试的覆盖准则，将测试生成问题简化成模型检测中寻找反例的问题，自动生成满足数据流覆盖准则的类方法测试调用序列，提出了一种适用于类方法调用序列自动生成的搜索算法，并在程序模型检测器JPF上实现。算法分析和实验结果表明，该算法能生成高效的方法调用序列并明显减少测试生成代价。

关键词: 程序模型检测, 数据流测试, 类测试序列生成, Java

Abstract: The coverage criteria on data-flow test is achieved by applying trap properties and the temporal logic relationship, the problem of test sequence generation is transformed into the one of finding the counter example in model check, and an automatic generation approach of the test sequences calling methods in class is presented. A searching algorithm to generate automatically the test sequences is designed and implemented with the program model checker called Java PathFinder. The algorithm analysis and experimental results show that the presented algorithm can generate efficiently the test sequences and reduce remarkably the test generation cost.

Key words: program model check, dataflow test, generation of test sequences for classes, Java

中图分类号: 

• TP311