An introduction to assertional reasoning for concurrent systems
- 1 September 1993
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Computing Surveys
- Vol. 25 (3) , 225-262
- https://doi.org/10.1145/158439.158441
Abstract
This is a tutorial introduction to assertional reasoning based on temporal logic. The objective is to provide a working familiarity with the technique. We use a simple system model and a simple proof system, and we keep to a minimum the treatment of issues such as soundness, completeness, compositionality, and abstraction. We model a concurrent system by a state transition system and fairness requirements. We reason about such systems using Hoare logic and a subset of linear-time temporal logic, specifically, invariant assertions and leads-to assertions. We apply the method to several examples.Keywords
This publication has 33 references indexed in Scilit:
- Stepwise refinement of parallel algorithmsScience of Computer Programming, 1990
- A method for solving synchronization problemsScience of Computer Programming, 1989
- The derivation of graph marking algorithms from distributed termination detection protocolsScience of Computer Programming, 1988
- Adequate proof principles for invariance and liveness properties of concurrent programsScience of Computer Programming, 1984
- An HDLC protocol specification and its verification using image protocolsACM Transactions on Computer Systems, 1983
- Derivation of a termination detection algorithm for distributed computationsInformation Processing Letters, 1983
- An assertional correctness proof of a distributed algorithmScience of Computer Programming, 1982
- Proving Liveness Properties of Concurrent ProgramsACM Transactions on Programming Languages and Systems, 1982
- Ten Years of Hoare's Logic: A Survey—Part IACM Transactions on Programming Languages and Systems, 1981
- Verification of link-level protocolsBIT Numerical Mathematics, 1981