TY - JOUR A1 - Schneider, Sven A1 - Maximova, Maria A1 - Sakizloglou, Lucas A1 - Giese, Holger T1 - Formal testing of timed graph transformation systems using metric temporal graph logic JF - International journal on software tools for technology transfer N2 - Embedded real-time systems generate state sequences where time elapses between state changes. Ensuring that such systems adhere to a provided specification of admissible or desired behavior is essential. Formal model-based testing is often a suitable cost-effective approach. We introduce an extended version of the formalism of symbolic graphs, which encompasses types as well as attributes, for representing states of dynamic systems. Relying on this extension of symbolic graphs, we present a novel formalism of timed graph transformation systems (TGTSs) that supports the model-based development of dynamic real-time systems at an abstract level where possible state changes and delays are specified by graph transformation rules. We then introduce an extended form of the metric temporal graph logic (MTGL) with increased expressiveness to improve the applicability of MTGL for the specification of timed graph sequences generated by a TGTS. Based on the metric temporal operators of MTGL and its built-in graph binding mechanics, we express properties on the structure and attributes of graphs as well as on the occurrence of graphs over time that are related by their inner structure. We provide formal support for checking whether a single generated timed graph sequence adheres to a provided MTGL specification. Relying on this logical foundation, we develop a testing framework for TGTSs that are specified using MTGL. Lastly, we apply this testing framework to a running example by using our prototypical implementation in the tool AutoGraph. KW - formal testing KW - typed attributed symbolic graphs KW - timed graph KW - transformation KW - graph conditions KW - metric temporal graph logic Y1 - 2021 U6 - https://doi.org/10.1007/s10009-020-00585-w SN - 1433-2779 SN - 1433-2787 VL - 23 IS - 3 SP - 411 EP - 488 PB - Springer CY - Heidelberg ER - TY - JOUR A1 - Maximova, Maria A1 - Giese, Holger A1 - Krause, Christian T1 - Probabilistic timed graph transformation systems JF - Journal of Logical and Algebraic Methods in Programming N2 - Today, software has become an intrinsic part of complex distributed embedded real-time systems. The next generation of embedded real-time systems will interconnect the today unconnected systems via complex software parts and the service-oriented paradigm. Due to these interconnections, the architecture of systems can be subject to changes at run-time, e.g. when dynamic binding of service end-points is employed or complex collaborations are established dynamically. However, suitable formalisms and techniques that allow for modeling and analysis of timed and probabilistic behavior of such systems as well as of their structure dynamics do not exist so far. To fill the identified gap, we propose Probabilistic Timed Graph Transformation Systems (PTGTSs) as a high-level description language that supports all the necessary aspects of structure dynamics, timed behavior, and probabilistic behavior. We introduce the formal model of PTGTSs in this paper as well as present and formally verify a mapping of models with finite state spaces to probabilistic timed automata (PTA) that allows to use the PRISM model checker to analyze PTGTS models with respect to PTCTL properties. (C) 2018 Elsevier Inc. All rights reserved. KW - Graph transformations KW - Probabilistic timed automata KW - PTCTL KW - PRISM model checker KW - HENSHIN Y1 - 2018 U6 - https://doi.org/10.1016/j.jlamp.2018.09.003 SN - 2352-2208 VL - 101 SP - 110 EP - 131 PB - Elsevier CY - New York ER - TY - GEN A1 - Brand, Thomas A1 - Giese, Holger T1 - Generic adaptive monitoring based on executed architecture runtime model queries and events T2 - IEEE Xplore N2 - Monitoring is a key functionality for automated decision making as it is performed by self-adaptive systems, too. Effective monitoring provides the relevant information on time. This can be achieved with exhaustive monitoring causing a high overhead consumption of economical and ecological resources. In contrast, our generic adaptive monitoring approach supports effectiveness with increased efficiency. Also, it adapts to changes regarding the information demand and the monitored system without additional configuration and software implementation effort. The approach observes the executions of runtime model queries and processes change events to determine the currently required monitoring configuration. In this paper we explicate different possibilities to use the approach and evaluate their characteristics regarding the phenomenon detection time and the monitoring effort. Our approach allows balancing between those two characteristics. This makes it an interesting option for the monitoring function of self-adaptive systems because for them usually very short-lived phenomena are not relevant. Y1 - 2019 SN - 978-1-7281-2731-6 U6 - https://doi.org/10.1109/SASO.2019.00012 SN - 1949-3673 SP - 17 EP - 22 PB - IEEE CY - New York ER - TY - JOUR A1 - Dyck, Johannes A1 - Giese, Holger A1 - Lambers, Leen T1 - Automatic verification of behavior preservation at the transformation level for relational model transformation JF - Software and systems modeling N2 - The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp.simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata. KW - Relational model transformation KW - Formal verification of behavior preservation KW - Behavioral equivalence and refinement KW - Bisimulation and simulation KW - Graph transformation KW - Triple graph grammars KW - Invariant checking Y1 - 2018 U6 - https://doi.org/10.1007/s10270-018-00706-9 SN - 1619-1366 SN - 1619-1374 VL - 18 IS - 5 SP - 2937 EP - 2972 PB - Springer CY - Heidelberg ER -