Specifying Concurrent Program Modules
- 1 April 1983
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 5 (2), 190-222
- https://doi.org/10.1145/69624.357207
Abstract
A method for specifying program modules in a concurrent program is described. It is based upon temporal logic, but uses new kinds of temporal assertions to make the specifications simpler and easier to understand. The semantics of the specifications is described informally, and a sequence of examples are given culminating in a specification of three modules comprising the alternating-bit communication protocol. A formal semantics is given in the appendix.Keywords
This publication has 4 references indexed in Scilit:
- Proving Liveness Properties of Concurrent ProgramsACM Transactions on Programming Languages and Systems, 1982
- The ?Hoare logic? of concurrent programsActa Informatica, 1980
- Formal Methods in Communication Protocol DesignIEEE Transactions on Communications, 1980
- Concurrent reading and writingCommunications of the ACM, 1977