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