Department of Computer Science


The aim of this project is to define a refinement strategy for UML-RT. The proposed strategy deals with classes and capsules. A capsule models an active class in the sense that, in addition to attributes and methods, its dynamic behaviour is given by a state machine. The interaction of a capsule with its environment (other capsules) is achieved via protocols. Typically, the only visible elements of a capsule are the signals introduced in the protocols to which a capsule is attached. Despite its name, the focus of UML-RT is on modelling concurrent and distributed aspects through the concept of a capsule, rather than on time aspects.

Like UML, UML-RT has no formal semantics, and therefore no proved sound refinement strategy. Our approach is to define refinement laws and techniques, for classes and capsules, based on results already consolidated in formal approaches.

The language OhCircus extends Circus with object-oriented features (classes, inheritance and dynamic binding). The other elements of OhCircus are exactly as in Circus, including the notion of a process, whose state is defined using a Z schema and whose behaviour is given by an action expressed in the CSP notation. Both Circus and OhCircus have a copy semantics. Adopting OhCircus as our semantic model, we propose transformation laws which do not involve sharing (references). Dealing with references at the semantic and at the UML-RT levels is a future research topic. One of our purposes is to preserve the style of UML-RT as much as possible. However, following a contractual approach, the characterisation of the laws needs to refer to invariants of classes and capsules, as well as to pre and postconditions of methods. The standard notation used to annotate the model with formal constraints is OCL, but we use Z for a matter of readability and for simplifying the mapping into OhCircus.


(Top of the page)

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599