State-Based Refinement of Distributed Systems

Michael Butler

I have a long-standing interest in refinement approaches to state-based formalisms for distributed systems.  I have worked a lot with the action system formalism originally developed by Ralph Back and Reino Kurki-Suonio in Finland.  An action system models a reactive system with guarded actions on state variables.  The important contributions are notions of refinement and decomposition which allow one to formally relate an abstract global, architecture-independent model of a system or service with a distributed design or implementation through a series of intermediate refinements.  In principle this allows one to take a purely top-down approach to development starting with a high level specification and refining this to a distributed implementation.  In my experience, refinement is never purely top down.  The reason is that it is difficult to get the abstract model precisely right.  One usually starts with an idealistic abstract model because that is easy to define.  As refinement proceeds and more architectural and environmental details are addressed it often becomes clearer how the ideal abstract model needs to be modified to reflect reality better.  This is not a weakness of the refinement approach, rather a reflection of the reality of engineering complex systems.

My work has been strongly influenced by Tony Hoare’s CSP process algebra.  In my DPhil (Oxford label for a PhD) I expanded on work by Carroll Morgan on showing the link between the CSP failures-divergence semantics and action systems:

A CSP Approach to Action Systems.

The 2 important contributions are a refinement rule which allows hidden actions to be introduced in a refinement step and a decomposition rule which allows a system model to be decomposed into parallel subsystems.  The influence of CSP is that the hidden actions correspond to event hiding in CSP and the parallel subsystems have independent state variables and only interact through synchronised message passing.  A typical use of these rules is to start with a model which abstracts away from internal communications in a system, then introduce new actions in a refinement corresponding to desired internal communications, then decompose the system using the recently introduced actions as synchronisation between the subsystems.  This is a bit different to Back’s approach where the focus is on interaction through shared variables.  Details on my approach can be found in the following paper:

Stepwise Refinement of Communicating Systems.

It turns out that there is a strong correspondence between action systems and Abrial’s B method.  Just like action systems, B models consist of state variables and operations on those variables and B makes strong use of refinement.  Early work of mine relating B with my approach can be found in this paper:

An Approach to the Design of Distributed Systems with B AMN.

I also did some work with Marina Waldén on linking B with the original Back-style action systems:

Distributed System Development in B.

The more recent Event B approach developed by Jean-Raymond Abrial is strongly influenced by refinement and decomposition in action systems.

Some further applications of state based refinement and decomposition can be found in the following papers:

On the Use of Data Refinement in the Development of Secure Communications Systems.

A System-based Approach to the Formal Development of Embedded Controllers for a Railway

Application of Event B to Global Causal Ordering for Fault Tolerant Transactions

Some Guidelines for Formal Development of Web-based Applications in B-Method.