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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Robust Structural Transformations for Real-Time Systems

  • Ernst-Rüdiger Olderog,
  • Mani Swaminathan

摘要

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.