The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - July (1981 vol.7)
pp: 417-426
J. Misra , Department of Computer Sciences, University of Texas
ABSTRACT
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.
INDEX TERMS
program proofs, Communication networks, distributed systems, message passing systems
CITATION
J. Misra, K.M. Chandy, "Proofs of Networks of Processes", IEEE Transactions on Software Engineering, vol.7, no. 4, pp. 417-426, July 1981, doi:10.1109/TSE.1981.230844
24 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool