Optimizing Symbolic Model Checking for Constraint-Rich Models ...
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 op...
| Main Authors: | , , , |
|---|---|
| Format: | Other Non-Article Part of Journal/Newspaper |
| Language: | unknown |
| Published: |
Carnegie Mellon University
2006
|
| Subjects: | |
| Online Access: | https://dx.doi.org/10.1184/r1/6608210.v1 https://kilthub.cmu.edu/articles/Optimizing_Symbolic_Model_Checking_for_Constraint-Rich_Models/6608210/1 |
| Summary: | 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. ... |
|---|