Computer Science Department
School of Computer Science, Carnegie Mellon University
Optimizing Symbolic Model Checking for Constraint-Rich Models
Bwolen Yang, Reid Simmons, Randal E. Bryant, David R. O'Hallaron
March 1999
A condensed version of this technical report will appear in
Proceedings of the International Conference on Computer-Aided
Verification, Trento, Italy, July 1999.
CMU-CS-99-118.ps
CMU-CS-99-118.pdf
This paper presents optimizations for verifying systems with
complex time-invariant constraints. These constraints arise
naturally from modeling physical systems, e.g., in
establishing the relationship between different components
in a system. To verify constraint-rich systems, we propose
two new optimizations. The first optimization is a simple,
yet powerful, extension of the conjunctive-partitioning
algorithm. The second is a collection of BDD-based
macro-extraction and macro-expansion algorithms to remove
state variables. We show that these two optimizations are
essential in verifying constraint-rich problems; in
particular, this work has enabled the verification of fault
diagnosis models of the Nomad robot (an Antarctic meteorite
explorer) and of the NASA Deep Space One spacecraft.
25 pages
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu
School of Computer Science homepage