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

利用模型检验器输出的反例构造测试用例是测试自动化的一种重要手段.由于一个测试用例可能覆盖多个测试目标,测试生成过程中可能存在不必要的对模型检验器的调用,测试包也往往存在大量冗余,严重影响测试性能.为此,提出一种测试生成的动态监控优化方法.在模型检验一个测试目标产生测试用例后,采用时态逻辑公式重写技术缩减测试目标集,删除那些被新测试用例覆盖的测试目标;同时,在新测试用例加入测试包时对其进行筛选,以消除冗余.实例结果表明,文中方法可有效地减少模型检验器的调用次数,缩减测试包.