Model Checking, Abstraction, and Compositional Verification
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
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 01, 1993
- Accession Number
- ADA270552
Entities
People
- David E. Long
- Edmund M. Clarke
- Orna Grumberg
- Randal Bryant
- Stephen D. Brookes
Organizations
- Carnegie Mellon University