Specification-based testing with linear temporal logic
Specification-based testing with linear temporal logic
复制标题
使用线性时序逻辑进行基于规范的测试
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Insup Lee
中科院分区：
文献类型：
--
作者：
Liqun Tan;O. Sokolsky;Insup Lee
本文考虑了基于规范的测试，其中需求是在线性时序逻辑（LTL）中给出的。所需的LTL属性必须包含系统的所有执行，这些执行通常在大小和/或长度上是无限的。我们框架的中心部分是财产覆盖度量。基于需求变化，度量标准度量一个属性被测试套件测试得有多好。我们根据从系统的所有可能执行中选择有限测试集的度量来定义覆盖率标准。我们还讨论了通过使用模型检查器的反例机制为规范测试生成测试套件的技术。通过利用生成测试的特殊结构，我们能够将无限长度的测试简化为有限长度的等效测试。我们的框架提供了一种模型检查辅助方法，该方法生成一个大小和长度有限的测试套件，用于测试实现上的线性时间属性。
This paper considers the specification-based testing in which the requirement is given in the linear temporal logic (LTL). The required LTL property must hold on all the executions of the system, which are often infinite in size and/or in length. The central piece of our framework is a property-coverage metric. Based on requirement mutation, the metric measures how well a property has been tested by a test suite. We define a coverage criterion based on the metric that selects a finite set of tests from all the possible executions of the system. We also discuss the technique of generating a test suite for specification testing by using the counterexample mechanism of a model checker. By exploiting the special structure of a generated test, we are able to reduce a test with infinite length to an equivalent one of finite length. Our framework provides a model-checking-assisted approach that generates a test suite that is finite in size and in length for testing linear temporal properties on an implementation.