Une plate-forme mécanisée et basée sur la preuve pour la vérification d'obligations de preuve B – BWare

Le projet BWare est un projet de recherche industrielle qui a pour objectif de produire un environnement mécanisé pour prendre en charge la vérification automatique d'obligations de preuve provenant du développement d'applications industrielles utilisant la méthode B et exigeant de fortes garanties de confiance. Il concerne donc l'axe thématique 1 (« Ingénierie du logiciel et du matériel ») et l'axe thématique 2 (« Ingénierie Numérique & Sécurité ») de l'appel à projets « Ingénierie Numérique & Sécurité ».

La méthodologie utilisée par ce projet consistera à construire une plate-forme générique de vérification reposant sur différents outils de démonstration, tels que des outils de démonstration au premier ordre et des solveurs SMT (« Satisfiability Modulo Theories »). La variété de ces outils de démonstration a pour objectif de permettre de démontrer automatiquement un large panel d'obligations de preuve avec notre plate-forme. La majeure partie des outils de vérification utilisés dans BWare a déjà été utilisé dans des expérimentations, qui ont consisté à vérifier des obligations de preuve ou des règles de preuve provenant d'applications industrielles. Cela devrait donc constituer un facteur décisif pour réduire les risques du projet, qui peut alors se concentrer sur la conception de plusieurs extensions pour les outils de vérification afin de traiter un plus grand nombre d'obligations de preuve.

Au-delà de l'aspect multi-outils de notre méthodologie, l'originalité du projet BWare réside également dans l'obligation pour les outils de vérification de produire des objets preuves, qui sont à vérifier indépendemment. Ce « backend » devrait nous permettre non seulement d'accroître la confiance dans les preuves produites, mais aussi de fournir de l'interopérabilité entre outils de démonstration. Le succès de BWare sera assuré par une large collection d'obligations de preuve fournie par certains des partenaires industriels de ce projet, qui développent soit des outils implantant la méthode B ou des applications impliquant l'utilisation de la méthode B.

Ce projet combine quatre types différents d'expertise : production d'obligations de preuve pour la méthode B ; traduction de la théorie des ensembles vers la logique du premier ordre ; démonstration automatique ; production et vérification de preuves. Le consortium de BWare associe des entités académiques (CEDRIC, LRI et Inria) et des partenaires industriels (Mitsubishi Electric R&D Centre Europe, ClearSy et OCamlPro). Cela assurera un excellent niveau d'expertise pour les aspects scientifiques, ainsi que pour leur exploitation pour le développement de logiciels exigeant de fortes garanties de confiance.

L'organisation du projet consiste en plusieurs parties. Parmi ces parties, il y a une étude théorique concernant la génération d'obligations de preuve, ainsi que la formalisation de plusieurs modèles pour la théorie des ensembles sous-jacente à la méthode B. Cette partie servira à une autre partie concernant la conception d'une plate-forme de vérification, qui réunira plusieurs outils, et des extensions de ces outils seront considérées et développées. Cette plate-forme sera intégrée à l'outil d'un partenaire industriel (l'Atelier B de ClearSy) pour une évaluation sur des applications industrielles et une comparaison avec d'autres outils de vérification similaires. Une activité de preuve interactive sera également conduite de manière à combiner de façon optimale les outils de démonstration automatique, et des optimisations des outils de vérification seront aussi étudiées.

La dissémination des résultats sera assurée par un site web, des publications, l'organisation de séminaires (et éventuellement des workshops), et un accès libre à la plate-forme de vérification. La diversité des membres du consortium aidera à promouvoir assez largement les résultats de ce projet dans différentes communautés, telles que les académiques, les acteurs industriels, les développeurs et les utilisateurs.