posted on 2006-01-01, 00:00authored byBwolen Yang, Reid Simmons, Randal E. Bryant, David R. O’Hallaron
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 conjunctivepartitioning
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.