Coverage-directed test generation with model checkers: Challenges and opportunities

George Devaraj, Mats Heimdahl, Donglin Liang

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Scopus citations

Abstract

When using tools to automatically generate tests-suites from a specification, the selection of coverage criterion that guides the generation process is of imperative importance. In a previous study that evaluated test generation with model checking, we observed that although a coverage criterion may seem reasonable when instrumenting a model or code to measure the adequacy of a test suite, it may be unsuitable when formalized and used to guide the model checker to generate a test suite; the generated tests technically provide adequate coverage according to the formalization, but do so in a way that exercises only small portions of the system under study and finds few faults. Based on those results, we concluded that fully automated test-suite generation techniques must be pursued with great caution and that coverage criteria specifically addressing test-suite generation from formal specifications are needed. In this report, we attempt to better understand these concerns by evaluating several coverage criteria that bring together aspects from condition and control based criteria. We evaluate the fault finding capability of the criteria on a close to production flight guidance system and discuss the opportunities and challenges that arise from the increased use of fully automated model-based testing.

Original languageEnglish (US)
Title of host publicationProceedings of the 29th Annual International Computer Software and Applications Conference - Workshops and Fast Abstracts, COMPSAC 2005
Pages455-462
Number of pages8
Volume1
DOIs
StatePublished - Dec 1 2005
Event29th Annual International Computer Software and Applications Conference, COMPSAC 2005 - Edinburgh, Scotland, United Kingdom
Duration: Jul 26 2005Jul 28 2005

Other

Other29th Annual International Computer Software and Applications Conference, COMPSAC 2005
CountryUnited Kingdom
CityEdinburgh, Scotland
Period7/26/057/28/05

Fingerprint Dive into the research topics of 'Coverage-directed test generation with model checkers: Challenges and opportunities'. Together they form a unique fingerprint.

  • Cite this

    Devaraj, G., Heimdahl, M., & Liang, D. (2005). Coverage-directed test generation with model checkers: Challenges and opportunities. In Proceedings of the 29th Annual International Computer Software and Applications Conference - Workshops and Fast Abstracts, COMPSAC 2005 (Vol. 1, pp. 455-462). [1510066] https://doi.org/10.1109/COMPSAC.2005.66