PhD Seminar • Formal Methods | Software Engineering • Compositional Analysis of Parameterized Distributed Hybrid Systems

Please note: This PhD seminar will take place in DC 2310.

Raniah Alghamdi, PhD candidate
David R. Cheriton School of Computer Science

Supervisor: Professor Richard Trefler

Distributed hybrid systems have diverse applications across various domains, including cyber-physical systems, multi-agent systems, and robotics. A common feature of these safety-critical systems is that they are modeled as a set of distributed agents that cooperatively interact to accomplish common goals. Formal analysis of such systems is challenging due to their parametrized nature, involving an unbounded number N of interacting agents, as well as their hybrid behavior combining discrete software transitions with continuous dynamic evolution. Additionally, continuous interference among agents can impact local safety. Using the traditional non-parametric model-checking approach to verify the global correctness of distributed hybrid systems leads to the well-known state space explosion problem.

To tackle these challenges, this seminar introduces the parameterized compositional model checking problem (PCMCP) method for analyzing global safety properties of hybrid systems modeled as networks of hybrid I/O automata (HIOA). Combining local symmetry amongst the agents, compositionality, and parametric analysis can avoid the computational cost associated with global analysis of the hybrid system's state space. PCMCP involves analyzing the local symmetry of the agent networks and the agents' continuous interfering interactions with their neighboring agents. This analysis identifies a representative agent (HIOA) from each locally symmetric equivalent class of the system. A key step in this analysis is the calculation of overapproximations of the reachable states set for representative agents in a small cutoff instance of the system that then generalizes to arbitrarily sized HIOA networks. We illustrate this technique by outlining its application to compute a compositional local invariant for a platoon of N cooperative adaptive cruise control (CACC) vehicles. We establish a platoon cutoff and show that our simplified CACC model is collision-free, which then generalizes to the entire platoon family.