Optimizing Symbolic Model Checking for Constraint-Rich Models

This paper presents optimizations for verifying systems with complex timeinvariant 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 opt...

Full description

Bibliographic Details
Main Authors: Bwolen Yang, Reid Simmons, Randal E. Bryant, David R. O'hallaron
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published: Springer 1999
Subjects:
symbolic model checking
Binary Decision Diagram (BDD
timeinvariant constraints
redundant state-variable elimination
Antarctic
Antarc*
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.35.811
http://www-cgi.cs.cmu.edu/afs/cs.cmu.edu/usr/bwolen/www/papers/cav99-tr.ps
Description
Summary:This paper presents optimizations for verifying systems with complex timeinvariant 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. 1 Introduction To Appear in CAV'99. This paper presents techniques for using symbolic model checking to automatically verify a class of real-world applications that have many time-invariant constraints.

Similar Items