Stage R&D : Modélisation formelle de systèmes multi-agents cyber-physiques communicants  – Analyse et preuves de propriétés

Contexte du stage

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.
Vous travaillerez au sein du projet CVH (Chaîne Outillée pour la Validation et l’Homologation du véhicule  automatisé connecté), en partenariat avec Airbus Protect, AVSimulation, OKTAL-SE, Renault Group, Stellantis, Valeo et le Laboratoire Méthodes Formelles (LMF, ENS Paris-Saclay). 

Présentation du sujet

Contexte projet
Lancé en 2023 pour une durée de 4 ans, le projet CVH (Chaîne outillée pour la Validation et l’Homologation du véhicule automatisé connecté) vise à améliorer la méthodologie et l’outillage pour la validation des véhicules automatisés (VA) connectés, en respect des exigences réglementaires et normatives.
Il vise notamment à constituer un cadre d’ingénierie pour la safety du VA fondé sur la preuve formelle, simplifiant considérablement les étapes de conception et de validation (réduction d’effort et coûts), en lui donnant des critères de safety mesurables et atteignables, en particulier au travers d’une méthode d’optimisation des plans de test. 

Objectifs
La modélisation et l’analyse des systèmes cyber-physiques est un défi pour les méthodes formelles et un domaine de recherche très actif. Initialement élaboré pour l’analyse des propriétés de sûreté des véhicules autonomes [1], le framework HOL-Cyberphy, fondé sur l’assistant de preuve Isabelle/HOL, a été généralisé pour modéliser des systèmes cyber-physiques multi-agents.
La finalité du stage est de contribuer au déploiement de véhicules et systèmes de transport autonomes offrant des garanties formelles de sûreté de fonctionnement. Pour ce faire, l’objectif su stage du stage est d’étudier le framework HOL-CyberPhy, notamment fondé sur l’utilisation d’une théorie Isabelle pour les Communicating Sequential Processes [2][4], et de l’adapter à la modélisation de scénarios automobiles impliquant plusieurs véhicules et équipements communicants, afin d’en analyser et prouver des propriétés de fonctionnement sûr. On pourra notamment s’inspirer des travaux d’André Platzer dans ce domaine [3]. 

Missions 

• Constituer un état de l’art sur la modélisation formelle des systèmes multi-agents cyber-physiques communicants ; 
• Prendre en main le framework Isabelle HOL-CyberPhy, en réalisant quelques modèles de systèmes cyber-physiques mono et multi-agents ; 
• Concevoir un modèle générique de systèmes multi-agents cyber-physiques communicants à partir de scénarios automobiles à identifier avec les partenaires du projet CVH, et proposer une adaptation du framework HOL-CyberPhy en conséquence. 

Le stage pourra déboucher sur un recrutement en thèse.  

Références bibliographiques
[1] Paolo Crisafulli, Safouan Taha, Burkhart Wolff. Modelling and Proving Safety in Autonomous Cars Scenarios in HOL-CSP. [Research Report] 1, University Paris-Saclay; IRT SystemX, Palaiseau. 2021, pp.81. URL : https://hal.inria.fr/hal-03429597v2
[2] Taha S., Ye L., Wolff B.: HOL-CSP Version 2.0. Archive of Formal Proofs (2019). http://isa-afp.org/entries/HOL-CSP.html
[3] Brieger, Marvin & Mitsch, Stefan & Platzer, André. (2023). Dynamic Logic of Communicating Hybrid Programs. https://arxiv.org/abs/2302.14546
[4] S. D. Brookes & A. W. Roscoe (2005) An improved failures model for communicating processes. International Conference on Concurrency. https://www.cs.ox.ac.uk/people/bill.roscoe/publications/9.pdf 

Profil et compétences

De formation bac +5 Master Recherche ou Ingénieur en Informatique. 

Compétences :  

• Bonne formation en informatique, analyse mathématique et programmation fonctionnelle ainsi qu’un intérêt pour les outils de preuve formelle. 
• Notions d’algèbres de processus (en particulier Communicating Sequential Processes). 
• La connaissance du framework HOL/Isabelle est un plus. 
• Un bon niveau d’anglais est indispensable. 

Aptitudes personnelles:

• Intérêt avéré pour la recherche 
• Goût pour la prise en compte de problématiques industrielles et de leurs traductions en questions scientifiques. 
• Travail en équipe. 

Merci d’indiquer la référence du stage dans l’objet de votre mail de candidature, d’y joindre CV, lettre de motivation et relevés de notes.