Please note: This PhD seminar will take place online.
Raniah Alghamdi, PhD candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Richard Trefler
Cyber-Physical Systems (CPS) applications are seen across various safety-critical domains as a set of distributed agents that cooperatively interact to accomplish common goals. Such distributed hybrid systems are parameterized by N, an unbounded number of interacting agents. Using the traditional non-parametric model-checking approach to verify their correctness is limited to the gradual composition of more agents, leading to the well-known “state-space explosion” problem. Therefore, it is vital to find a scalable method to verify the safety of such massive state space systems, regardless of the number of participating agents. That problem is known as the parameterized model checking problem (PMCP).
This seminar sheds light on both related works and foundational concepts crucial for understanding the complexity of analyzing parametric CPS. Different relevant works in parameterized CPS will be discussed to grasp the current state of the art in this evolving field through real-world applications. Additionally, we will give a comprehensive background on key notions including parametrized compositional model checking problem (PCMCP), hybrid models, hybrid input/output automata (HIOA), networks of HIOA, inductive invariants of HIOA, and local symmetry. Furthermore, developing the modular verification technique of PCMCP to analyze global safety properties of parametric CPS will be briefly discussed. To illustrate the challenges in analyzing parameterized CPS, we will briefly outline its application in a platoon of N cooperative adaptive cruise control (CACC) vehicles.