Formal Models of Process Components

Peter Henderson

Department of Electronics and Computer Science
University of Southampton
SO17 1BJ, UK
Tel: (+44) 1703 593440
Fax: (+44) 1703 593045
Email: peter@ecs.soton.ac.uk

August 1997

Abstract:

The way we have come to expect computer systems to behave is that we can simply add a new component to a running system and then this new component will begin to interwork with the running system without interuption of service. Describing and validating such systems of dynamic, reconfigurable components presents a challenge for contemporary methods of formal description. Milner's pi-calculus goes some way towards addressing this issue.

In this short paper we show that the pi-calculus is particularly good at describing the behaviour of components of a distributed system. We give a pragmatic introduction to the pi-calculus and illustrate this conjecture, using an example of clients and servers collaborating on the Web. The formalisation gives us the capability to define distributable components and to formulate properties of systems built from such components. The formalisation is different from, and probably complementary to, object-oriented formulations of such components. We describe how an elementary form of model-checking, actually a curtailed state-space search, can then be used to check these properties.

My position is that, formal methods (such as the pi-calculus) are mature enough to be used in the design and validation of components of large distributed systems and that the use of such methods will lead to the better design of components and of component-oriented architectures for dynamically reconfigurable systems.

Keywords: process components, system architecture, system evolution, client-server systems, reconfigurable systems, dynamically-loaded components, pi-calculus, model checking, state-space search