Accession Number : ADA188618

Title :   Research on Automatic Verification of Finite-State Concurrent Systems.

Descriptive Note : Interim rept.,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : Bryant, R E ; Clarke, E M ; Grumberg, O

PDF Url : ADA188618

Report Date : Dec 1987

Pagination or Media Count : 30

Abstract : This survey is organized as follows: Section 2 describes the syntax and semantics of the temporal logics that are used in this paper. Section 3 states the model checking problem and give an efficient algorithm for checking simple branching-time formulas. Section 4 discusses the issue of fairness and show how the algorithm of Section 3 can be extended to include fairness constraints. Section 5 demonstrates how the model checking algorithm can be used to debug a simple mutual exclusion program. Section 6 describes some alternative approaches for verifying systems of finite state concurrent process. The complexity of checking linear temporal logic formulas are analyzed and the techniques of Pnueli and Lichtenstein and Vardi and Wolper are outlined. Additional applications to circuit and protocol verification are discussed in Section 7. The paper concludes in Section 8 with a discussion of some of the important remaining research problems like the state explosion problem.

Descriptors :   *ALGORITHMS, *CIRCUITS, AUTOMATIC, DEBUGGING(COMPUTERS), EFFICIENCY, EXPLOSIONS, SYNTAX

Subject Categories : Electrical and Electronic Equipment
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE