nach oben

2021 | Buch

Kapitel lesen Erstes Kapitel lesen

Model-Driven Engineering and Software Development

8th International Conference, MODELSWARD 2020, Valletta, Malta, February 25–27, 2020, Revised Selected Papers

herausgegeben von: Slimane Hammoudi, Luís Ferreira Pires, Bran Selić

Verlag: Springer International Publishing

Buchreihe : Communications in Computer and Information Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes thoroughly revised and selected papers from the 8th International Conference on Model-Driven Engineering and Software Development, MODELSWARD 2020, held in Valletta, Malta, in February 2020.

The 15 revised and extended papers presented in this volume were carefully reviewed and selected from 66 submissions. They present recent research results and development activities in using models and model driven engineering techniques for software development. The papers are organized in topical sections on methodologies, processes and platforms; applications and software development; modeling languages, tools and architectures.

Inhaltsverzeichnis

Frontmatter

Methodologies, Processes and Platforms

Frontmatter

The Smart Grid Simulation Framework: Model-Driven Engineering Applied to Cyber-Physical Systems

Abstract

Smart grids are complex systems for which simulation offers a practical way to evaluate and compare multiple solutions before deployment. However, the simulation of a Smart Grid requires the development of heterogeneous models corresponding to electrical, information processing, and telecommunication behaviors. These heterogeneous models must be linked and analyzed together in order to detect the influences on one another and identify emerging behaviors. We apply model-driven engineering to such cyber-physical systems combining physical and digital components and propose SGridSF, the Smart Grid Simulation Framework, which automates tasks in order to ensure consistency between different simulation models. This framework consists mainly of a domain specific language for modeling a cosimulation unit, called CosiML for Cosimulation Modeling Language, a domain specific language for modeling the functional architecture of a Smart Grid, called SGridML for Smart Grid Modeling Language, and a tool implementing different transformation rules to generate the files and scripts for executing a cosimulation. Finally, we illustrate the use of SGridSF on the real use case of an islanded grid implementing diesel and renewable sources, battery storage and intelligent control of the production. We show the sequencing of automatic generation tasks that minimizes the effort and the risk of error at each iteration of the process.

David Oudart, Jérôme Cantenot, Frédéric Boulanger, Sophie Chabridon

Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications

Abstract

This work proposes an alternative hardware design approach that allows the detection of arithmetic overflows at the specification level. The established hardware design approach describes infinite integer types at that level while the model describes finite types. This opens a semantic gap between both levels, which means that arithmetic overflows cannot be detected at the specification level. To address this problem the CompCert integer library is utilized that describes finite integer types as dependent types using the proof assistant Coq. Properties that argue about these finite types can be specified and verified at the specification level. This closes the semantic gap the established hardware design approach suffers from.

Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler

Systematic Synthesis of Energy-Aware Timing Models in Automotive Software Systems

Abstract

In automotive embedded software, functions have several performance requirements such as timing, energy, safety and reliability. For such complex software architectures, an early evaluation and decision on the best set of performance configuration (e.g. timing vs energy trade-offs) could save costly corrections of potential errors in the design. For example, appropriate performance analysis workflows and frameworks if employed already during early design stages, allow us to understand the performance aspects and behavior of the system depending on software and hardware characteristics. The main input required for such analysis is the performance-analysis model based on the underlying design model. In this context, this chapter presents a workflow for synthesis of energy-aware timing analysis models for AUTOSAR-based embedded software systems developed using the Unified Modeling Language (UML)/Systems Modeling Language (SysML) domains. A prototype of the model transformations for the synthesis of the energy-aware timing models and its evaluation in an automotive use case is presented.

Padma Iyenghar

Model-Based Virtual Prototyping of CPS: Application to Bio-Medical Devices

Abstract

Virtual prototyping and co-simulation of mixed analog/ digital embedded systems have emerged as a promising research topic, in particular for designing medical appliances. In the paper, we show how the integration of different, analog and digital, Models of Computation (MoC) within an UML/SysML based environment, can offer an efficient assistance for designing a cyber-physical system in a progressive and systematic manner. For this, we rely on formal verification and abstract simulation on a high abstraction level, and on Multi-MoC virtual prototyping on a lower abstraction level. A realistic echo monitoring system illustrates (i) the method, (ii) the modeling languages, and (iii) the different verification techniques.

