Accession Number:

ADA270552

Title:

Model Checking, Abstraction, and Compositional Verification

Descriptive Note:

Doctoral thesis

Corporate Author:

CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Report Date:

1993-07-01

Pagination or Media Count:

221.0

Abstract:

Because of the difficulty of adequately simulating large digital designs, there has been a recent surge of interest in formal verification, in which a mathematical model of the design is proved to satisfy a precise specification. Model checking is one formal verification technique. It consists of checking that a finite-state model of the design satisfies a specification given in temporal logic, which is a logic that can express properties involving the sequencing of events in time. One of the main drawbacks of model checking is the state explosion problem. This problem occurs in systems composed of multiple process executing in parallel the size of the state space generally grows exponentially with the number of components. This thesis considers two methods for avoiding the state explosion problem in the context of model checking compositional verification and abstraction

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE