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 https://kilthub.cmu.edu/articles/Optimizing_Symbolic_Model_Checking_for_Constraint-Rich_Models/6608210 |
id |
ftdatacite:10.1184/r1/6608210 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.1184/r1/6608210 2023-08-27T04:05:52+02:00 Optimizing Symbolic Model Checking for Constraint-Rich Models ... Bwolen Yang Simmons, Reid Bryant, Randal E. O’Hallaron, David R. 2006 https://dx.doi.org/10.1184/r1/6608210 https://kilthub.cmu.edu/articles/Optimizing_Symbolic_Model_Checking_for_Constraint-Rich_Models/6608210 unknown Carnegie Mellon University In Copyright http://rightsstatements.org/vocab/InC/1.0/ 89999 Information and Computing Sciences not elsewhere classified FOS Computer and information sciences Text article-journal Journal contribution ScholarlyArticle 2006 ftdatacite https://doi.org/10.1184/r1/6608210 2023-08-07T14:24:23Z 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. ... Other Non-Article Part of Journal/Newspaper Antarc* Antarctic DataCite Metadata Store (German National Library of Science and Technology) Antarctic |
institution |
Open Polar |
collection |
DataCite Metadata Store (German National Library of Science and Technology) |
op_collection_id |
ftdatacite |
language |
unknown |
topic |
89999 Information and Computing Sciences not elsewhere classified FOS Computer and information sciences |
spellingShingle |
89999 Information and Computing Sciences not elsewhere classified FOS Computer and information sciences Bwolen Yang Simmons, Reid Bryant, Randal E. O’Hallaron, David R. Optimizing Symbolic Model Checking for Constraint-Rich Models ... |
topic_facet |
89999 Information and Computing Sciences not elsewhere classified FOS Computer and information sciences |
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. ... |
format |
Other Non-Article Part of Journal/Newspaper |
author |
Bwolen Yang Simmons, Reid Bryant, Randal E. O’Hallaron, David R. |
author_facet |
Bwolen Yang Simmons, Reid Bryant, Randal E. O’Hallaron, David R. |
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 |
Carnegie Mellon University |
publishDate |
2006 |
url |
https://dx.doi.org/10.1184/r1/6608210 https://kilthub.cmu.edu/articles/Optimizing_Symbolic_Model_Checking_for_Constraint-Rich_Models/6608210 |
geographic |
Antarctic |
geographic_facet |
Antarctic |
genre |
Antarc* Antarctic |
genre_facet |
Antarc* Antarctic |
op_rights |
In Copyright http://rightsstatements.org/vocab/InC/1.0/ |
op_doi |
https://doi.org/10.1184/r1/6608210 |
_version_ |
1775346602833084416 |