CE25 - Sciences et génie du logiciel - Réseaux de communication multi-usages, infrastructures de hautes performances

Assistants de preuve basés sur la théorie des ensembles interopérables et sûrs – ICSPA

Résumé de soumission

Les méthodes formelles déductives visent à améliorer la qualité des logiciels à l'aide d'outils qui sont construits sur des fondements mathématiques solides, tels que la théorie des ensembles. Ces outils permettent à leur utilisateur de démontrer des propriétés de correction d'un programme par rapport à ses spécifications. La confiance dans ces preuves est donc un enjeu crucial, alors même que l'implémentation des prouveurs est complexe et parfois entachée d'erreurs.

L'objectif d'ICSPA est de renforcer la confiance dans les preuves mécanisées qui sont au coeur des formalismes B, Event-B et TLA+ de spécification fondées sur la théorie des ensembles. Ces environnements de développement sûr sont utilisés dans de nombreux projets industriels, là où la correction logicielle est un besoin critique. Notre projet a aussi pour objectif l'établissement d'un cadre de partage, afin que ces trois systèmes puissent s'échanger leurs preuves et leurs théories, ce qui rendra interopérable les outils respectifs, Atelier B, Rodin et TLAPS.

Notre stratégie pour cela est de vérifier, de manière formelle et indépendante, les preuves produites par ces outils avec Dedukti, un vérificateur de preuves suffisamment simple pour être facilement expertisable, voire ré-implémentable. Par sa structure versatile Dedukti offrira une base commune qui ouvrira la possibilité aux développeurs de B, Event-B et TLA+ de partager et de réutiliser entre les systèmes leurs résultats et formalisations. Cette approche est inspirée de Logipedia, une petite bibliothèque de résultats mathématiques qui peuvent être exportés vers, et vérifiés par, un large spectre de cadres logiques, entre autres Coq et HOL.

Pour atteindre nos objectifs, nous exprimerons les théories des ensembles qui sous-tendent les trois langages de spécifications en Dedukti, puis nous exporterons leurs traces de preuves, afin de les revérifier indépendamment avec Dedukti. Ce mécanisme formera le noyau d'une fonctionnalité plus ambitieuse d'export de modèles complets, utilisés en pratique pour le développement de logiciel pour les systèmes critiques, en mettant un accent particulier sur les Systèmes de transition d'états étiquetés (LTS). Toutes ces données permettront la mise au point de traductions entre les trois systèmes au niveau de Dedukti, et de procédures d'import dans les trois outils Atelier B, Rodin et TLAPS. Un outil pourra alors utiliser ce qui aura été défini ou prouvé dans un autre.

Cette architecture sera étayée par des fonctionnalités de reconstruction de preuve, fournies par des prouveurs automatiques qui permettront la complétion automatique des traces de preuves reçues en entrée, souvent incomplètes car de niveau d'abstraction relativement élevé. La reconstruction sera assistée par des points d'ancrage supplémentaires qui résulteront d'une mise en correspondance horizontale entre les outils des définitions et concepts.

Cette méthodologie sera testée et évaluée sur un large corpus d'obligations de preuve fournies par notre partenaire industriel. De plus, des cas d'étude démontrant l'interopérabilité seront mis en oeuvre. Enfin, outre la dissémination académique et éducative, Atelier B intégrera l'import et l'export de preuves, la complétion automatique de celles-ci, ainsi que leur vérification, et exploitera les résultats d'ICSPA à une échelle industrielle.

Coordination du projet

Catherine Dubois (Télécom SudParis)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

Inria Saclay - Ile de France - Equipe DEDUCTEAM Centre de Recherche Inria Saclay - Île-de-France
CLE CLEARSY / N/A
TSP Télécom SudParis
IRIT/ Université Toulouse Institut de Recherche en Informatique de Toulouse
Inria Nancy Grand Est Centre de Recherche Inria Nancy - Grand Est
UM-LIRMM Laboratoire d'Informatique, de Robotique et de Microélectronique de Montpellier

Aide de l'ANR 624 014 euros
Début et durée du projet scientifique : décembre 2021 - 48 Mois

Liens utiles

Explorez notre base de projets financés

 

 

L’ANR met à disposition ses jeux de données sur les projets, cliquez ici pour en savoir plus.

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter