Search

In earlier work we gave a game-based semantics for checkonly QVT-R transformations. We restricted when and where clauses to be conjunctions of relation invocations only, and like the OMG standard, we did not consider cases in which a relation might (directly or indirectly) invoke itself recursively. In this paper we show how to interpret checkonly QVT-R – or any future model transformation language structured similarly – in the modal mu calculus and use its well-understood model-checking game to lift these restrictions. The interpretation via fixpoints gives a principled argument for assigning semantics to recursive transformations. We demonstrate that a particular class of recursive transformations must be ruled out due to monotonicity considerations. We demonstrate and justify a corresponding extension to the rules of the QVT-R game.

The QVT Relations (QVT-R) transformation language allows the definition of bidirectional model transformations, which are required in cases where a two (or more) models must be kept consistent in the face of changes to either. A QVT-R transformation can be used either in checkonly mode, to determine whether a target model is consistent with a given source model, or in enforce mode, to change the target model. Although the most obvious semantic issues in the QVT standard concern the restoration of consistency, in fact even checkonly mode is not completely straightforward; this mode is the focus of this paper. We need to consider the overall structure of the transformation as given by when and where clauses, and the role of trace classes. In the standard, the semantics of QVT-R are given both directly, and by means of a translation to QVT Core, a language which is intended to be simpler. In this paper, we argue that there are irreconcilable differences between the intended semantics of QVT-R and those of QVT Core, so that the translation cannot be helpful. Treating QVT-R directly, we propose a simple game-theoretic semantics. We demonstrate that consistent models may not possess a single trace model whose objects can be read as traceability links in either direction. We briefly discuss the effect of variations in the rules of the game, to elucidate some design choices available to the designers of the QVT-R language.

Bidirectional transformations are important for model-driven development, and are also of wide interest in computer science. In this paper we present early work on an algebraic presentation of bidirectional transformations. In general, a bidirectional transformation must maintain consistency between two models, either of which may be edited, and each of which may incorporate information not represented in the other. Our main focus here is on lenses [2,1,3] which provide a particularly well-understood special case, in which one model is an abstraction of the other, and either the abstraction or the full model may be edited. We show that there is a correspondence between lenses and short exact sequences of monoids of edits. We go on to show that if we restrict attention to invertible edits, very well-behaved lenses correspond to split short exact sequences of groups; this helps to elucidate the structure of the edit groups.

Model transformations are a key element in the OMG's Model Driven Development agenda. They did not begin here: the fundamental idea of transforming, automatically, one model into another is at least as old as the computer, provided that we take a sufficiently broad view of what a model is. In many contexts, people have encountered the need for bidirectional transformations. In this survey paper we discuss the various notions of bidirectional transformation, and their motivation from the needs of software engineering. We discuss the state of the art in work targeted specifically at the OMG's MDD initiative, and also, briefly, related work from other communities. We point out some areas which are so far relatively under-researched, and propose research topics for the future.

We consider the OMG's Queries, Views and Transformations (QVT) standard as applied to the specification of bidirectional transformations between models. We discuss what is meant by bidirectional transformations, and the model-driven development scenarios in which they are needed. We analyse the fundamental requirements on tools which support such transformations, and discuss some semantic issues which arise. We argue that a considerable amount of basic research is needed before suitable tools will be fully realisable, and suggest directions for this future research.

One of the principal uses of UML is the modelling of synchronous object-oriented software systems, in which the behaviour of each of several classes is modelled using a state diagram. UML permits a transition of the state diagram to show both the event which causes the transition (typically, the fact that the object receives a message) and the object's reaction (typically, the fact that the object sends a message). UML's semantics for state diagrams is "run to completion". We show that this can lead to anomalous behaviour, and in particular that it is not possible to model recursive calls, in which an object receives a second message whilst still in the process of reacting to the first. Drawing on both ongoing work by the UML2.0 submitters and recent theoretical work [ 1 ],[ 6 ], we propose a solution to this problem using state diagrams in two complementary ways.

Global systems – systems which may operate over transient networks including mobile elements and in which computation itself may be mobile – are gaining in importance. Nevertheless, the means for their modelling are still underdeveloped. The Unified Modelling Language (UML) is well developed for convenient modelling of behavior, but is not yet so useful for modelling aspects of design relevant to global systems, such as mobility. Non-functional requirements such as performance and security also assume an increased importance in the context of global systems, and here too, UML requires enhancement.In this paper we present an extension to UML class, sequence and activity diagrams to model mobile systems. We also describe extensions to model performance and security characteristics. We will describe how, wherever possible, we reuse existing work in these areas.

In the Unified Modelling Language, use cases are provided as a way of summarising the requirements on a system. They are defined informally as specifications of sets of sequences of actions, and several relationships between use cases are informally defined. Dependable, tool-supported software development necessitates precise definitions of all these concepts but the topic has so far received little attention in the literature, beyond what is present in Catalysis. This paper explores how these notions can be formalised whilst staying as close as possible to the UML standard, makes some suggestions and raises further questions.

In this paper we propose finding winning strategies of abstract games as an approach to verification problems which permits both a variable level of abstraction and on-the-fly exploration. We describe a generic algorithm which, when instantiated with certain functions specific to the concrete game, computes a winning strategy. We apply this technique to bisimulation and model-checking of value-passing processes, and to timed automata.