Modeling and analysis of cyber-physical systems is a challenge for formal methods and an active area of research. Initially developed for the analysis of the safety properties of autonomous vehicles (see [1]), the HOL-Cyberphy framework, based on the Isabelle/HOL proof assistant, has been generalized to model multi-agent cyber-physical systems. . The objective of this internship is to study this framework, notably based on the use of an Isabelle theory of Communicating Sequential Processes (see [2]), and to adapt it to the modeling of cyber-multi-agent systems. communicating physics, in order to analyze and prove their proper functioning properties. We can particularly draw inspiration from the work of André Platzer in this area (see [3]).
Missions:
- Constitute a state of the art on the formal modeling of communicating cyber-physical multi-agent systems;
- Take charge of the Isabelle HOL-CyberPhy framework, by creating some models of single and multi-agent cyber-physical systems;
- Design a generic model of communicating cyber-physical multi-agent systems based on case studies to be identified, and propose an adaptation of the HOL-CyberPhy framework accordingly.
Bibliographic references on the subject:
- [1] Paolo Crisafulli, Safouan Taha, Burkhart Wolff. Modeling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP. Research Report 1, University Paris-Saclay; IRT SystemX, Palaiseau. 2021, pp.81. URL:
- [2] Taha S., Ye L., Wolff B.: HOL-CSP Version 2.0. Archive of Formal Proofs (2019).
- [3] Brieger, Marvin & Mitsch, Stefan & Platzer, André. (2023). Dynamic Logic of Communicating Hybrid Programs
The internship may lead to recruitment for a thesis, on the subject described here