The Community for Technology Leaders
2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011) (2004)
Linz, Austria
Sept. 20, 2004 to Sept. 24, 2004
ISSN: 1068-3062
ISBN: 0-7695-2131-2
pp: 354-357
Yunja Choi , Fraunhofer Institute for Experimental Software Engineering
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.
INDEX TERMS
Computer aided software engineering, Counting circuits, Data structures, Boolean functions, Software engineering, NASA, Computer science, Performance gain, Usability, Acceleration
CITATION
Yunja Choi, M.P.E. Heimdahl, "Combination model checking: approach and a case study", 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), vol. 00, no. , pp. 354-357, 2004, doi:10.1109/ASE.2004.1342763
87 ms
(Ver 3.3 (11022016))