OUTIL DE PREUVE DE BONNE DÉFINITION DE MODÈLES FORMELS UTILISÉS EN VALIDATION DE DONNÉES
Objectifs du stage :
Évaluation et test d’un prouveur de bonne définition. 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, il est nécessaire de le faire évoluer afin de le rendre plus robuste aux erreurs de mauvaises définitions B.
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.
- Écrire des tests couvrant les différents cas afin d’avoir une garantie.
- Améliorer le parseur syntaxique de langage B de l’atelier B afin d’y inclure les nouvelles formes du langage proposé par l’outil ProB.
- Comparer entre les résultats du nouveau prouveur de bonne définition et celui de l’atelier B (en termes de qualité et de performance)
Compétences recherchées :
- C++
- Git
- Rigueur & autonomie