Proofs of Networks of Processes

TLDR

We present a proof method for networks of processes that communicate solely via messages. The method specifies each process with a pair of assertions like pre‑ and post‑conditions and proves network correctness by applying inference rules to component specifications. We construct proofs of invariant and terminal properties for networks and demonstrate the technique on several examples.

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.