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: | , , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
Springer
1999
|
Subjects: | |
Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.804 http://www.cs.cmu.edu/afs/cs.cmu.edu/user/bwolen/www/papers/cav99.ps |
id |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.34.804 |
---|---|
record_format |
openpolar |
spelling |
ftciteseerx:oai:CiteSeerX.psu:10.1.1.34.804 2023-05-15T13:40:22+02:00 Optimizing Symbolic Model Checking for Constraint-Rich Models Bwolen Yang Reid Simmons Randal E. Bryant David R. O'Hallaron The Pennsylvania State University CiteSeerX Archives 1999 application/postscript http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.804 http://www.cs.cmu.edu/afs/cs.cmu.edu/user/bwolen/www/papers/cav99.ps en eng Springer http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.804 http://www.cs.cmu.edu/afs/cs.cmu.edu/user/bwolen/www/papers/cav99.ps Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.cs.cmu.edu/afs/cs.cmu.edu/user/bwolen/www/papers/cav99.ps text 1999 ftciteseerx 2016-01-07T23:51:44Z 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. Text Antarc* Antarctic Unknown Antarctic |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
ftciteseerx |
language |
English |
description |
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. |
author2 |
The Pennsylvania State University CiteSeerX Archives |
format |
Text |
author |
Bwolen Yang Reid Simmons Randal E. Bryant David R. O'Hallaron |
spellingShingle |
Bwolen Yang Reid Simmons Randal E. Bryant David R. O'Hallaron Optimizing Symbolic Model Checking for Constraint-Rich Models |
author_facet |
Bwolen Yang Reid Simmons Randal E. Bryant David R. O'Hallaron |
author_sort |
Bwolen Yang |
title |
Optimizing Symbolic Model Checking for Constraint-Rich Models |
title_short |
Optimizing Symbolic Model Checking for Constraint-Rich Models |
title_full |
Optimizing Symbolic Model Checking for Constraint-Rich Models |
title_fullStr |
Optimizing Symbolic Model Checking for Constraint-Rich Models |
title_full_unstemmed |
Optimizing Symbolic Model Checking for Constraint-Rich Models |
title_sort |
optimizing symbolic model checking for constraint-rich models |
publisher |
Springer |
publishDate |
1999 |
url |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.804 http://www.cs.cmu.edu/afs/cs.cmu.edu/user/bwolen/www/papers/cav99.ps |
geographic |
Antarctic |
geographic_facet |
Antarctic |
genre |
Antarc* Antarctic |
genre_facet |
Antarc* Antarctic |
op_source |
http://www.cs.cmu.edu/afs/cs.cmu.edu/user/bwolen/www/papers/cav99.ps |
op_relation |
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.34.804 http://www.cs.cmu.edu/afs/cs.cmu.edu/user/bwolen/www/papers/cav99.ps |
op_rights |
Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
_version_ |
1766132918401368064 |