This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
July 1981 (vol. 7 no. 4)
pp. 417-426
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.
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
Usage of this product signifies your acceptance of the Terms of Use.