Bonjour à tous,
Je suis un utilisateur de Coq de longue date, mais j’utilise également d’autres outils de preuves formelle; aujourd’hui nous collaborons avec Burkhart Wolff sur Isabelle/HOL pour la validation de systèmes cyber-physiques, et je me permet de laisser ici une offre de thèse pour ce projet.
Si certains étudiants utilisateurs de Coq sont intéressés dans une thèse avec de la preuve formelle, leur candidature serait très appréciée, et je n’ai aucun doute qu’il serait tout à fait à leur portée de se reconvertir dans un autre assistant de preuve, comme je l’ai (partiellement) fait. De plus je crois que c’est réellement enrichissant d’être capable de manier différents outils de preuve. Cela permet d’éviter de s’enfermer dans les aspects techniques d’un seul outil, et surtout d’éviter le néfaste état d’esprit “de chapelle”, qui ne rend certainement pas service à la science.
Voilà pour l’explication, je laisse l’offre de thèse ci-dessous.
Adrien Durier (Laboratoire des Méthodes Formelles, Université Paris-Saclay)
=======
(Please find the French version below)
This offer is further detailed here:
https://adum.fr/download.pl?tk=PyEJzvew7H224x1CFK9NkuYegmaKR21lCo9nT66NDcq8qnwsGdmVrud2WfD4xb5G
Context
As Cyber-Physical Systems (CPS) such as robots or Autonomous Vehicles (AV) are a developing industrial field, the need for safety certification is widening. Therefore, there is an important opportunity for formal methods to address this type of systems and a need to meet the respective scientific
challenges. It turns out that Communicating Sequential Processes (CSP) standard refinement notions can be adapted to meaningful notions in the CPS domain, notably to communication and interaction as well as a particular discretized/sampled view of continuous variables. This thesis will rely on a framework based on CSP, developed for modeling and formally analyzing CPSs in general and concrete instances in the form of case studies from the AV domain.
This thesis is offered as part of a collaboration between the Institute of Technology Research SystemX (IRT SystemX, Palaiseau) and the Formal Methods Laboratory (LMF) at the University of Paris-Saclay, within the Automated Connected Vehicle Validation and Homologation Toolchain (CVH) project.
Objectives
Study of AV driving strategies taking into account:
- complex dynamics (eg. external accelerations and forces, …)
- approximations of topologies (e.g curves and lanes, … )
- partial perceptions of the global scene (e.g. occluded obstacles and
actors) - liveness of trajectories in (more) complex topologies.
Prerequisites
Good background in mathematical analysis and functional programming as well as an interest in formal proof with Isabelle/HOL.
Application
To apply, please send the following items to both burkhart.wolff@universite-paris-saclay.fr> and
paolo.crisafulli@irt-systemx.fr: a CV, a cover letter, transcripts for your Master’s degree, and letters
of recommendation.
Offre de thèse en preuve formelle - Vérification des Stratégies de Conduite pour des Véhicules Autonomes
Cette offre est détaillée ici :
https://adum.fr/as/ed/voirproposition.pl?matricule_prop=49879&site=adumR
Contexte
Les Systèmes Cyber-Physiques (CPS) tels que les robots ou les Véhicules Autonomes (VA) étant en fort développement dans le milieu industriel, le besoin de certification de sécurité s’étend. Les méthodes formelles sont naturellement candidates pour adresser ces besoins et relever les défis scientifiques correspondants. Les notions de raffinement standards de CSP peuvent être adaptées
à la communication et à l’interaction ainsi qu’à une représentation particulière discrétisée/échantillonnée des variables continues des CPS. Cette thèse s’appuiera sur un environnement fondé sur CSP, développé pour la modélisation et l’analyse formelle des systèmes cyber-physiques en général et des cas concrets sous forme d’études de cas du domaine des VA.
Cette thèse est proposée dans le cadre d’une collaboration entre l’Institut de Recherche Technologique SystemX (IRT SystemX, Palaiseau) et le Laboratoire Méthodes Formelles (LMF) de l’Université Paris-Saclay, au sein du projet Chaîne outillée pour la Validation et l’Homologation du véhicule automatisé connecté (CVH).
Objectifs
Étude de stratégies de conduite des VA prenant en compte :
- des dynamiques complexes (ex. accélérations et forces externes, …) ;
- des approximations de topologies (par exemple courbes et voies, …) ;
- des perceptions partielles de la scène globale (par exemple,
occlusions d’obstacles et d’acteurs) ; - vivacité des trajectoires dans des topologies complexes.
Prérequis
Bonne formation en informatique, analyse et programmation fonctionnelle ainsi qu’un intérêt pour les outils de preuve formelle (Isabelle-HOL).
Candidature
Pour postuler, merci d’envoyer les éléments suivants à burkhart.wolff@universite-paris-saclay.fr et paolo.crisafulli@irt-systemx.fr : un CV, une lettre de motivation, les relevés de note de Master 2,
des lettres de recommandation.