|
Published Articles >> Table of Contents >> Abstract
19th IEEE International Conference on Automated Software Engineering (ASE'04)
pp. 354-357
Combination Model Checking: Approach and a Case Study
Yunja Choi, Fraunhofer Institute for Experimental Software Engineering, Germany
Mats P. E. Heimdahl, University of Minnesota, USA
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2004.10039
Send link to a friend
| 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.
|
 Additional Information
|
Citation:
Yunja Choi, Mats P. E. Heimdahl,
"Combination Model Checking: Approach and a Case Study,"
ase,
pp. 354-357,
19th IEEE International Conference on Automated Software Engineering (ASE'04),
2004
|
|
