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.

Bidirectional transformations (bx) support principled consistency maintenance between data sources. Each data source corresponds to one perspective on a composite system, manifested by operations to 'get' and 'set' a view of the whole from that particular perspective. Bx are important in a wide range of settings, including databases, interactive applications, and model-driven development. We show that bx are naturally modelled in terms of mutable state; in particular, the 'set' operations are stateful functions. This leads naturally to considering bx that exploit other computational effects too, such as I/O, nondeterminism, and failure, all largely ignored in the bx literature to date. We present a semantic foundation for symmetric bidirectional transformations with effects. We build on the mature theory of monadic encapsulation of effects in functional programming, develop the equational theory and important combinators for effectful bx, and provide a prototype implementation in Haskell along with several illustrative examples.

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.

Electronic Communications of the EASST, Volume 57: Bidirectional Transformations 2013

Electronic Communications of the EASST, Volume 57: Bidirectional Transformations 2013

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.

Bidirectional transformations bx are a mechanism for maintaining the consistency of two (or more) related sources of information. Researchers from many different areas of computer science including databases (DB), graph transformations (GT), software engineering (SE), and programming languages (PL) are actively investigating the use of bx to solve a diverse set of problems. Although researchers have been actively working on bidirectional transformations in the above mentioned communities for many years already, there has been very little cross-discipline interaction and cooperation so far. The purpose of a first International Meeting on Bidirectional Transformations (GRACE-BX), held in December 2008 near Tokyo, was therefore to bring together international elites, promising young researchers, and leading practitioners to share problems, discuss solutions, and open a dialogue towards understanding the common underpinnings of bx in all these areas. While the GRACE-BX meeting provided a starting point for exchanging ideas in different communities and confirmed our believe that there is a considerable overlap of studied problems and developed solutions in the identified communities, the Dagstuhl Seminar 11031 on ``Bidirectional Transformations'' also aimed at providing a place for working together to define a common vocabulary of terms and desirable properties of bidirectional transformations, develop a suite of benchmarks, solve some challenging problems, and launch joint efforts to form a living bx community of cooperating experts across the identified subdisciplines. This report documents the program and the outcomes of Dagstuhl Seminar 11031 with abstracts of tutorials, working groups, and presentations on specific research topics.

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.

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.

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

Performance, dependability and quality of service (QoS) are prime aspects of the UML modeling domain. To capture these aspects effectively in a modeling language requires easy-to-use support for the specification and analysis of randomly varying behaviors. This paper introduces an extension of UML statecharts with randomly varying durations, by enriching a specific syntactic construct: The after operator is equipped with (discrete or continuous) probability distributions, determining the duration of the delay caused by this operator. The semantics of this extension is given in terms of a variant of stochastic automata. It is shown how existing model-checking tools can be used to calculate model-inherent QoS characteristics automatically. We study a UML model of an automatic teller machine scenario using this approach.

The main motivation for the development of the OMG's XML Metadata Interchange Format (XMI) was the need to have a standard way for UML tools to interchange UML models. However, the fact that UML models, saved as XML documents, are now accessible to standard XML tools, opens up new possibilities to which less attention has so far been paid. This paper discusses how XMI can be exploited for performing model analysis and housekeeping tasks and for the integration of third party or in-house tools. With the help of examples we focus on what can be achieved with small-scale XMI programming by a single developer in hours rather than days. We suggest that this new capability may have important and positive implications for the future of UML modelling using tools.

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.

In recent work we have proposed abstract games, and an example algorithm for finding winning strategies of them, as an approach to verification problems - such as model-checking and equivalence checking - which permits both a variable level of abstraction and on-the-fly exploration. It was clear that this work had something in common with abstract interpretation. This paper, which describes work in progress, generalises and makes the connection explicit.

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.

