Research on the Paul protocol checker

During my work for Compuware/Uniface, I developed a protocol checker named Paul which is available for free download, together with the Santa demonstration package. The name stands for Protocol Assuring Universal Language. The aim of Paul is to verify that a number of objects, which each are specified separately, communicate well together. Paul captures message passing and is aware of who takes initiatives (usually the client object, but it is possible to model the server's influence through return values).

We have an interesting little exercise with protocol specification online for your pleasure. This checker is able to check most statically structured networks of objects, and its model has been specialised to apply to the specific wishes for Uniface's evolving component modelling environment.

The Paul tool is limited in a number of ways:

• It cannot deal with runtime creation/deletion of objects.
• It assumes an imperative language, which forces the protocol designer to take aspects of computation into account which may be too detailed for some purposes.

• It has thus far proven to capture object oriented models quite well. This is partially due to the general nature of the underlying model which identifies several distinct protocols.
• Most (if not all) comparable checkers build a global process structure comprising of all parts of a program woven together. This makes it impossible to deal with varying structures caused by such real-world phenomena as unconstrained object creation and component composition. The locality built into Paul means that the Paul checker only looks at small parts of the design in turn, and the language concepts and the checks are designed to ensure global correctness if all local checks succeed.
• It is built to support component integration. That is made possible by distinguishing a separate client and server protocol on every interaction link; these can be severed due to the locality.
• It has chances of being extended to include multiplicity on associations, and thus ways to deal with creation and deletion of objects.
  
  Note: This extension will not be made to Paul; it may however be incorporated in my current research instead.

Current research: Paul was my first approach to practical checking of object systems. To overcome its lack of dynamicity (at least in the distributed version) and to turn to declarative models, I decided to build a new process language, which I call Life cycles.