Optimizing Symbolic Model Checking for Constraint-Rich Models

		      Bwolen Yang, Reid Simmons,
	       Randal E. Bryant, and David R. O'Hallaron


Abstract:

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.



@techreport{bwolen-cav99-tr,
    key="invariant constraint-rich models",
    author="Bwolen Yang and Reid Simmons and Randal E. Bryant and
            David R. O'Hallaron and Bwolen Yang",
    Title="Optimizing Symbolic Model Checking for Constraint-Rich Models",
    institution	= "{School of Computer Science, Carnegie Mellon University}",
    number	= "CMU-CS-99-118",
    month       = "March",
    year	= "1999"
}