1;3409;0c Specifying Concurrent Program Modules

Specifying Concurrent Program Modules

ACM Transactions on Programming Languages and Systems, vol. 5, no. 2, 1983
Pages: 190-222DOI: 10.1145/69624.357207



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