Responsable : Tristan Crolard

L’équipe « Systèmes Sûrs » consacre ses recherches à la spécification, la conception, la vérification et l’évaluation des systèmes, en particulier des applications critiques du point de vue de la sûreté et de la sécurité. L'objectif est de développer des méthodes, techniques et outils permettant d'énoncer les propriétés recherchées pour des applications et de démontrer que ces applications satisfont les propriétés attendues. Toutes les recherches menées dans notre équipe rentrent dans le cadre général des méthodes formelles. Nos activités s'articulent autour de trois axes : l'axe « Typage, Sémantique et Preuves », l'axe « Architecture Logicielle, Architecture Système et Lignes de produits et l'axe « Vérification et Evaluation de Systèmes Parallèles et Asynchrones ».

Axe 1. Typage, Sémantique et Preuves

Coordinateur : Pierre Courtieu

Les membres de l’équipe qui contribuent dans cet axe sont pour la plupart des utilisateurs avancés, des experts, voire des développeurs de Coq. Nous comptons mettre à profit cette expertise en continuant à développer certaines thématiques comme la formalisation de protocoles distribués pour robots autonomes, ou la sémantique formelle de SPARK Ada:

Formalisation et preuves de protocoles distribués pour robots autonomes. Les essaims de robots effectuant une tâche de manière autonome et collaborative font l'objet d'une attention grandissante. Ce paradigme est particulièrement adapté aux situations dans lesquelles l'envoi d'agents humains est difficile voire exclu (environnement dangereux, catastrophe). Les robots agissant sans intervention humaine, les protocoles nécessitent des garanties très fortes quant à leur comportement et sont donc une cible privilégiée pour la preuve formelle. Cet axe de recherche vise à fournir les outils théoriques et pratiques (s'appuyant sur l'assistant Coq) et des études de cas pour la preuve formelles de ces protocoles, y compris en présence de fautes byzantines (agents malveillants).

Sémantique et compilation certifiée de programme impératifs. SPARK est une plateforme de vérification de programmes impératifs, dont le but est de concevoir des algorithmes à haut degré de confiance (aéronautique, défense, etc). Le langage SPARK est un sous-ensemble de Ada conçu spécifiquement pour permettre des analyses fines et obtenir des garantie fortes. Cet axe de recherche vise d'une part à écrire la sémantique formelle de certaines constructions avancées de SPARK, comme les procédures imbriquées, et d'autre part à proposer un prototype de compilateur certifié pour SPARK via le compilateur certifié CompCert. Cette sémantique formelle a déjà permis la conception d'un certificateur de vérifications à l’exécution, prouvé correct en Coq, permettant d'exclure un certain type d'erreurs de compilation. Elle fournit aussi le cadre théorique permettant de valider une technique de génération automatique d’invariants de boucles basée sur la détection de « motifs » dans les boucles.

Nous développons aussi des thématiques nouvelles dans l’équipe et Coq sera utilisé pour développer la meta-théorie de ces méthodes (en s’appuyant sur les travaux récents de la communauté) :

1. Une thématique portant sur des méthodes de preuve de correction de programmes synchrones qui prennent en compte les contraintes temps-réels.

2. Une thématique portant sur les méthodes permettant d'obtenir des programmes Scala concorrects par construction, par exemple par traduction de programmes fonctionnels prouvé corrects dans Coq.

Collaboration avec l’équipe MIM, les équipes Whisper, NPA et APR du LIP6, l’équipe Drim du LIRIS (Université Claude Bernard Lyon 1), le CIMTI (Université Saint Joseph, Liban).

Axe 2. Vérification et Evaluation de Systèmes Parallèles et Asynchrones

Coordinateur : Kamel Barkaoui

Spécification et vérification formelle : modèles et outils. Nous continuons à développer nos activités de recherche en spécification et vérification formelle de systèmes distribués concurrents, reconfigurables et temps réel en privilégiant les modèles suivants : les Bigraphical reactive systems, les Réseaux de Petri temporels et récursifs, la Logique de réécriture et les Automates temporisés. Nous cherchons aussi à développer de nouvelles approches de vérification automatique : l'analyse statique (génération d’invariants de boucle non linéaires) et model-checking (combinant techniques d’ordre partiel et sémantique de vraie concurrence).

Collaboration avec : Lab. Veriform de Ecole Polytechnique de Montréal (Canada) et Institute of Computing University of Campinas (Brésil), UC2 (Algérie)

Apprentissage Automatique, Data Science et Méthodes Formelles. Nous proposons de combiner des techniques data science avec des méthodes formelles pour extraire automatiquement des connaissances pertinentes :

1. Développer des techniques d'extraction de modèle (e.g., "process mining"), d'ensembles de base de données et leurs règles associées

2. Modéliser formellement à partir de règles qui régissent les systèmes. Nous visons appliquer ces techniques aux systèmes de détection d'intrusion (IDS), blockchain, réseaux sociaux (confidentialité).

Synthèse de contrôleurs des systèmes à évènements discrets. Nous cherchons à étendre nos travaux précédents avec la prise en compte de transitions non contrôlables et non observables.

Collaboration avec l’équipe Laetitia, System Control Group Xidian University (Chine), SysCom Enit (Tunisie)

Axe 3. Architecture Logicielle, Architecture Système et Lignes de produits

Coordinatrice : Nicole Levy

Une entreprise possède souvent de nombreux logiciels d’un même domaine fonctionnel et assurant des missions similaires, mais avec des exigences non fonctionnelles et des contraintes différentes et au final des architectures différentes, mais comparables. Notre objectif est de proposer des aides au développement permettant de valoriser la connaissance implicite de l’entreprise pour spécifier, concevoir et valider de nouveaux systèmes d’un même domaine fonctionnel, et réutiliser au maximum des parties des systèmes existants.

Pour cela, nous combinons plusieurs approches : analyse fonctionnelle, définition d’une architecture de référence, expression de la variabilité aussi bien au niveau architectural que du code, définition de mécanismes de gestion de la variabilité dynamique. Nos travaux se font dans le cadre d’un partenariat avec la société Berger-Levrault qui nous permet d’étudier plusieurs de leurs systèmes de gestion de collectivités territoriales.

Collaboration avec l’équipe MIM et la société Berger-Levrault. 

Développement de lignes de produits corrects par construction. L'objectif est d'offrir des techniques de réutilisation en mettant l’accent sur la gestion de la variabilité et de la réutilisation. Pour cela, une approche garantissant la correction des produits issus d’une ligne de produits est proposée basée sur le langage FFML (Formal Feature Module Language), inspiré de FoCaLiZe qui incorpore des mécanismes d’expression de la variabilité. L'approche est outillée : le compilateur de FFML vers FoCaLiZe et le générateur de produits qui permet de construire un produit correct par construction à partir d'une configuration correcte de la ligne de produit, ont été développés. De plus, les outils de FoCaLiZe (prouveur et générateur de code exécutable OCaml) sont intégrés dans la plateforme.

Collaboration avec l’équipe METHODES du laboratoire Samovar.