Abstraction and Compositionality for the Verification of Infinite-State Reactive Systems

Abstract

We describe several techniques for verifying infinite-state systems via finite-state abstractions. Diagrams are top-down property-driven abstractions, which are especially suited for compositional, assume-guarantee reasoning. Predicate abstraction uses a bottom-up approach for generating abstractions; invariant generation techniques are applied to automatically generate the required predicates. Extended finite-state abstractions allow inclusion of extra information produced by the deductive abstraction, which can be used by the model checker to reduce the number of spurious counterexamples. These methods have been or currently are being implemented in the Stanford Temporal Prover. The methods have been applied in the analysis of a medical device.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 01, 2001
Accession Number
ADA398862

Entities

People

  • Henny Sipma
  • Zohar Manna

Organizations

  • Stanford University

Tags

Communities of Interest

  • Biomedical

DTIC Thesaurus Topics

  • Abstracts
  • Artificial Intelligence
  • Automata
  • Classification
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Demographic Cohorts
  • Hybrid Systems
  • Language
  • Military Research
  • Scientists
  • Standards
  • Theoretical Computer Science
  • Universities
  • Verification

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computer Vision.
  • Mathematical Modeling and Probability Theory.