TY - GEN A1 - Giese, Holger A1 - Henkler, Stefan A1 - Hirsch, Martin T1 - A multi-paradigm approach supporting the modular execution of reconfigurable hybrid systems N2 - Advanced mechatronic systems have to integrate existing technologies from mechanical, electrical and software engineering. They must be able to adapt their structure and behavior at runtime by reconfiguration to react flexibly to changes in the environment. Therefore, a tight integration of structural and behavioral models of the different domains is required. This integration results in complex reconfigurable hybrid systems, the execution logic of which cannot be addressed directly with existing standard modeling, simulation, and code-generation techniques. We present in this paper how our component-based approach for reconfigurable mechatronic systems, M ECHATRONIC UML, efficiently handles the complex interplay of discrete behavior and continuous behavior in a modular manner. In addition, its extension to even more flexible reconfiguration cases is presented. T3 - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 410 KW - code generation KW - hybrid systems KW - reconfigurable systems KW - simulation Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-402896 ER - TY - BOOK A1 - Dyck, Johannes A1 - Giese, Holger A1 - Lambers, Leen T1 - Automatic verification of behavior preservation at the transformation level for relational model transformation N2 - The correctness of model transformations is a crucial element for model-driven engineering of high quality software. In particular, behavior preservation is the most important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques either show that specific properties are preserved, or more generally and complex, they show some kind of behavioral equivalence or refinement between source and target model of the transformation. Both kinds of behavior preservation verification goals have been presented with automatic tool support for the instance level, i.e. for a given source and target model specified by the model transformation. However, up until now there is no automatic verification approach available at the transformation level, i.e. for all source and target models specified by the model transformation. In this report, we extend our results presented in [27] and outline a new sophisticated approach for the automatic verification of behavior preservation captured by bisimulation resp. simulation for model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we show that the behavior preservation problem can be reduced to invariant checking for graph transformation and that the resulting checking problem can be addressed by our own invariant checker even for a complex example where a sequence chart is transformed into communicating automata. We further discuss today's limitations of invariant checking for graph transformation and motivate further lines of future work in this direction. N2 - Die Korrektheit von Modelltransformationen ist von zentraler Wichtigkeit bei der Anwendung modellgetriebener Softwareentwicklung für die Entwicklung hochqualitativer Software. Insbesondere verhindert Verhaltensbewahrung als wichtigste Korrektheitseigenschaft die Entstehung semantischer Fehler während des modellgetriebenen Entwicklungsprozesses. Techniken zur Verifikation von Verhaltensbewahrung zeigen, dass bestimmte spezifische Eigenschaften bewahrt bleiben oder, im allgemeineren und komplexeren Fall, dass eine Form von Verhaltensäquivalenz oder Verhaltensverfeinerung zwischen Quell- und Zielmodell der Transformation besteht. Für beide Ansätze existieren automatisierte Werkzeuge für die Verifikation auf der Instanzebene, also zur Überprüfung konkreter Paare aus Quell- und Zielmodellen der Transformation. Allerdings existiert kein automatischer Verifikationsansatz, der auf der Transformationsebene arbeitet, also Aussagen zu allen Quell- und Zielmodellen einer Modelltransformation treffen kann. Dieser Bericht erweitert unsere Vorarbeit und Ergebnisse aus [27] und stellt einen neuen Ansatz zur automatischen Verifikation von Verhaltensbewahrung vor, der auf Bisimulation bzw. Simulation basiert. Dabei werden Modelltransformationen durch Triple-Graph-Grammatiken und Verhaltensdefinitionen mittels Graphtransformationsregeln beschrieben. Insbesondere weisen wir nach, dass das Problem der Verhaltensbewahrung durch Bisimulation auf Invariant-Checking für Graphtransformationssysteme reduziert werden kann und dass das entstehende Invariant-Checking-Problem für ein komplexes Beispiel durch unser Werkzeug zur Verifikation induktiver Invarianten gelöst werden kann. Das Beispiel beschreibt die Transformation von Sequenzdiagrammen in Systeme kommunizierender Automaten. Darüber hinaus diskutieren wir bestehende Einschränkungen von Invariant-Checking für Graphtransformationssysteme und Ansätze für zukünftige Arbeiten in diesem Bereich. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 112 KW - model transformation KW - behavior preservation KW - semantics preservation KW - relational model transformation KW - bisimulation KW - simulation KW - invariant checking KW - transformation level KW - behavioral equivalenc KW - behavioral refinement KW - behavioral abstraction KW - graph transformation systems KW - graph constraints KW - triple graph grammars KW - Modelltransformationen KW - Verhaltensbewahrung KW - relationale Modelltransformationen KW - Bisimulation KW - Simulation KW - Invariant-Checking KW - Transformationsebene KW - Verhaltensäquivalenz KW - Verhaltensverfeinerung KW - Verhaltensabstraktion KW - Graphtransformationssysteme KW - Graph-Constraints KW - Triple-Graph-Grammatiken Y1 - 2017 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-100279 SN - 978-3-86956-391-6 SN - 1613-5652 SN - 2191-1665 IS - 112 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - JOUR A1 - Ghahremani, Sona A1 - Giese, Holger T1 - Evaluation of self-healing systems BT - An analysis of the state-of-the-art and required improvements JF - Computers N2 - Evaluating the performance of self-adaptive systems is challenging due to their interactions with often highly dynamic environments. In the specific case of self-healing systems, the performance evaluations of self-healing approaches and their parameter tuning rely on the considered characteristics of failure occurrences and the resulting interactions with the self-healing actions. In this paper, we first study the state-of-the-art for evaluating the performances of self-healing systems by means of a systematic literature review. We provide a classification of different input types for such systems and analyse the limitations of each input type. A main finding is that the employed inputs are often not sophisticated regarding the considered characteristics for failure occurrences. To further study the impact of the identified limitations, we present experiments demonstrating that wrong assumptions regarding the characteristics of the failure occurrences can result in large performance prediction errors, disadvantageous design-time decisions concerning the selection of alternative self-healing approaches, and disadvantageous deployment-time decisions concerning parameter tuning. Furthermore, the experiments indicate that employing multiple alternative input characteristics can help with reducing the risk of premature disadvantageous design-time decisions. KW - self-healing KW - failure model KW - performance KW - simulation KW - evaluation Y1 - 2020 U6 - https://doi.org/10.3390/computers9010016 SN - 2073-431X VL - 9 IS - 1 PB - MDPI CY - Basel ER -