Modern software systems are often realized by coordinating multiple heterogeneous parts, each responsible for specific tasks. These parts must work together seamlessly to satisfy the overall system requirements. To verify such complex systems, we have developed a non-intrusive coordination frame-work capable of performing formal analysis of heterogeneous parts that exchange data and include real-time capabilities. The framework utilizes a linguistic extension-which is implemented as a central broker and a domain-specific language-for the integration of heterogeneous languages and coordination of parts. Moreover, abstract rule templates are reified as language adapters for non-intrusive communications with the broker. The framework is implemented using rewriting logic (Maude), and its applicability is demonstrated by verifying certain correctness properties of a heterogeneous road-rail crossing system.

The Business Process Modeling Notation (BPMN) is a widely used standard notation for defining intra- and inter-organizational workflows. However, the informal description of the BPMN execution semantics leads to different interpretations of BPMN elements and difficulties in checking behavioral properties. In this article, we propose a formalization of the execution semantics of BPMN that, compared to existing approaches, covers more BPMN elements while also facilitating property checking. Our approach is based on a higher-order transformation from BPMN models to graph transformation systems. To show the capabilities of our approach, we implemented it as an open-source web-based tool.

Multilevel Modelling (MLM) approaches make it possible for designers and modellers to work with an unlimited number of abstraction levels to specify their domain-specific modelling languages (DSMLs). To fully exploit MLM techniques, we need powerful model composition operators. Indeed, the composition of DSMLs is becoming increasingly relevant to the modelling community either because some DSMLs may share commonalities that we want to make reusable, or because we want to facilitate interoperability between DSMLs. In this paper, we propose a composition mechanism for structure and behaviour of multilevel modelling hierarchies. Our approach facilitates the inclusion of additional features while keeping a clear separation of concerns that enhances modularity. We provide a formal semantics of the constructions based on category theory and graph transformations, and show their use in practice on a case study.

Debugging is an essential part of software maintenance and evolution since it allows software developers to analyze program execution step by step. Understanding a program is required to fix potential flaws, alleviate bottlenecks, and implement new desired features. Thus, software developers spend a large percentage of their time validating and debugging software, resulting in high software maintenance and evolution cost. We aim to reduce this cost by providing a novel visual debugging tool to software developers to foster program comprehension during debugging. Our debugging tool visualizes program execution information graphically as an object diagram and is fully integrated into the popular Java development environment IntelliJ IDEA. Moreover, the object diagram allows interactions to explore program execution information in more detail. A demonstration of our tool is available at https://www.youtube.com/watch?v=lU_OgotweRk.

Abstract In model-driven software engineering, models are used in all phases of the development process. These models must hold a high quality since the implementation of the systems they represent relies on them. Several existing tools reduce the burden of manually dealing with issues that affect models’ quality, such as syntax errors, model smells, and inadequate structures. However, these tools are often inflexible for customization and hard to extend. This paper presents a customizable and extensible model repair framework, PARMOREL, that enables users to deal with different issues in different types of models. The framework uses reinforcement learning to automatically find the best sequence of actions for repairing a broken model according to user preferences. As proof of concept, we repair syntactic errors in class diagrams taking into account a model distance metric and quality characteristics. In addition, we restore inter-model consistency between UML class and sequence diagrams while improving the coupling qualities of the sequence diagrams. Furthermore, we evaluate the approach on a large publicly available dataset and a set of real-world inspired models to show that PARMOREL can decide and pick the best solution to solve the issues present in the models to satisfy user preferences.

Abstract Artificial intelligence has already proven to be a powerful tool to automate and improve how we deal with software development processes. The application of artificial intelligence to model-driven engineering projects is becoming more and more popular; however, within the model repair field, the use of this technique remains mostly an open challenge. In this paper, we explore some existing approaches in the field of AI-powered model repair. From the existing approaches in this field, we identify a series of challenges which the community needs to overcome. In addition, we present a number of research opportunities by taking inspiration from other fields which have successfully used artificial intelligence, such as code repair. Moreover, we discuss the connection between the existing approaches and the opportunities with the identified challenges. Finally, we present the outcomes of our experience of applying artificial intelligence to model repair.

Abstract Digital fabrication tools such as 3D printers, computer-numerically controlled (CNC) milling machines, and laser cutters are becoming increasingly available, ranging from consumer to industrial versions. Recent studies have shown that users, ranging from researchers, to industry professionals, to hobbyists, are interested in modifying and changing the inherit workflows these tools provide. As an answer to this, these users are increasingly modifying and customizing their machines by changing the work envelope, adding different end-effectors, and creating their own fabrication workflows in software. However, customizing, modifying and creating digital fabrication machines and the workflows they provide require extensive knowledge within multiple different engineering domains and is non-trivial. In this article we present a model-driven approach that enables users to expand their digital fabrication scope by providing a high-level tool that facilitates the customization of fabrication tools. We present The Farbicatable Axis, a model that enables users to create customized linear actuators. The model takes high-level input parameters such as length and gearing-parameters, and outputs a CAD model of a linear motion axis consisting of fabricatable parts. We then present how instances of the Fabricatable Axis can be combined and used to design and implement Fabricatable Machines.

