Reachability Analysis on Timed Graph Transformation Systems - Heinzemann, Christian; Suck, Julian; Eckardt, Tobias (Electronic Communications of the EASST, 2011)
In recent years, software increasingly exhibits self-* properties like selfoptimizationor self-healing. Such properties require reconfiguration at runtime inorder to react to changing environments or detected defects. A reconfiguration mightadd or delete components as well as it might change the communication topology ofthe system. Considering communication protocols between an arbitrary number ofparticipants, reconfiguration and state-based protocol behavior are no longer independentfrom 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 thusneed to be considered during the verification of the protocol. In current approacheseither reconfigurations or timing constraints are not considered. Existing approachesfor the verification of timed graph transformation systems lack important constructsneeded for the verification of state-based real-time protocol behaviors. As a firststep towards a solution to this problem, we introduced Timed Story Driven Modeling[HHH10] as a common formalism integrating state-based real-time protocolbehaviors and system reconfigurations based on graph transformations.In this paper, we introduce a framework allowing to perform reachability analysisbased on Timed Story Driven Modeling. The framework allows to compute thereachable timed graph transition system based on an initial graph and a set of timedtransformation and invariant rules.