Robust Structural Transformations for Real-Time Systems
摘要
In previous work, we introduced structural transformations for data-enriched real-time systems modelled by extended timed automata, aiming at a simplification of the verification of such systems. There we assumed perfectly synchronous clocks proceeding at the same rate across the systems. In this paper, we permit that clocks may be subject to (sufficiently small) bounded drifts. We consider the transformations of layering and of flattening, and show that under reasonable conditions these transformations are robust against such bounded drifts in clocks. We illustrate this using a parameterized version of Fischer’s real-time protocol for mutual exclusion.