Combination model checking: Approach and a case study

Yunja Choi, Mats P.E. Heimdahl

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

1 Scopus citations

Abstract

We present combination model checking approach using a SAT-based bounded model checker together with a BDD-based symbolic model checker to provide a more efficient counter example generation process. We provide this capability without compromising the verification capability of the symbolic model checker. The basic idea is to use the symbolic model checker to determine whether or not a property holds in the model. If the property holds, we are done. If it does not, we preempt the counterexample generation and use the SAT-based model checker for this purpose. An application of the combination approach to a version of a Flight Guidance System (FGS)from Rockwell Collins, Inc. shows huge performance gain when checking a collection of several hundred properties.

Original languageEnglish (US)
Title of host publicationProceedings - 19th International Conference on Automated Software Engineering, ASE 2004
Pages354-357
Number of pages4
StatePublished - Dec 1 2004
EventProceedings - 19th International Conference on Automated Software Engineering, ASE 2004 - Linz, Austria
Duration: Sep 20 2004Sep 24 2004

Publication series

NameProceedings - 19th International Conference on Automated Software Engineering, ASE 2004

Other

OtherProceedings - 19th International Conference on Automated Software Engineering, ASE 2004
CountryAustria
CityLinz
Period9/20/049/24/04

Fingerprint Dive into the research topics of 'Combination model checking: Approach and a case study'. Together they form a unique fingerprint.

  • Cite this

    Choi, Y., & Heimdahl, M. P. E. (2004). Combination model checking: Approach and a case study. In Proceedings - 19th International Conference on Automated Software Engineering, ASE 2004 (pp. 354-357). (Proceedings - 19th International Conference on Automated Software Engineering, ASE 2004).