Compositional Analysis of Parametric Cooperative Cyber-Physical Systems
This paper studies the parameterized compositional model checking problem (PCMCP) for analyzing global safety properties of cooperative Cyber-Physical Systems modeled as networks of hybrid automata. We develop the modular verification technique of PCMCP to analyze global safety properties of parametric models of distributed cooperative agents, where each agent is modeled as a hybrid I/O automaton (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.
Sun 14 AprDisplayed time zone: Lisbon change
16:00 - 17:30 | Formal methods for cyber-physical systems and requirements engineeringFormaliSE 2024 at Eugénio de Andrade Chair(s): Cristian Cadar Imperial College London | ||
16:00 30mTalk | Automated Repair of Violated Eventually Properties in Concurrent Programs FormaliSE 2024 Irman Faqrizal Univ. Grenoble Alpes, CNRS, Grenoble INP, Inria, LIG, Grenoble, France, Quentin Nivon Univ. Grenoble Alpes, CNRS, Grenoble INP, Inria, LIG, Grenoble, France, Gwen Salaün University of Grenoble Alpes | ||
16:30 30mTalk | Compositional Analysis of Parametric Cooperative Cyber-Physical Systems FormaliSE 2024 Raniah Alghamdi University of Waterloo and King Abdulaziz University, Richard Trefler University of Waterloo | ||
17:00 30mTalk | Formal Methods in Requirements Engineering: Survey and Future Directions FormaliSE 2024 Robert Lorch GE Research, Baoluo Meng GE Research, Kit Siu GE Research, Abha Moitra General Electric Research, Michael Durling GE Research, Saswata Paul GE Research, Sarat Chandra Varanasi GE Research, Craig McMillan GE Aerospace |