Proofs of Networks of Processes

The proof method is based upon specifying a process by a pair of assertions, analogous to pre-and post-conditions in sequential program proving, and the correctness of network specification is proven by applying inference rules to the specifications of component processes.

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.