Constructing Correct Communicating Systems

Published in Volume XI, 2002, p. 46-68

Author(s): Traian MUNTEAN

Abstract

This paper presents a model for the design of correct distributed systems of communicating mobile objects. It first makes a proposal for introducing a new refinement operator for construction of complex systems that is dedicated to take into account distribution from the very specification level through all stepwise refinement process towards implementations. Our operator expresses how a whole system composed of many concurrent and communicating processes can be designed by refinement. The proposed operator is compatible with classical algorithmic and data refinements found for instance in the B Method, CSP, Action Systems and others models.

Then we introduce a diffuse-model, based on broadcasting communications instead of largely used point-to-point communication schemes. For this model we have developed a process calculus for reconfigurable communicating systems based on mobile processes which has broadcast as unique basic exchange mechanism, b$\pi$ calculus 15,16?. We have provided a full operational semantics for this calculus and we illustrate its expressiveness through some examples taken from complementary classes of applications (built correct exchange mechanisms for messages in reconfigurable networks, checking for inconsistencies of transactions between mobile distributed processes). We have proposed three behavioural equivalencies for reasoning about such systems, namely, barbed equivalence, step-equivalence and labelled bisimilarity. An important result 15?, is that all these relations coincide, providing different ways to study the equivalence/non-equivalence of two systems and also a further refinement model for broadcasting systems.