Accession Number:

ADA106750

Title:

Verification of Concurrent Programs. Part I. The Temporal Framework,

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

1981-06-01

Pagination or Media Count:

63.0

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 about 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. Author

Subject Categories:

  • Theoretical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE