SAVARA is about Enterprise Modelling, and ensuring that artifacts created through the development lifecycle are verified for consistency, to ensure the original business requirements are implemented in the deployed solution. So generally we don't talk about the lower level concepts that underpin this work, its not relevant to an architect, service designer or developer - they simply want the benefits that a Testable Architecture can offer.
However, it was with great sadness that we learnt that the inventor of the Pi Calculus, Professor Robin Milner, passed away last weekend. So in honour of Robin, we wanted to describe how important Pi Calculus is for computer science in general, and more specifically to the future of the SAVARA project.
The Pi Calculus provides a concise mathematical notation for expressing all of the constructs necessary to describe the concurrent communicating behaviour of a set of participants. Having such a description enables analysis to be performed, specifically to determine if those interactions will lead to undesirable consequences, such as livelocks or deadlocks. Another important goal is to check conformance or compatibility of communication behaviour between two or more parties that are interacting. This ensures that whenever one party sends a message to another party, the recipient is in a suitable state to be able to receive and handle that message type. All of these properties are required when verifying artifacts as part of Testable Architecture.
The work we are doing with our academic colleagues, led by Dr Kohei Honda and Dr Nobuko Yoshida, in consultation with Robin, has built upon the Pi Calculus with the concept of the global model. This uses the Pi Calculus notation to describe the behaviour from a participant neutral perspective, rather than each participant's behaviour individually - equivalent to the distinction between a choreography (e.g. WS-CDL) against a process model (e.g. WS-BPEL). Using a global model enables deadlock/livelock freedom by design, assuming that certain properties are adhered to, by simply ensuring that all participants conform to the global model.
To the best of our knowledge, currently there are no products or standards that are truely based on the Pi Calculus, or leverage the type theory to detect livelocks or deadlocks. They may claim to be based on it, but in reality they are just using some of the concepts, like parallelism, recursion, choice, etc. The same is true for the first version of SAVARA, it is based on an informal 'interpretation' of this work.
However, the work we are now doing with our academic partners should deliver an enterprise tool that truely leverages the Pi Calculus to help build type safe (deadlock and livelock free) distributed systems. This will also provide a more formal basis for other reasoning and analysis, as may be needed to ensure that the solution meets all of the constraints upon it, and is not merely a heuristic approximation to the desired outcome.
The work of Robin and his colleagues in developing the Pi-Calculus informs us and guides us in what we do in SAVARA, and without his contribution SAVARA would never have existed in the first place.
Robin was always seeking real world examples to give further meaning to his research. The fruitful collaboration that started in the early days of WS-CDL, and now embodied in SAVARA, are a testament to Robin and his desire for ever more grounded and meaningful collaboration.
Gary Brown and Steve Ross-Talbot
