Report Number: CS-TR-81-836
Institution: Stanford University, Department of Computer Science
Title: Verification of concurrent programs, Part I: The temporal
Author: Manna, Z ohar
Author: Pnueli, Amir
Date: June 1981
Abstract: This is the first in a series of reports describing the
application of temporal logic to the specification and
verification of concurrent programs.
We first introduce temporal logic as a tool for reasoning
about sequences of states. Models of concurrent programs
based both on transition graphs and on linear-text
representations are presented and the notions of concurrent
and fair executions are defined.
The general temporal language is then specialized to reason
aboaut those execution sequences that are fair computations
of a concurrent program. Subsequently, the language is used
to describe properties of concurrent programs.
The set of interesting properties is classified into
invariance (safety), eventuality (liveness), and precedence
(until) properties. Among the properties studied are: partial
correctness, global invariance, clean behavior, mutual
exclusion, absence of deadlock, termination, total
correctness, intermittent assertions, accessibility,
responsiveness, safe liveness, absence of unsolicited
response, fair responsiveness, and precedence.
In the following reports of this series, we will use the
temporal formalism to develop proof methodologies for proving
the properties discussed here.