Ontology engineering is the field, within knowledge representation, concerned with using logic-based formalisms to represent knowledge, typically moderately sized knowledge bases called ontologies. How to best develop, use and maintain these ontologies has produced relatively large bodies of both formal, theoretical and methodological research. One subfield of ontology engineering is ontology debugging, and is concerned with preventing, detecting and repairing errors (or more generally pitfalls, bad practices or faults) in ontologies. Due to the logical nature of ontologies and, in particular, entailment, these faults are often both hard to prevent and detect and have far reaching consequences. This makes ontology debugging one of the principal challenges to more widespread adoption of ontologies in applications. Moreover, another important subfield in ontology engineering is that of ontology alignment: combining multiple ontologies to produce more powerful results than the simple sum of the parts. Ontology alignment further increases the issues, difficulties and challenges of ontology debugging by introducing, propagating and exacerbating faults in ontologies. A relevant aspect of the field of ontology debugging is that, due to the challenges and difficulties, research within it is usually notably constrained in its scope, focusing on particular aspects of the problem or on the application to only certain subdomains or under specific methodologies. Similarly, the approaches are often ad hoc and only related to other approaches at a conceptual level. There are no well established and widely used formalisms, definitions or benchmarks that form a foundation of the field of ontology debugging. In this thesis, I tackle the problem of ontology debugging from a more abstract than usual point of view, looking at existing literature in the field and attempting to extract common ideas and specially focussing on formulating them in a common language and under a common approach. Meta-ontology fault detection is a framework for detecting faults in ontologies that utilizes semantic fault patterns to express schematic entailments that typically indicate faults in a systematic way. The formalism that I developed to represent these patterns is called existential second-order query logic (abbreviated as ESQ logic). I further reformulated a large proportion of the ideas present in some of the existing research pieces into this framework and as patterns in ESQ logic, providing a pattern catalogue. Most of the work during my PhD has been spent in designing and implementing an algorithm to effectively automatically detect arbitrary ESQ patterns in arbitrary ontologies. The result is what we call minimal commitment resolution for ESQ logic, an extension of first-order resolution, drawing on important ideas from higher-order unification and implementing a novel approach to unification problems using dependency graphs. I have proven important theoretical properties about this algorithm such as its soundness, its termination (in a certain sense and under certain conditions) and its fairness or completeness in the enumeration of infinite spaces of solutions. Moreover, I have produced an implementation of minimal commitment resolution for ESQ logic in Haskell that has passed all unit tests and produces non-trivial results on small examples. However, attempts to apply this algorithm to examples of a more realistic size have proven unsuccessful, with computation times that exceed our tolerance levels. In this thesis, I have provided both details of the challenges faced in this regard, as well as other successful forms of qualitative evaluation of the meta-ontology fault detection approach, and discussions about both what I believe are the main causes of the computational feasibility problems, ideas on how to overcome them, and also ideas on other directions of future work that could use the results in the thesis to contribute to the production of foundational formalisms, ideas and approaches to ontology debugging that can properly combine existing constrained research. It is unclear to me whether minimal commitment resolution for ESQ logic can, in its current shape, be implemented efficiently or not, but I believe that, at the very least, the theoretical and conceptual underpinnings that I have presented in this thesis will be useful to produce more foundational results in the field.

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.

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

Several European countries, including the UK, are investing in large-scale telehealthcare pilots, to thoroughly evaluate the benefits of telehealthcare. Due to the high level of risk associated with such projects, it becomes desirable to be able to predict the success of telehealthcare systems in potential deployments, in order to inform investment and help save resources. An important factor for the success of any telehealthcare deployment is usability, as it helps to achieve the benefits of the technology through increased productivity, decreased error rates, and better acceptance. In particular, efficiency, one of the characteristics of usability, should be seen as a central measure for success, as the timely care of a high number of patients is one of the important claims of telehealthcare. Despite the recognized importance of usability, it is seen as secondary in the design of telehealthcare systems. The resulting problems are difficult to predict due to the heterogeneity of deployment contexts. This thesis proposes the automation of usability evaluation through the use of modelling and simulation techniques. It describes a generic methodology which can guide a modeller in reusing models for predicting characteristics of usability within different deployment sites. It also describes a modelling approach which can be used together with the methodology, to run in parallel a user model, inspired from a cognitive architecture, and a system model, represented as a basic labelled transition system. The approach simulates a user working with a telehealthcare system, and within her environment, to predict the efficiency of the system and work process surrounding it. The modeller can experiment with different inputs to the models in terms of user profile, workload, ways of working, and system design, to model different potential- real or hypothetical- deployments, and obtain efficiency predictions for each. A comparison of the predictions helps analyse the effects on efficiency of changes in deployments. The work is presented as an experimental investigation, but emphasises the great potential of modelling and simulation for helping to inform investment, help reduce costs, mitigate risks and suggest changes that would be necessary for improving the usability, and therefore success or telehealthcare deployments. My vision is that, if used commercially, the approaches presented in this thesis could help reduce risks for scaling up telehealthcare deployments.

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.

The Unified Modeling Language (UML) has become the standard language for the design of object-oriented software systems over the past decade. Even though there exist various tools which claim to support design with UML, their functionality is usually focused on drawing UML diagrams and generating code from the UML model. The task of choosing a suitable design which fulfils the requirements still has to be accomplished by the human designer alone. The aim of this thesis is to develop concepts for UML design tools which assist the modeller in improving the system design and requirements incrementally. For this approach a variant of formal games called exploration games is introduced as underlying technique. Exploration games can be defined on the basis of incomplete and imprecise UML models as they occur frequently in practice. The designer repeatedly plays an exploration game to detect flaws or incompleteness in the design and its specification, which are both incorporated in the game definition. At any time the game definition can be incremented by the modeller which allows him to react to the discoveries made during a play and experiment with new design solutions. Exploration games can be applied to UML in different variants. For each variant must be specified how the UML diagrams are used to set up the game and how the semantic variation points of UML should be interpreted. Furthermore some parts of the game definition may not be contained in the UML model and have to be provided separately. The emphasis of this thesis is on game variants which make use of UML diagrams for modelling system behaviour, especially state machines and activity diagrams. A prototypical implementation demonstrates how the concepts developed in this thesis can be put into practice. The tool supports the user in defining, playing and incrementing a game. Moreover it can compute winning strategies for the players and may act as opponent of the modeller. As example a game variant based on UML state machines has been implemented. The architecture that has been chosen for the tool leaves room for extension by additional game variants and alternative algorithms.

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.