Le manuel d’utilisation de la méthode B, le B WORKBOOK, est désormais disponible sur le GitHub de CLEARSY : (https://github.com/CLEARSY/BWORKBOOK).
Après plusieurs mois de travail, cette première version (122 pages) peut désormais être utilisée comme ressource pour la formation aux méthodes formelles et l’enseignement de la méthode B.
Nous remercions chaleureusement les contributeurs et les relecteurs tel que l’institut IMD/Universidade Federal do Rio Grande do Norte UFRN (Natal, Brésil), l’Universidade Federal de Pernambuco UFPE (Recife, Brésil), l’Université de Düsseldorf (Düsseldorf, Allemagne) et Télécom-Paris (Paris, France), qui ont rendu cette publication possible.
Le B WORKBOOK propose actuellement 7 exercices de complexité croissante, offrant une introduction étape par étape à l’outil Atelier B.
Il couvre les principales phases de développement avec la méthode B : spécification formelle, implémentation, preuve, génération de code et compilation de l’exécutable final.
Chaque exercice est accompagné :
- de fichiers de modélisation
- de fichiers de preuve avec démonstrations automatiques
- d’un code source manuel complémentaire et d’un Makefile pour les environnements Unix (Windows WSL, Linux, MacOS)
- d’instructions pour animer les modèles avec l’outil dédié ProB
Une prochaine itération (prévue pour 2026) élargira le champ d’application avec de nouveaux exercices sur :
- le langage de modélisation formelle Event-B
- l’animation graphique avec l’outil VisB
- la génération de code Rust
- les preuves interactives, les tactiques de preuve et la rédaction de règles
Nous vous invitons à nous faire part de vos rapports d’erreurs, suggestions et nouvelles idées d’exercices via le réseau collaboratif GitHub.