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.