Vincent Rahli, University of Birmingham.
The accelerated digitalisation of society along with technological evolution have changed the landscape of cyber-physical systems. Two main threats make the reliable and real-time control of these systems challenging: the uncertainty in the communication infrastructure induced by scale and heterogeneity of the environment and devices; and targeted attacks maliciously worsening the impact of the above-mentioned communication uncertainties, disrupting the correctness of real-time applications. We have recently developed broadcast protocols that tackle these challenges by delivering real-time practical performance, while tolerating arbitrary faults, including malicious attacks. In this talk, we will describe these results and present preliminary work towards formally specifying and verifying such protocols. In particular, this involves formalizing non-traditional “quorum systems” and verifying quantitative timeliness properties as opposed to more traditional qualitative properties safety and liveness properties.