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

View Publication

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.


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.

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},
institution = {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},
} 2017-09-13T10:49:01-04:00