Research on the Paul protocol checker
During my work for Compuware/Uniface,
I developed a protocol checker named
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
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:
Of, course, Paul also has a number of strong sides:
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
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.
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.