Abstract The correct operation of safety-critical distributed embedded systems is crucial. Following a model-driven approach, the relevant system aspects must be captured and rigorous ideally fully-automatic analysis of (probabilistic) timed safety properties must be supported. Probabilistic Timed Graph Transformation Systems (PTGTSs) support the modeling of such systems and analysis of such properties via model checking or simulation. However, they only support the modeling of probabilistic choice with a fixed numbers of outcomes and non-deterministic timing delays via timing constraints limiting applicability (descriptive expressiveness) and usefulness (precision of analysis results). To remedy this drawback of PTGTSs, we (a) extend PTGTSs to Stochastic Timed Graph Transformation Systems (STGTSs) integrating discrete/continuous random variables to capture stochastic behavior and (b) outline an adaptation of PTGTS model checking for STGTSs to enable analysis w.r.t. probabilistic timed safety properties. Relying on a running example in which shuttles navigating on a track topology must avoid derailing, we exemplify STGTS support for modeling and analysis.

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 failures on demand. The rule-based formalism of Probabilistic Timed Graph Transformation Systems (PTGTSs) is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces. We present an approach for the analysis of large-scale systems modeled as PTGTSs by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large-scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large-scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large-scale system under analysis. We consider a running example in which shuttles drive on tracks of a large-scale topology and autonomously coordinate their local behavior with other shuttles nearby. For this running example, we verify that (a) shuttles can always make the expected forward progress using several properties, (b) shuttles never collide, and (c) shuttles are unlikely to execute emergency brakes in two scenarios. In our evaluation, we apply an implementation of our approach in the tool AutoGraph to our running example.

Abstract 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 failures on demand. The rule-based formalism of probabilistic timed graph transformation systems is a suitable choice when the models representing states of the system can be understood as graphs and timed and probabilistic behavior is important. However, model checking PTGTSs is limited to systems with rather small state spaces. We present an approach for the analysis of large-scale systems modeled as probabilistic timed graph transformation systems by systematically decomposing their state spaces into manageable fragments. To obtain qualitative and quantitative analysis results for a large-scale system, we verify that results obtained for its fragments serve as overapproximations for the corresponding results of the large-scale system. Hence, our approach allows for the detection of violations of qualitative and quantitative safety properties for the large-scale system under analysis. We consider a running example in which we model shuttles driving on tracks of a large-scale topology and for which we verify that shuttles never collide and are unlikely to execute emergency brakes. In our evaluation, we apply an implementation of our approach to the running example.

Abstract 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.

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 model for defining state sequences. We consider the case where time may elapse between state changes and introduce a logic, called Metric Temporal Graph Logic (MTGL), to reason about such timed graph sequences. With this logic, we express properties on the structure and attributes of states as well as on the occurrence of states over time that are related by their inner structure, which no formal logic over graphs concisely accomplishes so far. Firstly, based on timed graph sequences as models for system evolution, we define MTGL by integrating the temporal operator until with time bounds into the well-established logic of (nested) graph conditions. Secondly, we outline how a finite timed graph sequence can be represented as a single graph containing all changes over time (called graph with history), how the satisfaction of MTGL conditions can be defined for such a graph and show that both representations satisfy the same MTGL conditions. Thirdly, we present how MTGL conditions can be reduced to (nested) graph conditions and show using this reduction that both underlying logics are equally expressive. Finally, we present an extension of the tool $$\textsc {AutoGraph}$$ allowing to check the satisfaction of MTGL conditions for timed graph sequences, by checking the satisfaction of the (nested) graph conditions, obtained using the proposed reduction, for the graph with history corresponding to the timed graph sequence.