Optimizing Symbolic Model Checking for Constraint-Rich Models
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.
BibTeX
@techreport{Yang-1999-14875,author = {B. Yang and Reid Simmons and R. Bryant and D. O'Hallaron},
title = {Optimizing Symbolic Model Checking for Constraint-Rich Models},
year = {1999},
month = {March},
institute = {Carnegie Mellon University},
address = {Pittsburgh, PA},
number = {CMU-CS-99-118},
keywords = {Symbolic model checking, Binary Decision Diagram (BDD), time-invariant constraints, redundant state-variable elimination, macro},
}