2.2 Why make Formal Models

It is not common practice to make formal models of systems especially if these systems are large. The reason is that formal methods are expensive to apply and usually an engineering project doesn't have the necessary resources. But there are good reasons for making formal models of large systems. These include the prospects for validation of the design, the ability it gives us to devise a resilient architecture for the system and also the ability it gives us to consider alternative designs and architectures.

The apparent mismatch between formal models and large scale systems may be more of an illusion than a reality. Large systems are built from components. Formal descriptions of components and of the methods for combining components into systems need not be large, just because the components and systems they describe are large. The trick is to apply these methods at a system level.

It seems that process algebras have the necessary concepts to be able to describe systems at a system level. Especially when those systems have concurrent behaviour and where they are intended to be distributed across a network. To support this conjecture we will introduce the pi-calculus (in a pragmatic way) and use it to describe systems built from clients and servers. The intention is that these descriptions are formal models of the behaviour of such components in a distributed environment such as that provided by the Web.

At the end of this section we will briefly discuss the methods we have used to validate the models we are about to present. These methods include execution and model checking. Finally, we will discuss what research needs to be done next in order to further develop these ideas.