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 o...
Main Authors: | , , , |
---|---|
Other Authors: | |
Format: | Text |
Language: | English |
Published: |
1999
|
Subjects: | |
Online Access: | http://www.dtic.mil/docs/citations/ADA363778 http://oai.dtic.mil/oai/oai?&verb=getRecord&metadataPrefix=html&identifier=ADA363778 |
id |
ftdtic:ADA363778 |
---|---|
record_format |
openpolar |
spelling |
ftdtic:ADA363778 2023-05-15T14:00:11+02:00 Optimizing Symbolic Model Checking for Constraint-Rich Models Yang, Bwolen Simmons, Reid Bryant, Randal E. O'Hallaron, David R. CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE 1999-03 text/html http://www.dtic.mil/docs/citations/ADA363778 http://oai.dtic.mil/oai/oai?&verb=getRecord&metadataPrefix=html&identifier=ADA363778 en eng http://www.dtic.mil/docs/citations/ADA363778 APPROVED FOR PUBLIC RELEASE DTIC AND NTIS Computer Programming and Software *COMPUTER PROGRAM VERIFICATION *SYMBOLIC PROGRAMMING OPTIMIZATION SYSTEMS ANALYSIS ONLINE SYSTEMS COMPUTER AIDED DIAGNOSIS SYNTAX BDD(BINARY DECISION DIAGRAMS) *SYMBOLIC MODEL CHECKING Text 1999 ftdtic 2016-02-20T02:01:59Z 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 conjunctive-partitioning 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 Defense Technical Information Center: DTIC Technical Reports database Antarctic |
institution |
Open Polar |
collection |
Defense Technical Information Center: DTIC Technical Reports database |
op_collection_id |
ftdtic |
language |
English |
topic |
Computer Programming and Software *COMPUTER PROGRAM VERIFICATION *SYMBOLIC PROGRAMMING OPTIMIZATION SYSTEMS ANALYSIS ONLINE SYSTEMS COMPUTER AIDED DIAGNOSIS SYNTAX BDD(BINARY DECISION DIAGRAMS) *SYMBOLIC MODEL CHECKING |
spellingShingle |
Computer Programming and Software *COMPUTER PROGRAM VERIFICATION *SYMBOLIC PROGRAMMING OPTIMIZATION SYSTEMS ANALYSIS ONLINE SYSTEMS COMPUTER AIDED DIAGNOSIS SYNTAX BDD(BINARY DECISION DIAGRAMS) *SYMBOLIC MODEL CHECKING Yang, Bwolen Simmons, Reid Bryant, Randal E. O'Hallaron, David R. Optimizing Symbolic Model Checking for Constraint-Rich Models |
topic_facet |
Computer Programming and Software *COMPUTER PROGRAM VERIFICATION *SYMBOLIC PROGRAMMING OPTIMIZATION SYSTEMS ANALYSIS ONLINE SYSTEMS COMPUTER AIDED DIAGNOSIS SYNTAX BDD(BINARY DECISION DIAGRAMS) *SYMBOLIC MODEL CHECKING |
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 conjunctive-partitioning 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 |
CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE |
format |
Text |
author |
Yang, Bwolen Simmons, Reid Bryant, Randal E. O'Hallaron, David R. |
author_facet |
Yang, Bwolen Simmons, Reid Bryant, Randal E. O'Hallaron, David R. |
author_sort |
Yang, Bwolen |
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 |
publishDate |
1999 |
url |
http://www.dtic.mil/docs/citations/ADA363778 http://oai.dtic.mil/oai/oai?&verb=getRecord&metadataPrefix=html&identifier=ADA363778 |
geographic |
Antarctic |
geographic_facet |
Antarctic |
genre |
Antarc* Antarctic |
genre_facet |
Antarc* Antarctic |
op_source |
DTIC AND NTIS |
op_relation |
http://www.dtic.mil/docs/citations/ADA363778 |
op_rights |
APPROVED FOR PUBLIC RELEASE |
_version_ |
1766269175958863872 |