-
Chapter and Conference Paper
Localized RETE for Incremental Graph Queries
The growing size of graph-based modeling artifacts in model-driven engineering calls for techniques that enable efficient execution of graph queries. Incremental approaches based on the RETE algorithm provide ...
-
Chapter and Conference Paper
Deriving Delay-Robust Timed Graph Transformation System Models
Distributed Cyber-Physical Systems (DCPSs) are omnipresent and their analysis against provided specifications is a central challenge. Hereby, distribution results in communication delays among agents that have...
-
Chapter and Conference Paper
Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models
In model-driven engineering, runtime monitoring of systems with complex dynamic structures is typically performed via a runtime model capturing a snapshot of the system state: the model is represented as a gra...
-
Chapter and Conference Paper
Combining Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems
The correct operation of safety-critical cyber-physical systems is crucial. However, such systems often feature a large variability of start configurations, an intractably large state space, a high degree of u...
-
Article
Translation validation of coloured Petri net models of programs on integers
Programs are often subjected to significant optimizing and parallelizing transformations based on extensive dependence analysis. Formal validation of such transformations needs modelling paradigms which can ca...
-
Article
Open AccessIncremental execution of temporal graph queries over runtime models with history and its applications
Modern software systems are intricate and operate in highly dynamic environments for which few assumptions can be made at design-time. This setting has sparked an interest in solutions that use a runtime model...
-
Chapter and Conference Paper
Invariant Analysis for Multi-agent Graph Transformation Systems Using k-Induction
The analysis of behavioral models such as Graph Transformation Systems (GTSs) is of central importance in model-driven engineering. However, GTSs often result in intractably large or even infinite state spaces...
-
Chapter and Conference Paper
Towards Development with Multi-version Models: Detecting Merge Conflicts and Checking Well-Formedness
Develo** complex software requires that multiple views and versions of the software can be developed in parallel and merged as supported by views and managed by version control systems. In this context, this...
-
Chapter and Conference Paper
Probabilistic Metric Temporal Graph Logic
Cyber-physical systems often encompass complex concurrent behavior with timing constraints and probabilistic failures on demand. The analysis whether such systems with probabilistic timed behavior adhere to a ...
-
Article
Open AccessFormal testing of timed graph transformation systems using metric temporal graph logic
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. Forma...
-
Chapter and Conference Paper
Kee** Pace with the History of Evolving Runtime Models
Structural runtime models provide a snapshot of the constituents of a system and their state. Capturing the history of runtime models, i.e., previous snapshots, has been shown to be useful for a number of aims...
-
Chapter and Conference Paper
Compositional Analysis of Probabilistic Timed Graph Transformation Systems
The analysis of behavioral models is of high importance for cyber-physical systems, as the systems often encompass complex behavior based on e.g. concurrent components with mutual exclusion or probabilistic fa...
-
Chapter and Conference Paper
Host-Graph-Sensitive RETE Nets for Incremental Graph Pattern Matching
Efficient querying of large graph structures is a problem at the heart of several application domains such as social networks and model driven engineering. In particular in the context of model driven engineer...
-
Chapter and Conference Paper
Interval Probabilistic Timed Graph Transformation Systems
For complex distributed embedded probabilistic real-time systems, ensuring correctness of their software components is of great importance. The rule-based formalism of Probabilistic Timed Graph Transformation ...
-
Chapter and Conference Paper
On the Complexity of Simulating Probabilistic Timed Graph Transformation Systems
To develop future cyber-physical systems, like networks of autonomous vehicles, the modeling and simulation of huge networks of collaborating systems acting together on large-scale topologies is required. Prob...
-
Chapter and Conference Paper
A Simulator for Probabilistic Timed Graph Transformation Systems with Complex Large-Scale Topologies
Future cyber-physical systems, like networks of autonomous vehicles, will result in a huge number of collaborating systems acting together on large-scale topologies. Modeling them requires capturing timed and...
-
Chapter and Conference Paper
Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic
The nonpropositional Metric Temporal Graph Logic (MTGL) specifies the behavior of timed dynamic systems given by timed graph sequences (TGSs), which contain typed attributed graphs representing system states and ...
-
Chapter and Conference Paper
Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions
The behavior of various kinds of dynamic systems can be formalized using typed attributed graph transformation systems (GTSs). The states of these systems are then modelled using graphs and the evolution of th...
-
Article
Open AccessAutomatic verification of behavior preservation at the transformation level for relational model transformation
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 intro...
-
Chapter and Conference Paper
Metric Temporal Graph Logic over Typed Attributed Graphs
Various kinds of typed attributed graphs can be used to represent states of systems from a broad range of domains. For dynamic systems, established formalisms such as graph transformation can provide a formal ...
