Safety and progress for distributed cyber-physical systems with unreliable communication

Cyber-physical systems (CPSs) may interact and manipulate objects in the physical world, and therefore formal guarantees about their behavior are strongly desired. Static-time proofs of safety invariants, however, may be intractable for systems with distributed physical-world interactions. This is further complicated when realistic communication models are considered, for which there may not be bounds on message delays, or even when considering that messages will eventually reach their destination. In this work, we address the challenge of proving safety and progress in distributed CPSs communicating over an unreliable communication layer. We show that for this type of communication model, system safety is closely related to the results of a hybrid system's reachability computation, which can be computed at runtime. However, since computing reachability at runtime may be computationally intensive, we provide an approach that moves significant parts of the computation to design time. This approach is demonstrated with a case study of a simulation of multiple vehicles moving within a shared environment.