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