中文摘要：

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

英文摘要：

Constructing test cases from the counterexamples generated by a model checker is an important means to perform test automation. The fact that multiple goals in the set of test goals may be covered by the same counterexample, however, leads to some redundant calls to the model checker in the process of test generation, and redundant test cases in test suite such that decrease seriously testing performance. An optimization approach to test generation based on dynamic monitoring is proposed. After a new test case is generated by model checking for a selected test goal, temporal logic formula rewriting technique is employed to reduce the set of test goals, those goals covered by the new test case are picked out. Meanwhile, the new test ease is winnowed by the test suite to eliminate the redundancy when it is merged into the test suite. Experimental results illustrate that the proposed method is effective for reducing the numbers of calls to the model checker and the test suite.