Refining Interactions in a Distributed System

Abstract

We identify a type of refinement that we call interaction refinement that is very useful in designing distributed systems. An interaction refinement step is one in which a system designer decides to implement a given ‘high-level’ interaction as a particular sequence of ‘low-level’ interactions. For example a particular high-level interaction may be specified as ‘identify-client’ involving a ‘client process’ and a ‘server process’. The designer may decide to implement this interaction as a series of low-level interactions between the two processes, with the client process first sending to the server process an id, followed by a password, and perhaps allow the client several attempts at getting the password right, etc. Here the designer is not refining the internal structure of either the client process or the server process; rather he¹ is implementing the ‘identify-client’ interaction between the two processes in terms of a sequence of ‘low-level’ communications between them. By contrast, other types of refinement that are normally considered are concerned with refining the internal structure of one or more of the processes, the interactions between the processes being taken as a given.

We motivate the idea of interaction refinement with simple and natural examples and develop a preliminary formalism that can be used to establish correctness of systems developed using interaction refinement. We also compare our work with previous work which allow one to deal with restricted kinds of interaction refinement.