Issue No. 04 - July (1981 vol. 7)
J. Misra , Department of Computer Sciences, University of Texas
We present a proof method for networks of processes in which component processes communicate exclusively through messages. We show how to construct proofs of invariant properties which hold at all times during network computation, and terminal properties which hold upon termination of network computation, if network computation terminates. The proof method is based upon specifying a process by a pair of assertions, analogous to pre-and post-conditions in sequential program proving. The correctness of network specification is proven by applying inference rules to the specifications of component processes. Several examples are proved using this technique.
program proofs, Communication networks, distributed systems, message passing systems
K. Chandy and J. Misra, "Proofs of Networks of Processes," in IEEE Transactions on Software Engineering, vol. 7, no. , pp. 417-426, 1981.