Name
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 showthat 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. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48683-6_29 | CAV |
Keywords | Field | DocType |
new optimizations,complex time-invariant constraint,verifying system,constraint-rich models,constraint-rich problem,antarctic meteorite explorer,bdd-based macro-extraction,optimizing symbolic model checking,conjunctivepartitioning algorithm,nomad robot,constraint-rich system,nasa deep space,symbolic programming,optimization,syntax,systems analysis | Model checking,Computer science,Physical system,Systems analysis,Algorithm,Formal specification,Finite-state machine,Theoretical computer science,Symbolic programming,NASA Deep Space Network,Distributed computing,Formal verification | Conference |
ISBN | Citations | PageRank |
3-540-66202-2 | 9 | 1.12 |
References | Authors | |
13 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bwolen Yang | 1 | 123 | 9.89 |
| Reid G. Simmons | 2 | 4114 | 562.20 |
| Randal E. Bryant | 3 | 9204 | 1194.64 |
| David R. O'hallaron | 4 | 1243 | 126.28 |