1 Background

This short paper attempts to bridge the gap between contemporary methods of formal description and contemporary methods of system design. Modern computer systems are large and necessarily built from components. In particular, we have come to expect that new components can be added to an existing system without undue disturbance to the services which the existing system provides. This is particularly true when it comes to systems deployed on the Web, where technologies such as Java have begun to make commonplace the development of dynamically reconfigurable distributed systems. Such systems present a challenge for contemporary methods of formal description. One answer to (at least part of) this problem is offered by the pi-calculus, a process algebra developed by Robin Milner [Mil91]. In this short paper we will investigate application of this method of formal description to the design of dynamically reconfigurable distributed systems.

My view of formal methods is that their use at the design stage is made more effective if a tool is available to check properties of specifications as they are produced. I personally favour executable formal models [Hen86,Gra96] but this position is a matter of taste. We will however discuss how we have used executable formal models based on the pi-calculus to check properties of components described in that language.

An earlier method of component description which we produced [Hen91], where components were viewed as providers of services (which should in some sense match when components are plugged together) lacked the formal basis which the pi-calculus can now supply. More recently, we have developed an informal method of describing complex systems built from components [Hen95]. This method has acquired some popularity, particularly in the organisation which sponsored the research (ICL). But again, that method lacked a formal underpinning which I now hope the pi-calculus will supply. This short paper goes some way towards realising this ambition.