Search

In software engineering, documentation and models are both broad concepts which attract varying approaches and attitudes. Moreover, as the title indicates, they overlap: in some circumstances, an artefact thought of as a model can serve to document a software project, while in others, an artefact thought of as a document can be manipulated by model-driven engineering tools just like any other kind of model. In this short paper we briefly explore these issues and provide pointers to some of the relevant literature.

Separating concerns into multiple data sources, such as multiple models of a software system under development, enables people to work in parallel. However, concerns must also be re-integrated, and this gives rise to many interesting problems, both theoretical and practical. In my keynote talk I will discuss some of them; in this accompanying paper I give some background to my work in recent years and summarise some key points and definitions.

What is the future of programming, and what does it have to do with modelling? In this paper we will first argue that, despite impressive achievements, software development now suffers from a capacity crisis which cannot be alleviated by programming as currently conceived. Rather, it is necessary to democratise the development of software: stake-holders who are not software specialists must, somehow, be empowered to take more of the decisions about how the software they use shall behave. We will suggest that a potential way to achieve this is that software should be delivered in the form of a collection of models, each expressed in a (domain-specific) language appropriate to its intended users, and all connected by bidirectional transformations. We emphasise the pragmatic need to accommodate a heterogeneous collection of formalisms so that solutions can incorporate pre-existing transformations, with automatic “fixing up” of their results as necessary. We discuss the advances that are needed to make this a reality, and some early progress in this direction.

Bidirectional transformations (bx) are a mechanism for maintaining the consistency of two (or more) related sources of information, such as models in model-driven development, database schemas, or programs. Bx technologies have been developed for practical engineering purposes in many diverse fields. Different disciplines such as programming languages, graph transformations, software engineering, and databases have contributed to the concepts and theory of bx. However, so far, most efforts have been focused on the case where exactly two information sources must be kept consistent; the case of more than two has usually been considered as an afterthought. In many practical scenarios, it is essential to work with more than two information sources, but the community has hardly started to identify and address the research challenges that this brings. Driven by the practical needs and usage scenarios from industry, this Dagstuhl Seminar aimed to identify the challenges, issues and open research problems for multidirectional model transformations and synchronisations and sketch a road map for developing relevant concepts, theories and tools. The report contains an executive summary of the seminar, reports from its working groups, as well as descriptions of industrial and academic case studies that motivated the discussions.

Bidirectional transformations maintain consistency between information sources, such as different models of the same software system. In certain settings this is undeniably convenient – but is it important? I will argue that developing our ability to engineer dependable bidirectional transformations is likely to be crucial to our ability to meet the demand for software in coming decades. I will discuss some of the work that has been done so far, including some I’ve had a hand in, and what challenges remain.

Bidirectional transformations (bx) are a mechanism for maintaining the consistency of two (or more) related sources of information, such as models in model-driven development, database schemas, or programs. Bx technologies have been developed for practical engineering purposes in many diverse fields. Different disciplines such as programming languages, graph transformations, software engineering, and databases have contributed to the concepts and theory of bx. However, so far, most efforts have been focused on the case where exactly two information sources must be kept consistent; the case of more than two has usually been considered as an afterthought. In many practical scenarios, it is essential to work with more than two information sources, but the community has hardly started to identify and address the research challenges that this brings. Driven by the practical needs and usage scenarios from industry, this Dagstuhl Seminar aimed to identify the challenges, issues and open research problems for multidirectional model ransformations and synchronisations and sketch a road map for developing relevant concepts, theories and tools. The report contains an executive summary of the seminar, reports from its working groups, as well as descriptions of industrial and academic case studies that motivated the discussions.

The study of models, and related concepts such as metamodels, islargely situated within the software engineering community under thebanner of model-driven development. Yet these concepts have some obviousparallels with concepts developed within the articial intelligencecommunity under the banners of ontologies and the semantic web. Althougha considerable amount of work has been done that aims to relatethe development of ontologies to the model-driven development of software,the place of bidirectional transformations within these connectedworlds is (almost) unstudied. Yet, experts in the study of ontologieshave experienced the need to check and restore consistency, and havedeveloped techniques, terminology and tools that relate to these tasks.In this paper we provide a high-level introduction to the work that hasbeen done, aiming to promote further study and perhaps collaborationbetween these communities.

This paper presents a model-based testing framework for probabilistic systems. We provide algorithms to generate, execute and evaluate test cases from a probabilistic requirements model. In doing so, we connect ioco-theory for model-based testing and statistical hypothesis testing: our ioco-style algorithms handle the functional aspects, while statistical methods, using $$\chi ^2$$i¾?2 tests and fitting functions, assess if the frequencies observed during test execution correspond to the probabilities specified in the requirements. Key results of our paper are the classical soundness and completeness properties, establishing the mathematical correctness of our framework; Soundness states that each test case is assigned the right verdict. Completeness states that the framework is powerful enough to discover each probabilistic deviation from the specification, with arbitrary precision. We illustrate the use of our framework via two case studies.

