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

My work
has been strongly influenced by Tony Hoare’s CSP process algebra. In
my DPhil (

*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

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.