Coverage based test-case generation using model checkers

Research output: Contribution to conferencePaper

129 Scopus citations

Abstract

This paper presents a method for automatically generating test cases to structural coverage criteria. We show how a model checker can be used to automatically generate complete test sequences that will provide a predefined coverage of any software development artifact that can be represented as a finite state model. Our goal is to help reduce the high cost of developing test cases for safety-critical software applications that require a certain level of coverage for certification, for example, safety-critical avionics systems that need to demonstrate MC/DC (modified condition and decision) coverage of the code. We define a formal framework suitable for modeling software artifacts, like, requirements models, software specifications, or implementations. We then show how various structural coverage criteria can be formalized and used to make a model checker provide test sequences to achieve this coverage. To illustrate our approach, we demonstrate, for the first time, how a model checker can be used to generate test sequences for MC/DC coverage of a small case example.

Original languageEnglish (US)
Pages83-91
Number of pages9
StatePublished - Jan 1 2001
Event8th Annual IEEE International Conference on the Workshop on the Engineering of Computer Based Systems - Washington, DC, United States
Duration: Apr 17 2001Apr 20 2001

Other

Other8th Annual IEEE International Conference on the Workshop on the Engineering of Computer Based Systems
CountryUnited States
CityWashington, DC
Period4/17/014/20/01

Fingerprint Dive into the research topics of 'Coverage based test-case generation using model checkers'. Together they form a unique fingerprint.

Cite this