Optimizing Symbolic Model Checking for Constraint-Rich Models

B. Yang, Reid Simmons, R. Bryant, and D. O'Hallaron
tech. report CMU-CS-99-118, Computer Science Department, Carnegie Mellon University, March, 1999


Download
  • Adobe portable document format (pdf) (136KB)
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.

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.

Keywords
Symbolic model checking, Binary Decision Diagram (BDD), time-invariant constraints, redundant state-variable elimination, macro

Notes
Number of pages: 25

Text Reference
B. Yang, Reid Simmons, R. Bryant, and D. O'Hallaron, "Optimizing Symbolic Model Checking for Constraint-Rich Models," tech. report CMU-CS-99-118, Computer Science Department, Carnegie Mellon University, March, 1999

BibTeX Reference
@techreport{Simmons_1999_2651,
   author = "B. Yang and Reid Simmons and R. Bryant and D. O'Hallaron",
   title = "Optimizing Symbolic Model Checking for Constraint-Rich Models",
   booktitle = "",
   institution = "Computer Science Department",
   month = "March",
   year = "1999",
   number= "CMU-CS-99-118",
   address= "Pittsburgh, PA",
}