OUTIL DE PREUVE DE BONNE DÉFINITION DE MODÈLES FORMELS UTILISÉS EN VALIDATION DE DONNÉES

Objectifs du stage : Évaluation d’un prouveur de bonne définition et amélioration d’un parseur syntaxique B.

CLEARSY DATA SOLVER est un outil de validation de données permettant d’évaluer du code écrit en langage B afin d’en déduire les cas de contre-exemples à des règles de validation.

Dans le but de pérenniser l’outil, un outil automatique des preuves de bonnes définitions y sera intégré, ceci dans le but de garantir d’éviter toute erreur de définitions B. De plus, le parseur du langage B actuellement utilisé est écrit en Java et doit être remplacé par un autre parseur afin d’éliminer la dépendance à Java.

Les objectifs du stage seront de :

• Évaluer un nouveau générateur & prouveur de bonne définition : vérifier la complétude des cas et sa robustesse en comparaison à l’existant
• Analyse de faisabilité et migration du parseur syntaxique B de l’atelier B vers du Rust.
• Améliorer le parseur syntaxique B de l’atelier B afin d’y inclure les nouvelles formes du langage proposé par l’outil ProB
• Comparer la qualité et les performances entre l’ancien parseur Java et le nouveau parseur

Compétences recherchées : 

• Rigueur & autonomie
• C++/Rust