Specification and Design of Distributed Systems

Abstract

This thesis presents a method for specifying, analysing and refining the designs of distributed systems in terms of the permissible activity across the interfaces between process components. Such a specification gives the rules for the behaviour of each process component and postpones decisions about its internal structure.

This specification method will be shown to allow important questions about the behaviour of a distributed system to be posed early in the design process: in particular, designs will be analysed with respect to termination and absence of deadlocks. The specification method can be employed to describe systems in different degrees of detail, and it is demonstrated that a specification can evolve to a stage close to realisation using a stepwise refinement method which ensures that the important properties are maintained.