A proof system for distributed processes

Abstract

A partial correctness proof system for Brinch Hansen's Distributed Processes (DP) is presented. Two important aspects of the system are: Proofs of individual processes of a DP program are completely isolated from each other; in particular, no assumptions are allowed in the proof of one process about the behavior of the other processes. Secondly a process is characterized by its externally visible behavior, i.e. the sequence of interactions between this process and the other processes of the program. An example demonstrates the use of the system. © 1988 Springer-Verlag.