Abstract Model management is a central activity in Software Engineering. The most challenging aspect of model management is to keep inter-related models consistent with each other while they evolve. As a consequence, there is a lot of scientific activity in this area, which has produced an extensive body of knowledge, methods, results and tools. The majority of these approaches, however, are limited to binary inter-model relations; i.e. the synchronisation of exactly two models. Yet, not every multi-ary relation can be factored into a family of binary relations. In this paper, we propose and investigate a novel comprehensive system construction, which is able to represent multi-ary relations among multiple models in an integrated manner and thus serves as a formal foundation for artefacts used in consistency management activities involving multiple models. The construction is based on the definition of partial commonalities among a set of models using the same language, which is used to denote the (local) models. The main theoretical results of this paper are proofs of the facts that comprehensive systems are an admissible environment for (i) applying formal means of consistency verification (diagrammatic predicate framework), (ii) performing algebraic graph transformation (weak adhesive HLR category), and (iii) that they generalise the underlying setting of graph diagrams and triple graph grammars.

Model management is a central activity in Software Engineering. The most challenging aspect of model management is to keep models consistent with each other while they evolve. As a consequence, there has been increasing activity in this area, which has produced a number of approaches to address this synchronization challenge. The majority of these approaches, however, is limited to a binary setting; i.e. the synchronization of exactly two models with each other. A recent Dagstuhl seminar on multidirectional transformations made it clear that there is a need for further investigations in the domain of general multiple model synchronization simply because not every multiary consistency relation can be factored into binary ones. However, with the help of an auxiliary artifact, which provides a global view over all models, multiary synchronization can be achieved by existing binary model synchronization means. In this paper, we propose a novel comprehensive system construction to produce such an artifact using the same underlying base modelling language as the one used to define the models. Our approach is based on the definition of partial commonalities among a set of aligned models. Comprehensive systems can be shown to generalize the underlying categories of graph diagrams and triple graph grammars and can efficiently be implemented in existing tools.

In model-driven software engineering, models are used in all phases of the development process. These models may get broken due to various editions during the modeling process. There are a number of existing tools that reduce the burden of manually dealing with correctness issues in models, however, most of these tools do not prioritize customization to follow user requirements nor allow the extension of their components to adapt to different model types. In this paper, we present an extensible model repair framework which enables users to deal with different types of models and to add their own repair preferences to customize the results. The framework uses customizable learning algorithms to automatically find the best sequence of actions for repairing a broken model according to the user preferences. As an example, we customize the framework by including as a preference a model distance metric, which allows the user to choose a more or less conservative repair. Then, we evaluate how this preference extension affects the results of the repair by comparing different distance metric calculations. Our experiment proves that extending the framework makes it more precise and produces models with better quality characteristics.

Digital fabrication tools such as 3D printers, computer-numerically controlled (CNC) milling machines, and laser cutters are becoming increasingly available, ranging from consumer to industrial versions. Although these tools have enabled a completely new set of users to take part in manufacturing, they are still limited in their use and the workflows they provide. As an answer to this, users are modifying and customizing their machines by changing the work envelope and adding different end-effectors. However, customizing, modifying and creating digital fabrication machines require extensive knowledge within multiple different engineering domains, and is non-trivial. In this paper, we present The Fabricatable Axis, a high-level parametric model that aims to simplify the process of experimenting, customizing and implementing digital fabrication machines. This model encapsulates the knowledge of an experienced machine designer into a model that less experienced machine builders can use to design and customize linear and rotary motion axes which can be combined into different machines. The model receives high-level input parameters such as axis type, length and speed-parameters, and outputs a CAD model of a motion axis consisting of fabricatable parts (parts that are readily available or parts that can be fabricated using accessible tools such as a CNC milling machine). To validate our contribution, we first present a constructed scenario were we use the model to implement a specific machine. Secondly, we present an evaluation of our tool through a series of interviews with users who have been using the model to create different types of machines.

Metamodels are at the core of any modeling ecosystem. As their evolution is inevitable, the management of artifacts which depend on these metamodels is a complicated task. Restoring the validity of the corrupted artifacts after a metamodel evolution in a (semi-)automated manner is intrinsically difficult especially when considering the exact impact of the evolution on the restoring process. In this paper, we propose a generic approach to automatically quantify and identify the impact of metamodel evolution on two related artifacts: models and transformations. The approach starts from the evolution definition and generates OCL queries that can be executed on these artifacts to obtain the impacted elements. The knowledge gained from the impact analysis may then guide the user in the decision on whether to proceed with the evolution or to revert it.

Paraplegia is a disability caused by impairment in motor or sensory functions of the lower limbs. Most paraplegic subjects use mechanical wheelchairs for their movement, however, patients with reduced upper limb functionality may benefit from the use of motorised, electric wheel- chairs. Depending on the patient, learning how to control these wheelchairs can be hard (if at all possible), time-consuming, demotivating, and to some extent dangerous. This paper proposes a game-based learning framework for training these patients in a safe, virtual environment. Specifically, the framework utilises the Emotiv EPOC EEG headset to enable brain wave control of a virtual electric wheelchair in a realistic virtual world game environment created with the Unity 3D game engine.

