Niveau: M2, Postdoc

Contact: Burkhart Wolff

Lire la description du stage en pdf.

Contexte

Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, ce centre a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques.

Vous serez encadré par un ingénieur chercheur SystemX du domaine Sûreté de Fonctionnement, et vous aurez des échanges avec des chercheurs du Laboratoire Méthodes Formelles (LMF), notamment B. Wolff et S. Taha.

Vous travaillerez au sein du projet de recherche SystemX 3SA – Simulation pour la Sécurité des systèmes du véhicule Autonome – dont les partenaires industriels sont Apsys, AVsimulation, Expleo, Stellantis, Oktal-SE, Renault, SECTOR Group, Valeo et les partenaires académiques le CEA (Commissariat à l’Energie Atomique), le LNE (Laboratoire national de métrologie et d'essais) et le LMF (Laboratoire Méthodes Formelles).

Le poste est basé à l’IRT SystemX – 2, Boulevard Thomas Gobert 91120 Palaiseau.

Durée et date de démarrage

Read more...

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:

1. Constitute a state of the art on the formal modeling of communicating cyber-physical multi-agent systems;
2. Take charge of the Isabelle HOL-CyberPhy framework, by creating some models of single and multi-agent cyber-physical systems;
3. 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