Creol: A Formal Executable Model of Upgradeable Distributed Objects

The Creol project targets reasoning support for evolving distributed systems based on a formal object-oriented model. This talk will discuss the main ideas behind the approach, give an intuition about the formal model, and sketch some ongoing work on system analysis. In Creol, there is no assumption about network behavior. This work intersects with network coordination in the forthcoming Credo project. If we have time, I would therefore like to end with an open discussion of how channels may be represented in the Creol setting.

The Creol model proposes programming constructs for distributed concurrent objects typed by interfaces. The approach is based on communication by asynchronous method calls and a notion of processor release points.

Processor release points allow objects to dynamically change between active and reactive behavior (client and server). The model integrates asynchronous communication and multiple inheritance, allowing method overloading and redefinition. Further, the model addresses evolution by allowing class hierarchies to be modified at run-time; new attributes, methods, and superclasses may be added to a class. The upgrade propagates asynchronously to existing objects of the class and its subclasses. The model has an operational semantics defined in rewriting logic, which is executable on the Maude platform and provides an interpreter for Creol. Techniques for reasoning about distributed concurrent objects and their evolution are under development.  

hosted by