This paper demonstrates rapid prototyping of a stroke rehabilitation system consisting of an interactive 3D virtual reality computer game environment interfaced with an EEG headset for control and interaction using brain waves. The system is intended for training and rehabilitation of partially monoplegic stroke patients and uses low-cost commercial-off-the-shelf products like the Emotiv EPOC EEG headset and the Unity 3D game engine. A number of rehabilitation methods exist that can improve motor control and function of the paretic upper limb in stroke survivors. Unfortunately, most of these methods are commonly characterised by a number of drawbacks that can limit intensive treatment, including being repetitive, uninspiring, and labour intensive; requiring one-on-one manual interaction and assistance from a therapist, often for several weeks; and involve equipment and systems that are complex and expensive and cannot be used at home but only in hospitals and institutions by trained personnel. Inspired by the principles of mirror therapy and game-stimulated rehabilitation, we have developed a first prototype of a game-like computer application that tries to avoid these drawbacks. For rehabilitation purposes, we deprive the patient of the view of the paretic hand while being challenged with controlling a virtual hand in a simulated 3D game environment only by means of EEG brain waves interfaced with the computer. Whilst our system is only a first prototype, we hypothesise that by iteratively improving its design through refinements and tuning based on input from domain experts and testing on real patients, the system can be tailored for being used together with a conventional rehabilitation programme to improve patients’ ability to move the paretic limb much in the same vain as mirror therapy. Our proposed system has several advantages, including being game-based, customisable, adaptive, and extendable. In addition, when compared with conventional rehabilitation methods, our system is extremely low-cost and flexible, in particular because patients can use it in the comfort of their homes, with little or no need for professional human assistance. Preliminary tests are carried out to highlight the potential of the proposed rehabilitation system, however, in order to measure its efficiency in rehabilitation, the system must first be improved and then run through an extensive field test with a sufficiently large group of patients and compared with a control group.

Simulation is an important technique for integrating interacting models for predicting results of hypothetical scenarios. A typical application area for simulators is virtual prototyping (VP). In VP, simulators replace the real-world prototype. Hence, the quality of the virtual prototype depends on the quality of its simulations, which in turn are highly dependent on the quality of the models and the computational power, especially if visualization and/or real-time constraints are required. Unfortunately defining models is an error-prone activity which requires domain-experts to have knowledge about the implementation details and/or IT-technical concerns. In addition, the bigger the dataset, the more computational power is needed, which affects the cost, and in turn, the usability of today’s simulators. To address both of these aspects, we propose a user-friendly, adaptive and scalable agentbased modelling and simulation framework with a hybrid CPU/GPU/FPGA high performance computing platform. The solution we describe provides domain-experts with a a scalable, adaptive, and efficient simulator and enables domain-experts to define high quality models without indepth IT-knowledge. We use a running example from the particle transmission domain to illustrate our approach.

Abstract Metamodelling is one of the pillars of model-driven engineering, used for language engineering and domain modelling. Even though metamodelling is traditionally based on a two-metalevel approach, several researchers have pointed out limitations of this solution and proposed an alternative deep (also called multi-level ) approach to obtain simpler system specifications. However, this approach currently lacks a formalisation that can be used to explain fundamental concepts such as deep characterisation, double linguistic/ontological typing and linguistic extension. This paper provides such a formalisation based on the Diagram Predicate Framework, and discusses its practical realisation in the metaDepth tool.

In Model Driven Engineering (MDE) models are the main artefacts of the software development process. Model transformations are used both in the software development phase and for verification and simulation of the system behaviour. Hence, tools and languages for describing model transformations are essential in MDE. While many practical transformation languages and tools have been proposed, there is still the need for formal foundations of model transformations.

A workflow model is an abstract representation of a real life workflow and consists of interconnected tasks depicting the desired executions of real life activities. Time information is an important aspect of many safety-critical workflows. This paper presents a new formal diagrammatic approach to timed workflow modelling involving principles from model-driven engineering. The approach extends the Diagram Predicate Framework, which is based on category theory and graph transformations, for the specification of workflow modelling formalisms. We develop a transition system to represent the dynamic semantics involving time in which transitions are described by specification transformations between instances. To model time, we use predicates for time delay and duration with transition rules for time advancement.

The raise of the abstraction level of programming languages has resulted in the usage of models and model transformations in software development processes. As a consequence of the usage of models as input to model transformation tools, there is a need for formal modeling languages and formal transformation definition techniques which can be employed to automatically translate between (and integrate) models. Therefore, a major focus of our research is on the formalization of modeling and model transformation in the generic formalism, Diagrammatic Predicate Logic (DPL). In this paper, we discuss a formalization approach to model transformation definitions based on DPL. Then, based on this formalization, some features of model transformations such as traceability, bidirectionality and compositionality are discussed.