Search

OMG's Model Driven Architecture demonstrates how a system's specification model can be used within the process of creating supporting software implementations. This article documents the findings of an experiment aimed at determining the extent to which this method of software engineering can be used within the domain of e-Enterprise systems.

A subset of the UML is presented which has been found useful for notating what may loosely be called specification models. A model of aspects of the ODP trader case study is developed (a) to provide a vehicle for introducing the notation, and (b) to demonstrate how the notations can be used together in harmony. In the course of the presentation, some issues concerning the precise definition of UML, and its possible future status as a formal method are discussed.

The Unified Modeling Language (UML) is a set of notations for modelling object-oriented systems. It has become the de facto standard. Most of its notations are diagrammatic. An exception to this is the Object Constraint Language (OCL) which is essentially a textual, stylised form of first order predicate logic. We describe a notation, constraint diagrams, which were introduced as a visual technique intended to be used in conjunction with the UML for object-oriented modelling. Constraint diagrams provide a diagrammatic notation for expressing constraints (e.g., invariants) that could only be expressed in UML using OCL.

The current UML semantics documentation has made a significant step towards providing a precise description of the UML. However, at present the semantic model it proposes only provides a description of the language's syntax and well-formedness rules. The meaning of the language, which is mainly described in English, is too informal and unstructured to provide a foundation for developing formal anal- ysis and development techniques. Another problem is the scope of the model, which is both complex and large. This paper describes work currently being undertaken by the precise UML group (pUML), an international group of researchers and practitioners, to address these problems. A formalisation strategy is presented which concentrates on giving a precise denotational semantics to core elements of UML. This is illustrated through the development of precise definitions of two important concepts: generalization and packages. Finally, a viewpoint architecture is proposed as a means of providing improved separation of concerns in the semantics definition.

This paper makes two contributions. (1) it argues that precise visual modelling techniques are important for modelling large-scale software components, as they facilitate the core activities of component-based software development (CBSD): building, finding, adapting and assembling components. The paper argues for a carefully selected set of techniques based on UML, to provide accessible yet precise component models. (2) it proposes a high level reference model for CBSD to tease out exactly what is meant by the terms `component', `component adaptation' and `component assembly'. The paper illustrates this reference model by giving examples of components, and the transformations that can be applied to them, using precise visual models.

In recent years a number of OO methods have been enhanced with textual, mathematical languages for specifying invariants and action contracts (pre and post conditions). This paper builds on a recent proposal for ''constraint diagrams'', a diagrammatic notation allowing the expression of such assertions. Constraint diagrams essentially provide a pictorial representation of navigation expressions, specifically the sets of objects they define, and, using Venn diagrams and other techniques, constraints on the cardinalities of and relationships between those sets. The original proposal focused on the use of constraint diagrams for depicting invariants. This paper focuses on their use in depicting action contracts.

In component-based development, 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, pre & post conditions, to diagrams. Navigation expressions, which identify collections of objects by navigating associations, are central to making such annotations precise. We give a semantics to navigation expressions as they are used in recently proposed extensions to object-oriented modelling notations in widespread use by practitioners. The semantics is given using Larch (essentially FOPL), which makes it as accessible as possible while enabling some support for reasoning. The semantics helps to clarify some subtle issues to do with navigation expressions, including the meaning of navigating across collections (sets, bags and sequences) as opposed to just single objects, and the use of filters on collections within expressions.

Bespoke development of large business systems can be couched in terms of the composition of components, which are, put simply, chunks of development work. Design, mapping a specification to an implementation, can also be expressed in terms of components: a refinement comprising an abstract component, a concrete component and a mapping between them. Similarly, system extension is the composition of an existing component, the legacy system, with a new component, the extension. This paper overviews work being done on a UK EPSRC funded research project formulating and formalizing techniques for describing, composing and performing integrity checks on components. Although the paper focuses on the specification and development of information systems, the techniques are equally applicable to the modeling and re-engineering of businesses, where no computer system may be involved.

