FormaliSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
co-located with ICSE 2024

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 Apr

Displayed 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
30m
Talk
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
30m
Talk
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
30m
Talk
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