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 - THES A1 - Sakizloglou, Lucas T1 - Evaluating temporal queries over history-aware architectural runtime models T1 - Ausführung temporaler Anfragen über geschichtsbewusste Architektur-Laufzeitmodelle N2 - In model-driven engineering, the adaptation of large software systems with dynamic structure is enabled by architectural runtime models. Such a model represents an abstract state of the system as a graph of interacting components. Every relevant change in the system is mirrored in the model and triggers an evaluation of model queries, which search the model for structural patterns that should be adapted. This thesis focuses on a type of runtime models where the expressiveness of the model and model queries is extended to capture past changes and their timing. These history-aware models and temporal queries enable more informed decision-making during adaptation, as they support the formulation of requirements on the evolution of the pattern that should be adapted. However, evaluating temporal queries during adaptation poses significant challenges. First, it implies the capability to specify and evaluate requirements on the structure, as well as the ordering and timing in which structural changes occur. Then, query answers have to reflect that the history-aware model represents the architecture of a system whose execution may be ongoing, and thus answers may depend on future changes. Finally, query evaluation needs to be adequately fast and memory-efficient despite the increasing size of the history---especially for models that are altered by numerous, rapid changes. The thesis presents a query language and a querying approach for the specification and evaluation of temporal queries. These contributions aim to cope with the challenges of evaluating temporal queries at runtime, a prerequisite for history-aware architectural monitoring and adaptation which has not been systematically treated by prior model-based solutions. The distinguishing features of our contributions are: the specification of queries based on a temporal logic which encodes structural patterns as graphs; the provision of formally precise query answers which account for timing constraints and ongoing executions; the incremental evaluation which avoids the re-computation of query answers after each change; and the option to discard history that is no longer relevant to queries. The query evaluation searches the model for occurrences of a pattern whose evolution satisfies a temporal logic formula. Therefore, besides model-driven engineering, another related research community is runtime verification. The approach differs from prior logic-based runtime verification solutions by supporting the representation and querying of structure via graphs and graph queries, respectively, which is more efficient for queries with complex patterns. We present a prototypical implementation of the approach and measure its speed and memory consumption in monitoring and adaptation scenarios from two application domains, with executions of an increasing size. We assess scalability by a comparison to the state-of-the-art from both related research communities. The implementation yields promising results, which pave the way for sophisticated history-aware self-adaptation solutions and indicate that the approach constitutes a highly effective technique for runtime monitoring on an architectural level. N2 - In der modellgetriebenen Entwicklung wird die Adaptation großer Softwaresysteme mit dynamischer Struktur durch Architektur-Laufzeitmodelle ermöglicht. Ein solches Modell stellt einen abstrakten Zustand des Systems als einen Graphen von interagierenden Komponenten dar. Jede relevante Änderung im System spiegelt sich im Modell wider und löst eine Ausführung von Modellanfragen aus, die das Modell nach zu adaptierenden Strukturmustern durchsuchen. Diese Arbeit konzentriert sich auf eine Art von Laufzeitmodellen, bei denen die Ausdruckskraft des Modells und der Modellanfragen erweitert wird, um vergangene Änderungen und deren Zeitpunkt zu erfassen. Diese geschichtsbewussten Modelle und temporalen Anfragen ermöglichen eine fundiertere Entscheidungsfindung während der Adaptation, da sie die Formulierung von Anforderungen an die Entwicklung des Musters, das adaptiert werden soll, unterstützen. Die Ausführung von temporalen Anfragen während der Adaptation stellt jedoch eine große Herausforderung dar. Zunächst müssen Anforderungen an die Struktur sowie an die Reihenfolge und den Zeitpunkt von Strukturänderungen spezifiziert und evaluiert werden. Weiterhin müssen die Antworten auf die Anfragen berücksichtigen, dass das geschichtsbewusste Modell die Architektur eines Systems darstellt, dessen Ausführung fortlaufend sein kann, sodass die Antworten von zukünftigen Änderungen abhängen können. Schließlich muss die Anfrageausführung trotz der zunehmenden Größe der Historie hinreichend schnell und speichereffizient sein---insbesondere bei Modellen, die durch zahlreiche, schnelle Änderungen verändert werden. In dieser Arbeit werden eine Sprache für die Spezifikation von temporalen Anfragen sowie eine Technik für deren Ausführung vorgestellt. Diese Beiträge zielen darauf ab, die Herausforderungen bei der Ausführung temporaler Anfragen zur Laufzeit zu bewältigen---eine Voraussetzung für ein geschichtsbewusstes Architekturmonitoring und geschichtsbewusste Architekturadaptation, die von früheren modellbasierten Lösungen nicht systematisch behandelt wurde. Die besonderen Merkmale unserer Beiträge sind: die Spezifikation von Anfragen auf der Basis einer temporalen Logik, die strukturelle Muster als Graphen kodiert; die Bereitstellung formal präziser Anfrageantworten, die temporale Einschränkungen und laufende Ausführungen berücksichtigen; die inkrementelle Ausführung, die die Neuberechnung von Abfrageantworten nach jeder Änderung vermeidet; und die Option, Historie zu verwerfen, die für Abfragen nicht mehr relevant ist. Bei der Anfrageausführung wird das Modell nach dem Auftreten eines Musters durchsucht, dessen Entwicklung eine temporallogische Formel erfüllt. Neben der modellgetriebenen Entwicklung ist daher die Laufzeitverifikation ein weiteres verwandtes Forschungsgebiet. Der Ansatz unterscheidet sich von bisherigen logikbasierten Lösungen zur Laufzeitverifikation, indem er die Darstellung und Abfrage von Strukturen über Graphen bzw. Graphanfragen unterstützt, was bei Anfragen mit komplexen Mustern effizienter ist. Wir stellen eine prototypische Implementierung des Ansatzes vor und messen seine Laufzeit und seinen Speicherverbrauch in Monitoring- und Adaptationsszenarien aus zwei Anwendungsdomänen mit Ausführungen von zunehmender Größe. Wir bewerten die Skalierbarkeit durch einen Vergleich mit dem Stand der Technik aus beiden verwandten Forschungsgebieten. Die Implementierung liefert vielversprechende Ergebnisse, die den Weg für anspruchsvolle geschichtsbewusste Selbstadaptationslösungen ebnen und darauf hindeuten, dass der Ansatz eine effektive Technik für das Laufzeitmonitoring auf Architekturebene darstellt. KW - architectural adaptation KW - history-aware runtime models KW - incremental graph query evaluation KW - model-driven software engineering KW - temporal graph queries KW - Architekturadaptation KW - geschichtsbewusste Laufzeit-Modelle KW - inkrementelle Ausführung von Graphanfragen KW - modellgetriebene Softwaretechnik KW - temporale Graphanfragen Y1 - 2023 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-604396 ER - TY - BOOK A1 - Giese, Holger A1 - Maximova, Maria A1 - Sakizloglou, Lucas A1 - Schneider, Sven T1 - Metric temporal graph logic over typed attributed graphs N2 - Various kinds of typed attributed graphs are used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformations provide a formal model for defining state sequences. We consider the extended case where time elapses between states and introduce a logic to reason about these sequences. With this logic we express properties on the structure and attributes of states as well as on the temporal occurrence of states that are related by their inner structure, which no formal logic over graphs accomplishes concisely so far. Firstly, we introduce graphs with history by equipping every graph element with the timestamp of its creation and, if applicable, its deletion. Secondly, we define a logic on graphs by integrating the temporal operator until into the well-established logic of nested graph conditions. Thirdly, we prove that our logic is equally expressive to nested graph conditions by providing a suitable reduction. Finally, the implementation of this reduction allows for the tool-based analysis of metric temporal properties for state sequences. N2 - Verschiedene Arten von getypten attributierten Graphen werden benutzt, um Zustände von Systemen in vielen unterschiedlichen Anwendungsbereichen zu beschreiben. Der etablierte Formalismus der Graphtransformationen bietet ein formales Model, um Zustandssequenzen für dynamische Systeme zu definieren. Wir betrachten den erweiterten Fall von solchen Sequenzen, in dem Zeit zwischen zwei verschiedenen Systemzuständen vergeht, und führen eine Logik ein, um solche Sequenzen zu beschreiben. Mit dieser Logik drücken wir zum einen Eigenschaften über die Struktur und die Attribute von Zuständen aus und beschreiben zum anderen temporale Vorkommen von Zuständen, die durch ihre innere Struktur verbunden sind. Solche Eigenschaften können bisher von keiner der existierenden Logiken auf Graphen vergleichbar darstellt werden. Erstens führen wir Graphen mit Änderungshistorie ein, indem wir jedes Graphelement mit einem Zeitstempel seiner Erzeugung und, wenn nötig, seiner Löschung versehen. Zweitens definieren wir eine Logik auf Graphen, indem wir den Temporaloperator Until in die wohl-etablierte Logik der verschachtelten Graphbedingungen integrieren. Drittens beweisen wir, dass unsere Logik gleich ausdrucksmächtig ist, wie die Logik der verschachtelten Graphbedingungen, indem wir eine passende Reduktionsoperation definieren. Zuletzt erlaubt uns die Implementierung dieser Reduktionsoperation die werkzeukbasierte Analyse von metrisch-temporallogischen Eigenschaften für Zustandssequenzen zu führen. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 123 KW - nested graph conditions KW - sequence properties KW - symbolic graphs KW - typed attributed graphs KW - metric temporal logic KW - temporal logic KW - runtime monitoring KW - verschachtelte Anwendungsbedingungen KW - Sequenzeigenschaften KW - symbolische Graphen KW - getypte Attributierte Graphen KW - metrische Temporallogik KW - Temporallogik KW - Runtime-monitoring Y1 - 2018 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-411351 SN - 978-3-86956-433-3 SN - 1613-5652 SN - 2191-1665 IS - 123 PB - Universitätsverlag Potsdam CY - Potsdam ER - TY - BOOK A1 - Giese, Holger A1 - Maximova, Maria A1 - Sakizloglou, Lucas A1 - Schneider, Sven T1 - Metric temporal graph logic over typed attributed graphs BT - extended version N2 - Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas deltabased (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in AutoGraph. Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these STs incrementally with respect to a graph update. N2 - Verschiedene Arten typisierter attributierter Graphen können verwendet werden, um Systemzustände aus einem breiten Bereich von Domänen darzustellen. Für dynamische Systeme können etablierte Formalismen wie die Graphtransformation ein formales Modell für die Definition von Zustandssequenzen liefern. Wir betrachten den Fall, in dem zwischen Zustandsänderungen Zeit vergehen kann, und führen eine Logik ein, die als Metric Temporal Graph Logic (MTGL) bezeichnet wird, um über solche zeitgesteuerten Graphsequenzen zu urteilen. Mit dieser Logik drücken wir Eigenschaften der Struktur und der Attribute von Zuständen sowie des Auftretens von Zuständen über die Zeit aus, die durch ihre innere Struktur miteinander verbunden sind, was bisher keine formale Logik über Graphen präzise bewerkstelligt. Erstens, basierend auf zeitgesteuerten Graphsequenzen als Modelle für die Systemevolution, definieren wir MTGL, indem wir den zeitlichen Operator bis zu einer gewissen Zeitgrenze in die etablierte Logik von (verschachtelten) Graphbedingungen integrieren. Zweitens skizzieren wir, wie eine endliche zeitgesteuerte Diagrammsequenz als einzelnes Diagramm dargestellt werden kann, das alle zeitlichen Änderungen enthält (als Diagramm mit Verlauf bezeichnet), wie die Erfüllung von MTGL-Bedingungen für ein solches Diagramm definiert werden kann, und zeigen, dass beide Darstellungen dieselben MTGL-Bedingungen erfüllen. Drittens zeigen wir, wie MTGL-Bedingungen auf (verschachtelte) Diagrammbedingungen reduziert werden können, und zeigen anhand dieser Reduzierung, dass beide zugrunde liegenden Logiken gleichermaßen aussagekräftig sind. Schließlich stellen wir eine Erweiterung des Tools AutoGraph vor, mit der die Erfüllung der MTGL-Bedingungen für zeitgesteuerte Diagrammsequenzen überprüft werden kann, indem die Erfüllung der (verschachtelten) Diagrammbedingungen überprüft wird, die unter Verwendung der vorgeschlagenen Reduzierung für das Diagramm mit dem Verlauf entsprechend dem zeitgesteuerten Diagramm erhalten wurden. T3 - Technische Berichte des Hasso-Plattner-Instituts für Digital Engineering an der Universität Potsdam - 127 KW - typisierte attributierte Graphen KW - metrisch temporale Graph Logic KW - Spezifikation von gezeiteten Graph Transformationen KW - typed attributed graphs KW - metric termporal graph logic KW - specification of timed graph transformations Y1 - 2019 U6 - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-427522 SN - 978-3-86956-463-0 SN - 1613-5652 SN - 2191-1665 IS - 127 PB - Universitätsverlag Potsdam CY - Potsdam ER -