Local nondeterminism in asynchronously communicating processes

Abstract

In this paper we present a simple compositional Hoare logic for reasoning about the correctness of a certain class of distributed systems. We consider distributed systems composed of processes which interact asynchronously via unbounded FIFO buffers. The simplicity of the proof system is due to the restriction to local nondeterminism in the description of the sequential processes of a system. To illustrate the usefulness of the proof system we use PVS (Prototype Verification System, see [ORS92]) to prove in a compositional manner the correctness of a heartbeat algorithm for computing the topology of a network.