Life cycle Research

The protocol checker 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.

Life cycles may be compared to state diagrams as they are often drawn for objects in an object design (or, quite revolting, state charts). What life cycles add with respect to state diagrams is a precise mechanism for parameter passing and communication/synchronisation between multiple state diagrams. The parameters are an extension with respect to process algebras, but it is possible to simulate them (in an ugly way, using infinite alphabets) in plain process algebra. We are working on a proof for this statement (which is at the same time a semantics definition of life cycles).

The communication/synchronisation mechanism between life cycles is comparable to the usual communication mechanisms in process algebras such as ACP. This means that action occur jointly, without specifying an initiator. This model works quite well to declaratively specify processes, rather than the imperative programs that state charts are. To allow processes to link more flexibly, we allow multi-action on each state transition, rather than single actions.The declarative nature of life cycle communication comes with another advantage: polymorphic creation and deletion of processes.

By specifying the initial transition of a life cycle like any other transition, it becomes possible to treat the creation of a process as the result of communication. In comparison, state chart tools such as Rhapsody need to resolve to embedded C++ code in transitions to support object creation. Needless to say that C++ code is not helpful in formal analysis and checking.

Part of my PhD work is practical, setting up a life cycle system according to a particular architecture. Goals of this architecture are to allow both formal model checks and backend generation with a minimum of effort. Therefore, a generic backend describes the system-wide interactions of a composition of life cycles.

This backend is formulated in XML, and contains sufficient information for model checking. Furthermore, XML makes it straightforward to map it onto any more-specific format, all the way to an executional format.

A particular backend that we have in mind is a transactional database, where the transactions are used to model the joint work in cooperating life cycles. This database will be accessed through a generic SQL access layer from a cgi-bin script. This cgi-bin script is invoked from (also generated) HTML client forms. As a result, the path from a graphical life cycle specification in TCM to an executable, and proven correct, life cycle implementation (for example running under a http daemon and a database) is automatic.

More background on life cycles can be found here. When I have the compiler ready, I will also add a few demonstrations. For now, if you are interested, be welcome to send me an email.

If you're interested in a bit more, get the draft introduction chapter.