Verification system for partial correctness of communicating sequential processes

The communication sequential processes (CSP) system proposed by Hoare is a model for parallel computation which has no shared variables and performs information exchange and synchronization among processes by means of communication commands. In this paper we first consider a set of states for the given CSP program. Using a binary relation on the set, we introduce a semantics representing only the input‐output relations of the CSP program. Based on this semantics, we propose an axiom system which serves to verify the partial correctness of CSP. We prove the soundness of this axiom system. The axiom system proposed in this paper differs from the previously proposed systems in the following aspects. In our system, the inferences proceed simultaneously over all processes. On the other hand, conventional methods adopt a procedure wherein a given property is first proved independently for each process and it is then shown that a certain condition holds among the processes. Our method of proof is a more direct representation of the actual execution of process.