Deriving Delay-Robust Timed Graph Transformation System Models

Distributed Cyber-Physical Systems (DCPSs) are omnipresent and their analysis against provided specifications is a central challenge. Hereby, distribution results in communication delays among agents that have to be adequately taken into account by software models to avoid race conditions. However, engineering DCPSs at a higher level of detail by incorporating communication delays explicitly inflates model size and impedes analysis. In this paper, we employ Timed Graph Transformation Systems (TGTSs) to model DCPSs and distinguish between local immediate and remote \(\delta \) -delayed observations, requiring up to \(\delta \) time units. We then (a) demonstrate potential absence of \(\delta \) -delay robustness for TGTS models, (b) provide a procedure widening safe behavioral options of a verified 0-delay system model to derive a \(\delta \) -delay robust TGTS model, and (c) analyze the restrictiveness of the widening and the resulting TGTS model for new unsafe behavior. As a running example, we consider a DCPS in which multiple distributed autonomous shuttles locally coordinate their movement on a track topology to avoid collisions.