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...

Full description

Bibliographic Details
Main Authors: Yang, Bwolen, Simmons, Reid, Bryant, Randal E., O'Hallaron, David R.
Other Authors: CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE
Format: Text
Language:English
Published: 1999
Subjects:
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
Antarctic
Antarc*
Online Access:http://www.dtic.mil/docs/citations/ADA363778
http://oai.dtic.mil/oai/oai?&verb=getRecord&metadataPrefix=html&identifier=ADA363778
Description
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 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.

Similar Items