优化基于模型检验的测试生成

摘要

利用模型检验器输出的反例构造测试用倒是测试自动化的一种重要手段．然而由于一个反例可能对应多个性质违背，测试生成过程中可能存在大量不必要的对模型检验器的调用，测试包也往往存在大量冗余，严重影响测试生成和测试执行性能．rn 提出一种测试生成的动态监控优化方法．用时态逻辑公式重写技术缩减测试目标集，用测试树表示缩减的但符合覆盖准则的测试包．在模型检验被选择的测试目标时，新产生的测试用例被用于重写测试目标集中的剩余目标，删除那些被测试用例覆盖的目标以避免不必要的模型检验器的调用．同时在新测试用例加入测试包时，用测试树对其进行筛选，消除冗余．