Daniela Genius, Ilias Bournias, Ludovic Apvrille, Roselyne Chotin

Applications and Software Development

Frontmatter

ProvAnalyser: A Framework for Scientific Workflows Provenance

Abstract

The increasing ability of data-driven science is resulting in a growing need for applications that are under the control of data-centric workflows, also known as scientific workflows. The focus of this work is on provenance collection for these workflows, necessary to validate the workflow and to determine the quality of generated data products. However, the act of instrumenting a workflow engine for provenance collection is burdensome. This complex task requires adding hooks to the workflow engine to capture provenance, which can cause perturbation in execution. We address the challenge of extracting provenance data in the form of a knowledge graph from the event logs of the workflows to record critical information about the applications and the workflows. We present an ontology-based framework for provenance collection using the event logs of workflow engine. Further, we reduce provenance use cases to SPARQL queries over captured provenance knowledge graph. Performance evaluation demonstrates that the framework is capable of reconstructing complete data and invocation dependency graphs from one or various execution traces.

Anila Sahar Butt, Peter Fitch

A Multi-Model Reviewing Approach for Production Systems Engineering Models

Abstract

Background. In Production Systems Engineering (PSE) models, which describe plants, represent different views on several engineering disciplines (such as mechanical, electrical and software engineering) and may contain up to 10,000s of instance elements, such as concepts, attributes and relationships. Validating these models requires an integrated multi-model view and the domain expertise of human experts related to individual views. Unfortunately, the heterogeneity of disciplines, tools, and data formats makes it hard to provide a technology-independent multi-model view. Aim. In this paper, we aim at improving Multi-Model Reviewing (MMR) capabilities of domain experts based on selected model visualisation methods and mechanisms. Method. We (a) derive requirements for graph-based visualisation to facilitate reviewing multi-disciplinary models; (b) introduce the MMR approach to visualise engineering models for review as hierarchical and linked structures; (c) design an MMR software prototype; and (d) evaluate the prototype based on tasks derived from real-world PSE use cases. For evaluation purposes we compare capabilities of the MMR prototype and a text-based model editor. Results. The MMR prototype enabled performing the evaluation tasks in most cases considerable faster than the standard text-based model editor. Conclusion. The promising results of the MMR approach in the evaluation context warrant empirical studies with a wider range of domain experts and use cases on the usability and usefulness of the MMR approach in practice.

Felix Rinker, Laura Waltersdorfer, Manuel Schüller, Stefan Biffl, Dietmar Winkler

Augmenting Deep Neural Networks with Scenario-Based Guard Rules

Abstract

Deep neural networks (DNNs) are becoming widespread, and can often outperform manually-created systems. However, these networks are typically opaque to humans, and may demonstrate undesirable behavior in corner cases that were not encountered previously. In order to mitigate this risk, one approach calls for augmenting DNNs with hand-crafted override rules. These override rules serve to prevent the DNN from making certain decisions, when certain criteria are met. Here, we build on this approach and propose to bring together DNNs and the well-studied scenario-based modeling paradigm, by encoding override rules as simple and intuitive scenarios. We demonstrate that the scenario-based paradigm can render override rules more comprehensible to humans, while keeping them sufficiently powerful and expressive to increase the overall safety of the model. We propose a method for applying scenario-based modeling to this new setting, and apply it to multiple DNN models. (This paper substantially extends the paper titled “Guarded Deep Learning using Scenario-Based Modeling”, published in Modelsward 2020 [47]. Most notably, it includes an additional case study, extends the approach to recurrent neural networks, and discusses various aspects of the proposed paradigm more thoroughly).

Guy Katz

Modeling Languages, Tools and Architectures

Frontmatter

Resilient Business Process Modeling and Execution Using BPMN and Microservices

Abstract

Process Modeling Languages (PMLs) help to define, structure and organize operational workflows. The Business Process Model and Notation 2.0 (BPMN), one of the most prominent PMLs, allows the definition and execution of process models including distributed participants and systems. An increasing number of BPMN use cases take place in unreliable communication environments, where connectivity may be intermittent or broken. Resilient processes need to avoid failures that may result in process interruptions or complete breakdowns.

