Rechercher

Conception et Programmation Raisonnée

Groupes

Description

Cette page n'est plus actualisée, merci de visiter la page de l'équipe Systèmes Sûrs.

Présentation générale

Les travaux de l’'équipe CPR s'inscrivent dans le développement et l'utilisation de méthodes formelles pour le développement de logiciels sûrs. Sûrs signifie ici que les logiciels développés vérifient les propriétés que l'on a énoncées formellement. Ces propriétés caractérisent les fonctionnalités du logiciel, mais peuvent aussi être relatives à la sûreté et la sécurité.

Nos travaux portent sur le développement de langages, théories, techniques de preuve pour la spécification, la conception, la programmation, et la vérification des logiciels (soit toute l'étendue du cycle de vie du logiciel).

 

Les axes majeurs de l'équipe CPR :

  • Preuve automatique certifiée. Ce thème vise à la certification (par des outils de preuve mécanique, c'est-à-dire des assistants à la preuve) des résultats de démonstrateurs automatiques (sans interaction avec l'utilisateur) afin de permettre leur utilisation en conjonction avec des assistants à la preuve. Actuellement les travaux de l'équipe se concentrent sur l'outil CiME (dont la version 3 est en cours de développement) et la production automatique de certificats Coq pour des preuves (CiME) de propriétés liées à la réécriture. CiME3 traçant, c'est-à-dire produisant des traces vérifiables par Coq, et utilisant une partie du moteur de terminaison de CiME 2.04 est déjà disponible à l'adresse http://a3pat.ensiie.fr/ .
  • Vérification formelle de compilateurs. Ce thème, développé en collaboration avec Xavier Leroy de l'INRIA, vise à produire un compilateur pour un sous-ensemble réaliste de C, entièrement vérifié à l'aide du système Coq. Nos contributions principales (travail de S. Blazy) concernent la vérification du front-end du compilateur et la formalisation d'un modèle mémoire pour C utilisé tout au long de la chaîne de compilation par les nombreux langages intermédiaires du compilateur. En collaboration avec l'équipe OC, nous étudions et formalisons également l'allocation de registres.
  • Certification de générateurs aléatoires. Ces travaux s'intéressent à la certification d'outils basés sur des générateurs aléatoires, avec pour cas d'étude un algorithme de tatouage contraint de base de données.
  • Modélisation de composants logiciels. Nous nous intéressons à la définition d'un modèle formel de composants, suffisameent général pour capturer la majorité des modèles existants. Nous avons défini un un modèle formel pour les composants à la Fractal capturant les aspects relatifs au contrôle des liaisons et à la reconfiguration dynamique. Le cadre proposé, nommé FracL, est fondé sur une description axiomatique des primitives de Fractal en logique de premier ordre, et permet la spécification et la preuve des propriétés autant fonctionnelles que de contrôle dans ces systèmes.

Projets terminés récemment