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 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.