Considering the particular requirements of unreliable communication environments, this paper addresses shortcomings when modeling and executing business processes. With resilient BPMN (rBPMN), the BPMN meta model is extended to allow resilient process designs by domain experts. Exemplary realizations of the introduced resilience strategies use state of the art technologies such as microservices and container virtualization. A proof-of-concept implementation illustrates the resilient design and execution of process models, serving as a guide for other use cases exposed to unreliable communication.

Frank Nordemann, Ralf Tönjes, Elke Pulvermüller, Heiko Tapken

Model Transformation from CBM to EPL Rules to Detect Failure Symptoms

Abstract

The increasing complexity of modern systems, cost reduction policies and ever increasing safety requirements are bringing new challenges to the maintenance domain. In many fields, periodic maintenance actions become either insufficient or too expensive. In this context, Condition-Based Maintenance (CBM) strategies, and Prognostics and Health Management (PHM) in particular, are offering an interesting alternative by allowing systems to be maintained only when needed. These strategies rely on a constant monitoring and analysis of the systems operating conditions in order to detect and identify a failure when it occurs and even sometimes beforehand.

Nowadays, two main approaches are explored to detect failures in PHM solutions: one based on machine learning, the other based on expertise and capitalised system knowledge. This work proposes to combine a Complex Event Processing (CEP), to manage incoming data’s volumetry and velocity, with an Expert System (ES) in charge of exploiting the capitalized knowledge. This paper focuses on the configuration of a CEP from rules contained in a CBM ES using a Model Driven Architecture (MDA). This configuration is a challenge, especially regarding the management of rules with temporal parameters and the need for intermediate results to deal with the rule’s complexity.

Alexandre Sarazin, Sebastien Truptil, Aurélie Montarnal, Jérémy Bascans, Xavier Lorca

Verification and Simulation of Time-Domain Properties for Models of Behaviour

Abstract

Modelling and simulation are techniques instrumental in the engineering and design of complex systems. The reason is that both these techniques can anticipate possible failures when corrections are less costly to incorporate. Nevertheless, a correct behaviour is no guarantee, especially with software systems and their ubiquitous modelling notation: state machines. Correctness cannot be guaranteed because semantic gaps result from (1) abstractions in modelling and (2) ambiguities in simulation. Formal verification of a model may thus imply little about the correctness of the implementation. This situation is all the more serious with the emergence of Model-Driven Software Engineering and its penetration in the instrumentation of cyber-physical systems, where verification of time-domain properties of systems is now paramount. We use logic-labelled finite-state machines (LLFSMs), a formalism with a precise semantics. We introduce both model-to-model and model-to-text transformations from LLFSMs to either programming languages or formal-specification languages for model checkers with minimal semantic gaps. We describe a transformation in the Atlas Transformation Language (ATL), producing modules of the NuSMV model checker. The time complexity of this transformation is linear in the total number of states of an arrangement of LLFSMs. The transformation is so faithful that the model checker itself can be used as the execution engine of the LLFSMs models.

Miguel Carrillo, Vladimir Estivill-Castro, David A. Rosenblueth

Domain-Driven Architecture Modeling and Rapid Prototyping with Context Mapper

Abstract

Strategic Domain-driven Design (DDD) has become an established practice for system decomposition and service identification in recent years. The trend towards microservices increased the popularity of DDD patterns such as Subdomain, Bounded Context, Aggregate and Context Map. In our previous work, we presented a Domain-Specific Language (DSL) providing a clear and concise interpretation of the DDD patterns and their combinations. As a machine-readable description of DDD, the DSL establishes a foundation for systematic service decomposition and DDD-based architecture descriptions that can be refactored and refined by model transformations. The DSL and supporting tools are implemented in the open source project Context Mapper. In this extended version of our previous paper we enhance the DSL grammar to allow domain-driven designers to prototype applications rapidly: they can specify user stories and/or use cases in the DSL, and model transformations can then derive Subdomains and Bounded Contexts automatically. The Context Mapper tool chain supports the continuous, iterative specification and evolution of Context Maps and other service design artifacts. Our validation activities included prototyping, action research, and case studies. This paper illustrates such a transformation chain on the basis of one of our case studies.

Stefan Kapferer, Olaf Zimmermann

Abstract Test Execution for Early Testing Activities in Model-Driven Scenarios

