The Unified Modeling Language (UML) has become the de facto standard OO modelling notation. We have formalised much of UML and developed an underpinning semantic framework. We have used the semantic framework to develop refinement and verification rules. We have developed new notations and suggested extensions to existing notations.
In UML, class diagrams and state diagrams are graphical notations that are used to represent some aspects of object-oriented models. Class diagrams represent the static aspects, while state diagrams represent the dynamic aspects. We developed a compositional interpretation of object model and state diagrams. The interpretation supports the construction of separate theories for object instances, class managers and associations which are then combined with categorical constructions to yield a formal interpretation of the complete system. This leads to a highly modular approach, allowing reuse of generic semantic entities, resulting in an elegant, transparent semantics for individual models.
The Object Constraint Language (OCL) is a precise textual notation for expressing constraints on models such as invariants and operation specifications. We developed a formal semantics of the OCL that lays the foundation for building CASE tools that support integrity checking of whole UML models, not just the component expressed using OCL. We developed a semantics of navigation expressions as they are used in object-oriented modelling notations (e.g., UML/OCL) in widespread use by practitioners. The semantics helps to clarify some subtle issues to do with navigation expressions.
In component-based software development (CBSD), object-oriented modelling notations such as UML are being proposed as a way of providing richer specifications of components. We formulated and formalised techniques for describing, composing and performing integrity checks on components in CBSD. We proposed a high level reference model for CBSD and teased out what is meant by the terms "component", "component adaptation" and "component assembly". We developed examples of components and the transformations which can be applied to them.
Design patterns are characteristic structures of classes or objects which can be reused to achieve particular design goals in an elegant manner. We formalised design patterns as refinement transformations from a "before" system consisting of a set of classes (often a single unstructured class) into an "after" system consisting of a collection of classes organised by the pattern. We showed that patterns such as "State" and "Abstract Factory" could be proved to be formal refinements in the Object Calculus semantics of OO systems.
We provided a set of transformations on object-oriented models based on the formal semantics in the Object Calculus. We provided a systematic formal interpretation for most elements of the UML notation. This interpretation, in a structured temporal logic, enables precise analysis of the properties of these models, and the verification of one model against another. We also developed formal reasoning rules in other OO notations.
We developed a new visual notation, constraint diagrams, for precisely expressing constraints on object-oriented models, to be used in conjunction with the textual OCL. The notation is intuitive, expressive, integrates well with existing visual notations, and has a clear and unambiguous semantics. Constraint diagrams essentially provide a pictorial representation of navigation expressions, specifically the sets of objects they define, constraints on the cardinalities of and relationships between those sets. Spider diagrams emerged from work on constraint diagrams. They combine and extend Venn diagrams and Euler circles to express constraints on sets and their relationships with other sets. We produced full syntax and semantics for spider diagrams, showed that all spider diagrams are self-consistent and developed inference rules for reasoning with spider diagrams and rules for combining spider diagrams. We also developed the concept of a rooted class diagram, which captures a model from the perspective of a single object type.
We developed a formal semantics for object-oriented specification and analysis and design models, using the Object Calculus as a basis. The semantics is based on a logic of actions, real-time action logic (RAL) which integrates the object calculus and RTL to give a uniform reasoning framework for concurrent and real-time object systems.
We developed a compositional approach to the formal interpretation of type view diagrams and statecharts which led to the proposal of a notion of subsystem, which generalises the concept of object and yields an approach to system specification employing object-like encapsulation in a nested hierarchy of components. We also developed the notion of three-dimensional visual models, achieved by e.g., connecting several graphs together. We reflected on a number of aspects of the syntax and semantics of OCL, and made proposals for clarification or extension. Some of these proposals have been accepted by the developers of OCL and will be incorporated in the next version of OCL.
The precise UML group (PUML) is a group of international researchers and practitioners who share the aim of developing UML as a precise modelling language. The Amsterdam Group is working on improvements to OCL and comprises the lead designers of OCL, together with other leading OO developers and researchers. Members of the project team were instrumental in setting up both groups and also the Trusted Components Initiative.
The project consisted of teams based at Brighton and Imperial College. There is a web page for the project at http://www.biro.bton.ac.uk/biro/ containing full details of the project, with links to related sites. For more details on the project contact Dr John Howse, email John.Howse@brighton.ac.uk.