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

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.