Abstract

The continuous improvement of the performance of computing units makes it possible to cope with increasingly complex tasks. This results in more complex software systems. However, the development of such highly complex systems is difficult to achieve using traditional approaches. Concepts like model-driven software development can weaken this problem in these constructive phases. However, new challenges arise for the testing of development artifacts. In order to be able to perform a real shift left of verification and validation tasks towards early phases of development, we present a semi-formal approach that enables users to execute test cases against the system under development (SUD) on the model-level. Grounded on an Integrated Model Basis which is created and maintained during development, test reports are automatically derived. This opens up a wide range of possibilities for early and targeted troubleshooting.

Reinhard Pröll, Noël Hagemann, Bernhard Bauer

A Methodological Assistant for UML and SysML Use Case Diagrams

Abstract

Use case driven analysis is the corner stone of software and systems modeling in UML and SysML, respectively. A use case diagram identifies the main functions to be offered by the system and showcases the interactions between in-system use cases and out-system users. Identifying and organizing use cases requires good abstraction skills. Therefore, many students and industry practitioners face methodological problems in writing good use cases. Many books and tutorials have addressed the subject. Nevertheless, integration of use case elaboration principles into a UML or SysML tool still remains an open issue. This paper proposes solutions and discusses implementation in a methodological assistant named UCCheck. The latter helps use case diagrams designers to rely on formalized rules and reuse of previous diagrams to create and review their use case diagrams. Implemented in Python, UCCheck is interfaced with the free SysML software TTool and with Cameo Systems Modeler, leaving doors open for other UML or SysML tools.

Erika Rizzo Aquino, Pierre de Saqui-Sannes, Rob A. Vingerhoeds

Model-Based Static and Runtime Verification for Ethereum Smart Contracts

Abstract

Distributed ledger technologies, e.g. blockchains, are an innovative solution to the problem of trust between different parties. Smart contracts, programs executing on these ledgers present new challenges given their non-traditional execution context – blockchains. The immutability of smart contracts once they are deployed makes their pre-deployment correctness essential. This can be achieved through verification methods, which attempt to answer conclusively whether the code respects some specification. Another approach is model-driven development, where the specification is used directly to create a correct-by-const-ruction implementation. A specification may however still need to be verified to ensure it satisfies some properties. Verifying properties pre-deployment is ideal, however it may not always be possible to do completely, depending on the complexity of the smart contract. Traditionally upon failure of a verification attempt the only option is to attempt a different verification method. Recent approaches instead enable the transformation of the verification problem into a smaller problem, reducing the load of subsequent verification attempts. We have previously proposed an automata-theoretic approach to reason systematically about this kind of residual analysis for (co-)safety properties, while we have implemented an intraprocedural data-flow approach for Java programs. In this paper we extend our approach for Solidity smart contracts, present a corresponding tool, evaluate the approach with several new case studies, and compare it with existing approaches.

Shaun Azzopardi, Christian Colombo, Gordon Pace

A Novel Family of Queuing Network Models for Self-adaptive Systems

Abstract

A Self-adaptive System (SaS) consists of an autonomic manager which is able to adapt the system’s behavior by operating on a managed sub-system that perceives and affects the environment through its sensors and actuators, respectively. Self-adaptation may occur at different levels, devising a number of knobs that the autonomic manager can properly regulate in order to produce actuation in response to environment sensing.

This paper is an extension of our previous work introducing a generalized QN model that allows performance modeling and assessment of SaSs. We here extend previous work by defining modeling patterns and controller selection policies to conform to during the instantiation of the generalized model, resulting into a novel family of QN models aimed at representing the different parts of the system and the dynamics occurring over and among them.

A controlled experiment addressing a realistic SaS for emergency handling shows that, by adhering to the defined patterns and controller selection policies, QN models behave as expected, and that the latter can be immersed into a performance optimization context that opens to the development of automated solutions to support the identification of efficient system configurations.

Davide Arcelli

Backmatter

Titel: Model-Driven Engineering and Software Development
herausgegeben von: Slimane Hammoudi
Luís Ferreira Pires
Bran Selić
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-67445-8
Print ISBN: 978-3-030-67444-1
DOI: https://doi.org/10.1007/978-3-030-67445-8