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 - Schneider, Sven A1 - Lambers, Leen A1 - Orejas, Fernando T1 - A logic-based incremental approach to graph repair featuring delta preservation JF - International journal on software tools for technology transfer : STTT N2 - We introduce a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing graph repairs from which a user may select a graph repair based on non-formalized further requirements. This incremental approach features delta preservation as it allows to restrict the generation of graph repairs to delta-preserving graph repairs, which do not revert the additions and deletions of the most recent consistency-violating graph update. We specify consistency of graphs using the logic of nested graph conditions, which is equivalent to first-order logic on graphs. Technically, the incremental approach encodes if and how the graph under repair satisfies a graph condition using the novel data structure of satisfaction trees, which are adapted incrementally according to the graph updates applied. In addition to the incremental approach, we also present two state-based graph repair algorithms, which restore consistency of a graph independent of the most recent graph update and which generate additional graph repairs using a global perspective on the graph under repair. We evaluate the developed algorithms using our prototypical implementation in the tool AutoGraph and illustrate our incremental approach using a case study from the graph database domain. KW - Nested graph conditions KW - Graph repair KW - Model repair KW - Consistency KW - restoration KW - Delta preservation KW - Graph databases KW - Model-driven KW - engineering Y1 - 2021 U6 - https://doi.org/10.1007/s10009-020-00584-x SN - 1433-2779 SN - 1433-2787 VL - 23 IS - 3 SP - 369 EP - 410 PB - Springer CY - Berlin ; Heidelberg ER -