| Network topologies in distributed and mobile systems can be naturally described using graph-based models. Specifying configurations of such systems is realized by assigning nodes modeling entities in the network to logical locations in the graph. The operational semantics of such models can be formally described using graph transformation systems by modeling the interactive behavior of the entities in the network with rewrite rules. As an example, we model here the movement of autonomous railway shuttles along tracks and the creation of temporary convoys between shuttles.
|
| %mobile device from one network cell to another, or creating temporary local connections between mobile devices.
|
| As a standard approach in formal methods, model checking facilitates the analysis of the dynamics modeled by graph transformation systems. However, in many settings such as in mobile and distributed systems, the model checking yields useful results only if it allows to reason about individual entities, e.g. specific railway shuttles, and their interactive behavior during the execution. Since the existing tools lack support for reasoning about individual entities, we introduce an approach and a toolchain for instance-aware model checking of graph transformation systems. We use \henshin as a modeling language and state space generation tool and \mcrl as model checking back-end.
|
