Reachability Analysis on Timed Graph Transformation Systems

Abstract

In recent years, software increasingly exhibits self-* properties like selfoptimization
or self-healing. Such properties require reconfiguration at runtime in
order to react to changing environments or detected defects. A reconfiguration might
add or delete components as well as it might change the communication topology of
the system. Considering communication protocols between an arbitrary number of
participants, reconfiguration and state-based protocol behavior are no longer independent
from each other and need to be verified based on a common formalism. Additionally,
such protocols often contain timing constraints to model real-time properties.
These are of integral importance for the safety of the modeled system and thus
need to be considered during the verification of the protocol. In current approaches
either reconfigurations or timing constraints are not considered. Existing approaches
for the verification of timed graph transformation systems lack important constructs
needed for the verification of state-based real-time protocol behaviors. As a first
step towards a solution to this problem, we introduced Timed Story Driven Modeling
[HHH10] as a common formalism integrating state-based real-time protocol
behaviors and system reconfigurations based on graph transformations.

In this paper, we introduce a framework allowing to perform reachability analysis
based on Timed Story Driven Modeling. The framework allows to compute the
reachable timed graph transition system based on an initial graph and a set of timed
transformation and invariant rules.