Much of the bx literature, especially that couched in terms of consistency restoration, presupposes a workflow based on strict sequentialisation of model updates, and in some cases explicitly via a centralised broker of shared state. Put another way: the underlying mathematical semantics of bx take little account of the deployment context for such artefacts, which, from a user’s perspective, are typically concurrent and distributed. This discussion proposal invites discussion of the bx deployment context.

A foundational property of bidirectional transformations is that they should be correct: that is, the transformation should succeed in restoring consistency between any models it is given. In practice, however, transformation engines sometimes fail to restore consistency, e.g. because there is no consistent model to return, or because the tool is unable to select a best model to return from among equally good candidates. In this paper, we formalise properties that may nevertheless hold in such circumstances and discuss relationships and implications.

We survey the key objectives and the structure of this Dagstuhl seminar,and discuss common themes that emerged.

From 27.08.06 to 01.09.06, the Dagstuhl Seminar 06351 "Methods for Modelling Software Systems (MMOSS)" was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.

An important decision that must be taken by anyone designing a course involving (object oriented software) modelling is what tool support, if any, to use. Options include picking an industrial strength modelling tool, using a tool specifically designed for educational use, or eschewing tool use altogether in favour of pencil and paper. The best answer will depend on many factors, including the prior experience of the students (and staff), the length and organisation of the course, and the learning objectives. Moreover, decisions on tools have an impact on other aspects of course design. In this informal paper, the result of discussion at the MODELS Educators’ Symposium 2013, we survey previous work on this question, discuss our own experience, and draw out some key issues that someone designing a new course involving modelling must consider.

The success of telemedicine systems requires sufficiently high productivity, satisfaction and low error rates: in short, usability. However, the costs associated with performing pre-deployment usability studies often make them infeasible. This results in usability problems which may manifest differently in different deployment contexts and cause different levels of inefficiency and discomfort to their users, potentially even leading to errors which may threaten patients' lives. This paper shows by means of examples how experimentation with different workloads, user profiles and system characteristics can suggest problems that may arise in deploying a telemedicine system into new contexts. Such approaches might support the roll-out of large telemedicine implementations, as the one currently planned in the UK.

A bidirectional transformation on a pair of sets of models induces two principal equivalence relations on each set of models. Since a model can be uniquely identified by specifying its equivalence class in each of these relations, they function as a coordinate system for the model sets, with respect to the transformation. We prove some results relating to this observation. Using them we give the implication relationships between various properties of bidirectional transformations. In particular, we characterise the bidirectional transformations that can be decomposed into a pair of lenses working ``tail to tail''., Electronic Communications of the EASST, Volume 49: Bidirectional Transformations 2012

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.

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.

UML, the Unified Modeling Language, is a standard diagrammatic language for recording the design of systems, especially object-oriented software systems. One of the main benefits of a unified modeling language is that it enables competition between tool vendors and allows users a wide choice of tools. Getting the most out of a tool - which is often a significant investment - means using it as more than a fancy drawing tool. In this position paper I will argue that the combination of XML and UML - especially in the form of XMI, the OMG’s standard XML Metadata Interchange format - is crucial enabling technology for getting good value out of a UML tool. Indeed, I believe that it may revolutionise the use of modelling tools in future.

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.

We compare Haskell with ML as programming languages for verification tools, based on our experience developing TRUTH in Haskell and the Edinburgh Concurrency Workbench (CWB) in ML. We discuss not only technical language features but also the “worlds” of the languages, for example, the availability of tools and libraries.

This position paper reports some work in progress on the use of UML, the industry standard object oriented modelling language, as a notation for describing product line architectures. We draw on a great deal of previous work on notations for architectures and PLAs, and on UML as a notation for architectures and for frameworks, attempting to identify the salient points of this particular question.

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.

This paper reports the experience of Edinburgh University's Department of Computer Science in undertaking, in two stages, a major reform of its software engineering teaching in the third and fourth years of the degree. Our aim was to increase our students' exposure to object oriented and component based software engineering, aspects of modern software engineering which are highly relevant to the careers many of them undertake. One of our more significant decisions was to teach the emerging standard modelling language, UML. The paper describes the background to the decision to change the course, the changes that were made, and the results of the changes. It does not presume to draw universal lessons from the story, but does describe what we see as the significant features.

