Specification Test Coverage Adequacy Criteria = Specification Test Generation Inadequacy Criteria?
Loading...
View/Download File
Persistent link to this item
Statistics
View StatisticsJournal 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.