Delay-Robustness for Distributed Cyber-Physical System Models

Abstract

Distributed Cyber-Physical Systems operate in dynamic and safety-critical environments where distributed decision-making is affected by observation, execution, and communication delays. To ensure safety, model-based engineering typically verifies initially delay-idealized (i.e., zero-delay) models before deployment. However, introducing delay-related phenomena into executable models substantially increases model complexity and often renders formal verification infeasible, whereas neglecting them may invalidate the correctness guarantees established at the abstract level. This thesis addresses this challenge by investigating how delay-related phenomena can be introduced systematically through model refinement while preserving analyzability and formally established safety properties. To this end, it introduces Delay-Robustness as an intermediate correctness criterion between delay-idealized and delay-explicit models. A model is considered delay-robust if the safety properties established for its delay-idealized representation remain valid after bounded delay phenomena are incorporated through successive refinement steps. This paper outlines the motivation, research objectives, current results, and planned contributions of my PhD research. It summarizes published contributions, outlines further planned contributions, and discusses the remaining research plan toward the completion of the dissertation.