In this thesis we determine the integral forms in Weyl modules for GL(2,Q). We work with the Schur algebra exclusively; we do not use the Lie algebra of GL(2,Q).\ud \ud In Chapter 1 we give the necessary background. We begin to simplify the problem, using the known reduction of it to the problem of finding those integral forms which lie between certain limits -Y and V. Together with localisation at each prime p, this enables us to restrict our attention to the structure of X/Vp. We show that we can deduce the integral structure of any Weyl module from that of Weyl modules with highest weight (r, 0) for an integer r. We describe a duality which arises on X/Vp. In Chapter 2 we prove a rather surprising number-theoretic result which allows us to simplify the problem further. In Chapter 3 we arrive at a very simple characterisation of the integral forms, namely that they can be represented as those integer labellings of a particular graph, the scoreable set lattice, which satisfy a certain criterion. We exploit this to prove various general results about the structure of X/Vp. We show how it is possible, using our methods, to describe the structure of X/Vp in arbitrarily complicated cases in terms of simpler structures. In Chapter 4, we discuss the relevance of our work to the theory of modular Weyl modules, and we explain how our work relates to that of others.

Lecture Notes in Computer Science, 9633, ISSN:0302-9743, ISSN:1611-3349, Fundamental Approaches to Software Engineering, ISBN:978-3-662-49665-7, ISBN:978-3-662-49664-0

As interactions and dependencies within distributed reactive systems increase, the problem of detecting failures which depend on the exact situation and environmental conditions they occur in grows. As a result, not only the detection of failures is increasingly difficult, but also the differentiation between the symptoms of a fault, and the actual fault itself, i. e., the cause of a failure. This thesis proposes an efficient approach for the analysis of distributed reactive systems at runtime. It introduces a framework, referred to as monitoring-based runtime reflection framework, for the detection of failures as well as identification of their causes. As an interface to the framework, this thesis proposes a specification language, Salt, to express desired system properties, which then have to hold at all times while a system executes. Detection of failures in the framework is based upon monitoring systems with respect to their associated properties, defined in the high-level specification language Salt. Salt specifications are translatable into the real-time temporal logic TLTL as well as in the untimed temporal logic LTL, and as such can also be used with other temporal logic verification frameworks, such as model checkers. For both logics, an efficient monitor generation procedure is developed for either monitoring qualitative assertions about a system’s behaviour in the untimed case, or quantitative assertions reflecting dense real-time constraints. In order to reflect the semantics of LTL, respectively TLTL, with respect to a finite observational trace in a suitable and unambiguous manner, a 3-valued interpretation is proposed. The corresponding 3-valued monitoring procedure is shown to be optimal with respect to the space-complexity of the generated monitors, and able to detect all minimal bad prefixes of non-conforming system behaviour. Based on the results of the monitors, a dedicated failure diagnosis is performed to identify possible explanations for an observed deviation. As such, diagnosis can either confirm that a monitor detected the root cause for a failure, or indicate that the fault is located elsewhere, and possibly outside the scope of the monitored system. In the runtime reflection framework, diagnosis is based upon the principles of first-order model-based diagnosis, but developed in the propositional domain. The propositional diagnosis problem is then shown to correspond to a deterministic implementation of a solution to the #SAT problem for which a computationally efficient realisation is introduced. This thesis develops both the theoretical foundations for runtime reflection as well as efficient means for its implementation. Zunahme von Abhängigkeiten und daraus resultierende, komplexe Interaktionsmuster in verteilten reaktiven Systemen erschweren die Entdeckung von Fehlern, die in komplizierter Weise von Situations- und Umweltbedingungen der Systeme abhängen. In Folge ist oft nicht nur die Erkennung von Fehlverhalten technisch aufwändig, sondern auch die Unterscheidung zwischen Fehlersymptomen und -ursachen. Im Rahmen dieser Arbeit wird ein Verfahren zur dynamischen Analyse von verteilten reaktiven Systemen vorgestellt, welches auf der Überwachung und Interpretation des beobachtbaren Systemverhaltens, sowie der anschließenden Diagnose registrierter Abweichungen basiert. Als Schnittstelle zum Benutzer wird eine abstrakte Spezifikationssprache vorgestellt, um beobachtbare Eigenschaften zu definieren, die vom System stets erfüllt werden müssen. Die formalen Grundlagen des dynamischen Analyseverfahrens, sowie effiziente Techniken zu deren Umsetzung, bilden den Hauptgegenstand dieser Arbeit.

Performance analysis of computing systems, in particular distributed computing systems, is a complex process. Analysing the complex flows and interactions between a set of distributed processing nodes is a non-trivial task. The problem is exacerbated by the addition of continuous system functions that are time dependent, such as communication between components in the form of multimedia streams of video and audio data. Quality-of-Service (QoS) specifications define constraints on such communications and describe the required patterns of data transfer. By making use of these specifications as part of the performance analysis process it is possible to add significant confidence to predictions about the correct (required) operation of a distributed system. This paper presents a method for designing distributed multimedia systems, including the specification of QoS, using the ODP framework and UML and describes a technique for verifying the QoS specification against the designed functional behaviour of the system using Timed Automata.