A new visual notation is proposed for precisely expressing constraints on object-oriented models, as an alternative to mathematical logic notation used in methods such as Syntropy and Catalysis. The notation is potentially 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 generalization of instance diagrams.

An object-oriented (OO) model has a static component, the set of allowable snapshots or system states, and a dynamic component, the set of filmstrips or sequences of snapshots. Diagrammatic notations, such as those in UML, each places constraints on the static and/or dynamic models. A formal semantics of OO modeling notations can be constructed by providing a formal description of (i) sets of snapshots and filmstrips, (ii) constraints on those sets, and (iii) the derivation of those constraints from diagrammatic notations. In addition, since constraints are contributed by many diagrams for the same model, a way of doing this compositionally is desirable. One approach to the semantics is to use first-order logic for (i) and (ii), and theory inclusion with renaming, as in Larch, to characterize composition. A common approach to (iii) is to bootstrap: provide a semantics for a kernel of the notation and then use the kernel to give a semantics to the other notations. This only works if a kernel which is sufficiently expressive can be identified, and this is not the case for UML. However, we have developed a diagrammatic notation, dubbed constraint diagrams, which seems capable of expressing most if not all static and dynamic constraints, and it is proposed that this be used to give a diagrammatic semantics to OO models.

Describes a notation, constraint diagrams, which allows pre/post conditions and invariants to be expressed visually, rather than in the notation of mathematical logic. The notation is explored through a small case study (a library system). Some conclusions are drawn about the use of the notation in modelling, and its possible impact on tools and semantics. This report has been split into two and considerable revised and updated: Kent (1997b), Kent (1997c).

This paper presents work performed in the EPSRC ''Object-oriented Specification of Reactive and Real-time Systems'' project. It aims to extend the Object Calculus of Fiadeira and Mailbaum to cover durative actions and real-time constraints. We define a core logic, termed ''Real-time action logic'' (RAL) which can provide an axiomatic semantics and reasoning framework for concurrent, real-time and object-oriented specification languages. The logic could also be viewed as providing the basis of a specification language in its own right. We show how a model action logic (MAL) and real-time logic (RTL) for reasoning about concurrent object-oriented pograms and specifications can be derived from RAL, and indicate how this formalism can be used to provide an axiomatic semantics for a large part of the object-oriented specification language VDM++.

Identifies a number of problems with Eiffel's expanded types in modelling value types, and proposes a backward compatible syntactic extension, and a modified semantics. The latter is also shown to be (effectively) backward compatible, in the sense that existing programs would run unaffected if compilers implemented the new semantics. The benefits of the approach are discussed, including an elegant approach to rebuilding data structure libraries.

This paper considers the relative merits of using features and formal event models to characterise the semantics of English, French and German verb phrases, and con- siders the application of such semantics in machine translation. The feature-based ap- proach represents the semantics in terms of feature systems, which have been widely used in computational linguistics for representing complex syntactic structures. The paper shows how a simple intuitive semantics of verb phrases may be encoded as a feature system, and how this can be used to support modular construction of au- tomatic translation systems through feature look-up tables. This is illustrated by automated translation of English into either French or German. The paper contin- ues to formalise the feature-based approach via a model-based, Montague semantics, which extends previous work on the semantics of English verb phrases. In so doing, repercussions of and to this framework in conducting a contrastive semantic study are considered. The model-based approach also promises to provide support for a more sophisticated approach to translation through logical proof; the paper indicates further work required for the fulfilment of this promise.

This paper discusses extensions to the language Eiffel, required to write more comprehensive software specifications, where a specification in Eiffel is a collection of class interfaces with features specified using an assertion language (i.e. a BON static model). The focus of the paper is the extension of the assertion language with quantification. Two forms of quantification are identified, which are distinguished according to whether the quantified variable is of reference or expanded type. A semantics for each of the two forms is described, and the consequences for assertion checking at run-time considered.