A Refinement of Communicating Processes

Abstract

The programming of MIMD multiprocessors requires to design processes to be mapped on the nodes of the architecture and communicating by message passing. The aim of this paper is to give a contribution for a rationalized design of such programs from formal specifications. We introduce a refinement calculus of parallel specifications in which processes refine the safety properties and communications refine the liveness one. Rules and the stepwise technique are illustrated by the shortest path problem.