Specification test coverage adequacy criteria = specification test generation inadequacy criteria
Specification test coverage adequacy criteria = specification test generation inadequacy criteria
复制标题
规范测试覆盖充分性标准 = 规范测试生成不足性标准
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Robert J. Weber
中科院分区：
文献类型：
--
作者：
M. Heimdahl;G. Devaraj;Robert J. Weber
成功的分析技术模型检测可以被用作测试用例生成技术，从形式化模型生成测试。当使用模型检查器生成测试用例时，我们利用模型检查器的见证（或反例）生成功能来构建测试用例。测试准则被表示为时间属性，并且针对这些属性生成的见证迹被实例化以创建满足准则的完整测试序列。在这份报告中，我们描述了一个实验，我们调查的故障发现能力的测试套件生成提供三个规格覆盖度量文献中提出的（状态，过渡，决策覆盖）。我们的研究结果表明，虽然覆盖率似乎是合理的，以衡量充分的测试套件，他们是不合适的，当用来生成测试套件。简而言之，生成的测试序列在技术上提供了足够的覆盖率，但这样做的方式是只测试正式模型的一小部分。我们的结论是，自动化测试技术必须非常谨慎地进行，并需要新的覆盖标准，针对正式规范。
The successful analysis technique model checking can be employed as a test-case generation technique to generate tests from formal models. When using a model checker for test case generation, we leverage the witness (or counter-example) generation capability of model-checkers for constructing test cases. Test criteria are expressed as temporal properties and the witness traces generated for these properties are instantiated to create complete test sequences, satisfying the criteria. In this report we describe an experiment where we investigate the fault finding capability of test suites generated to provide three specification coverage metrics proposed in the literature (state, transition, and decision coverage). Our findings indicate that although the coverage may seem reasonable to measure the adequacy of a test suite, they are unsuitable when used to generate test suites. In short, the generated test sequences technically provide adequate coverage, but do so in a way that tests only a small portion of the formal model. We conclude that automated testing techniques must be pursued with great caution and that new coverage criteria targeting formal specifications are needed.