Optimizing Symbolic Model Checking for Constraint-Rich Models

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

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1999
Accession Number
ADA363778

Entities

People

  • Bwolen Yang
  • David R. O'hallaron
  • Randal Bryant
  • Reid Simmons

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • Autonomy
  • C4I
  • Materials and Manufacturing Processes
  • Space

DTIC Thesaurus Topics

  • Algorithms
  • C Programming Language
  • Complex Systems
  • Computations
  • Computer Programming
  • Computer Science
  • Computers
  • Deep Space
  • Extraction
  • Language
  • Optimization
  • Programming Languages
  • Removal
  • Spacecraft
  • Test And Evaluation
  • Transitions
  • Verification

Fields of Study

  • Computer science

Readers

  • Adaptive Control and Estimation with Uncertainty in Dynamic Systems.
  • Applied Combinatorial Optimization and Logic Circuit Design.
  • Materials Science.

Technology Areas

  • AI & ML
  • AI & ML - Information Retrieval
  • AI & ML - Machine Learning Algorithms
  • Autonomy
  • Autonomy - Autonomous System Control
  • Space
  • Space - Spacecraft Maneuvers