Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria?

Loading...
Thumbnail Image

Persistent link to this item

Statistics
View Statistics

Journal Title

Journal ISSN

Volume Title

Title

Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria?

Published Date

2004

Publisher

Type

Report

Abstract

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.

Keywords

Description

Associated research group: Critical Systems Research Group

Related to

Replaces

License

Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Proceedings of the 8th IEEE High Assurance in Systems Engineering Workshop

Suggested citation

Heimdahl, Mats; George, Devaraj; Weber, Robert. (2004). Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria?. Retrieved from the University Digital Conservancy, https://hdl.handle.net/11299/217328.

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.