Throughout the project we adapted the project plan to ensure that we were up-to-date with developments. The project originally concentrated on Syntropy, a method of developing object systems that embodies representative concepts and techniques, as the approach to object-oriented development mentioned in objective 1. However, it soon became clear that the Unified Modeling Language (UML) was becoming the de facto standard OO modelling notation. A key feature of the project was to formalise the technology in current use, so, a decision was taken to formalise UML instead of Syntropy.
The project consisted of two teams based at Brighton and Imperial College. Regular technical meetings were held to check progress and these fostered shared understanding. Good relations existed between the two teams and this resulted in a number of shared papers. 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.
In the following three sections, we describe the three main strands of the research under the headings: 1. Semantics, 2. Transformations, Refinement and Verification, and 3. Language and Extensions. In section 4, we describe other related work undertaken by the project team and in Section 5, we describe ongoing and future work.
1.1 Categorical framework
We developed a compositional interpretation of object model and statechart diagrams as used in Object-Oriented Analysis and Design notations. 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. We compared the use of state attributes to abstractly interpret history with temporal axioms governing behaviours and contrast the logical notion of locality with object-oriented data encapsulation. We considered the interpretation of statecharts partitioning the overall statespace and defining transitions between partitions and gave a formal interpretation to event parameters, filters, preconditions and postconditions. We observed that some features of the notations are not amenable to this systematic modular interpretation (1, 2, 4).
1.2 Element theories
This subsection details work undertaken on giving semantics to specific elements of UML. 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. 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, modular approach to the semantics of object-oriented models expressed using class diagrams, state diagrams and operation specifications. This approach to the semantics could easily be applied to other, similar notation sets. An important aspect of this approach is to treat every component of a model, down to the level of individual diagram elements, as distinct semantic entities. The semantics of a model or part of a model is then the composition of the semantic entities corresponding to the individual model elements. This leads to a highly modular approach, allowing reuse of generic semantic entities, resulting in an elegant, transparent semantics for individual models. The fine-grained modularity promises to support the extraction and manipulation of different "views" of a model. The composition of model elements supported by the semantics promises to underpin the development of systems from reusable components. We developed a formal semantics of the OCL expressed in Larch. This approach is based on mapping each OCL type to a Larch sort, and each OCL operation to a function specified in Larch. This semantics lays the foundation for building CASE tools that support integrity checking of whole UML models, not just the component expressed using OCL (13, 14).
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. Much more so than in bespoke software development, this requires a high level of precision coupled with sufficient expressive power. Expressive power is delivered by adding textual annotations, such as invariants, preconditions and postconditions, to diagrams. Navigation expressions, which identify collections of objects by navigating associations, are central to making such annotations precise. 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 (15).
1.3 Compositionality
In this strand of work 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" (23). We developed examples of components and the transformations which can be applied to them (24, 33).
We developed the concept of a rooted class diagram, which captures a model from the perspective of a single object type. Every property or invariant in a rooted class diagram is implicitly universally quantified over the set of objects of the root type. The two mappings which make up an association are shown separately in the diagrams of the types to which they belong. Specifying constraints on each type separately from other types makes each type specification context-independent and promotes reusability of types in different contexts. In addition, the resulting diagrams become easier to disambiguate and the use of a type by another can be cross-checked against its specification (5).
In this section we describe investigations undertaken into the use of the semantic framework to underpin design in software development. The first strand of work concentrated on "design patterns". The second strand developed a set of correct transformations. The third strand considered the development of verification rules in a variety of object-oriented notations.
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 (30). We utilised recent advances in visual modelling notation (e.g., constraint diagrams, see section 3.1) to achieve greater precision in the specification of patterns (38).
This area of work aimed to provide a set of transformations on object-oriented models (in Syntropy and UML) based on the formal semantics in the Object Calculus. A set of transformations for UML class diagrams and statecharts were given and applied to the development process. Transformations allow a verified development to be carried out while concealing the details of formal refinement proof. Specialisation of transformations to safety critical systems has also been defined (26, 27, 35, 37).
In classes developed using design-by-contract, contracts contain assertions that formalise preconditions, postconditions and invariants. To be sure that contracts are complete, they can be derived from specifications. For classes in a data structures library, equational specifications are appropriate. However, a conventional equational specification cannot usually be mapped directly to contracts. We proposed that a second, contract-oriented, equational specification can be devised, with two key properties: it can be proved that the contract-oriented specification implies the original specification; and the contract-oriented specification can be mapped systematically to contracts. These two properties combine to increase confidence that the contracts capture the same abstraction as the equational specification (39, 41).
In this section we describe the development of new notations and extensions to existing notations. The first strand of work developed new diagrammatic notations to complement the existing UML notations. The second strand developed a basis for temporal specifications. In the third strand of work, we made proposals for extending existing 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. It is reminiscent of informal diagrams used by mathematicians for illustrating relations, and borrows much from Venn diagrams. It may be viewed as a generalisation of instance diagrams. 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. They can be used to depict static constraints (e.g, invariants) or dynamic constraints (e.g., action contracts) (19, 21). Constraint diagrams seem capable of expressing most, if not all, static and dynamic constraints, and we proposed that they could be used to give a diagrammatic semantics to OO models (22). 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 and showed that all spider diagrams are self-consistent. We developed inference rules for reasoning with spider diagrams and rules for combining spider diagrams (10, 11, 17, 18).
A formal semantics for object-oriented specification and analysis and design models has been developed, 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. The logic has been applied to the definition of the semantics of VDM++ and the class diagram and statechart models of UML (25, 32, 36). We also propose adding temporal operators into OCL (16).
Traditionally, diagrams used in software systems modelling have been two-dimensional (2D). This is probably because graphical notations, such as those used in object-oriented and structured systems modelling, draw upon the topological graph metaphor, which, at its basic form, receives little benefit from three-dimensional (3D) rendering. Effective use of the third dimension in modelling is achieved by e.g., connecting several graphs together, or in using the Z co-ordinate to show special kinds of edges. Each notation combines several familiar 2D diagrams, which can be reproduced from 2D projections of the 3D model. 3D models are useful even in the absence of a powerful graphical workstation: even 2D stereoscopic projections can expose more information than a plain planar diagram (20).
In (12) we reflect on a number of aspects of the syntax and semantics of the OCL, and make 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.
In this section we describe other related work undertaken by members the project team.
This area of work developed techniques for synthesising and implementing controllers for reactive systems, using the B language and object-oriented specification (31, 34). Object-oriented design techniques such as the state and chain of responsibility design patterns were used.
We developed an approach to the specification of required external non-determinism: the willingness of a component to respond to a number of external action requests using a language which provides both permission and willingness guards on actions (9). We developed a definition of parallel composition for this language, and showed that refinement is compositional with respect to parallel composition. We used the concepts developed to identify extensions to the B and VDM++ languages to incorporate specification of required non-determinism. In particular, we showed that preconditions may be considered as a form of willingness guard, separating concerns of acceptance and termination, once module contracts are re-interpreted in a way suitable for a concurrent environment.
4.4 Distributed Systems
A technique for making physical design decisions within a distributed object-oriented system, based on the logical model of system behaviour is presented in (8). The approach supports iteration between logical and physical modelling activities.
Work under the aims of the project is ongoing. In this section we detail proposals for new projects developed from work done on this project, list collaborators with the project and relate other activities undertaken as part of the project.
Objects, Associations and Subsystems: a hierarchical approach to encapsulation, T.S.E.Maibaum and J.C.Bicarregui
This builds on work described in section 3.3. We propose 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.
Reasoning in Diagrammatic Object-oriented Notations, J. Howse and S. Kent
This builds on work described in section 3.1. We propose to investigate inference rules and composition rules for diagrammatic notations, and hence specify and prototype tools for reasoning with diagrams.
Combining Design by Contract and Proof, J. Howse and R. Mitchell
This builds on work described in section 2.3. We propose to develop a framework for proving a variety of properties of contracts, such as completeness (with respect to given criteria).
PICARD (Patterns in Concurrent and Real-time Design), K. Lano and A. Evans (York University)
This builds on work described in sections 2.1 and 2.2, and aims to define a set of design patterns and refinement transformations to support the use of UML for real-time and concurrent systems.
EPSRC grant GR/M02606, 1997-2000 Precise visual patterns for the evolutionary migration of legacy systems to reusable components. S Kent, J. Howse. This project builds on work described in sections 1.3, 2.1 and 3.1.
In addition, Jean-Marc Jézéquel (IRISA, France) and R. Mitchell have bid under the British Council’s Franco-British Alliance program for funds for exchange travel between Brighton and IRISA, Rennes, in connection with the Trusted Components Initiative (see below).
The project had a formal collaboration agreement with Object Designers Ltd in the person of Managing Director John Daniels. However, Object Designers Ltd ceased trading a short time into the project. Informal links were maintained with John Daniels. We have collaborated with the following: S. Cook (IBM); J. Durrant, F. Molina, J. Taylor (Brighton); A. Evans (York); J. Fiadeiro, A. Lopes (Lisbon); Y. Gil (Technion, Israel); S. Goldsack, P. Kan, A. Sanchez (Imperial); A. Haeberer (Rio de Janeiro); J.-M. Jézéquel (IRISA, France); A. Lauder (Kent); J. McKim (Rensselaer, Hartford, USA); I. Maung (Platinum Technology, USA); B. Meyer (ISE, Inc, USA); C. Mingins (Monash, Australia); B. Rumpe (Munich); A. Wills (Trireme).
The precise UML group (PUML) is a group of international researchers and practitioners who share the aim of developing UML as a precise (i.e., formally defined) modelling language. In particular, they are interested in developing the theory and practice required to reason with properties of UML models, to prove the correctness of UML designs and to give a sound formal basis to the UML Semantics. Stuart Kent and Kevin Lano are core, founder members of PUML.
The Amsterdam Group comprises the lead designers of OCL, together with other leading OO developers and researchers. Richard Mitchell is a founding member. The group is working on improvements to OCL and output from the project is being fed to the group. Work has already been carried out on connecting OCL and UML, on managing multiple semantics for UML, and on changes to OCL (6, 7). Richard Mitchell is also a member of steering group for the Trusted Components Initiative.
Members of the project team have given, or will give, tutorials on CBSD, Design/Analysis by Contract, and Advanced Visual Modelling at ECOOP, OOPSLA, TOOLS Europe, TOOLS USA and TOOLS Pacific.
Richard Mitchell is Programme Chair of TOOLS Europe. Members of the project team are/were programme committee members of OT99, ROOM3, TOOLS Europe 99, TOOLS USA 99, UML99 and organisers of various workshops.
6. References