A Model and Temporal proof system for Networks of Processes

Abstract

An approach is presented for modeling networks of processes that communicate exclusively through message passing. A process (or a network) is defined by its set of possible behaviors, where each behavior is an abstraction of an infinite execution sequence of the process. The resulting model is simple and modular and facilitates information hiding. It can describe both synchronous and asynchronous networks. It supports recursively-defined networks and can characterize liveness properties such as progress of inputs and outputs, termination, and deadlock. A sound and complete temporal proof system based on the model is presented. It is compositional - a specification of a network is formed naturally from specifications of its components.