Enseignement de la Méthode B
La méthode formelle B est enseignée dans de nombreux établissements et universités, sur tous les continents, pour :
- Le développement de logiciels (langage B)
- La modélisation (langage Event-B)
L’enseignement s’appuie sur l’Atelier B « community version » qui est entièrement fonctionnelle et pleinement utilisable pour la modélisation, la preuve et la génération de code C. Les modèles formels B peuvent être animés et vérifiés (model-checking) grâce à l’outil ProB.
Un MOOC dédié à la méthode B est accessible à tous. Il contient 20 vidéos pour une durée de 6h50, couvrant les bases de la méthode, depuis la modélisation jusqu’à la gestion de projet. Le site héberge les modèles utilisés pour les vidéos ainsi que les fichiers de preuve. Le MOOC a été réalisé en collaboration avec l’Instituto Metropole Digital / UFRN (Natal, Brésil).
Par ailleurs, l’université de Düsseldorf héberge un dépôt de modèles formels B provenant d’une large variété de modélisateurs industriels et académiques, pouvant être utilisés pour la formation et l’auto-amélioration.
Enfin le calculateur sécuritaire CLEARSY Safety Platform se programme avec le langage B pour la réalisation d’applications critiques.Parmi les deux configurations du calculateur, la version « for education » est disponible sous la forme de :
- Un IDE (Atelier B + plug-ins)
- Une carte de développement pour l’exécution des programmes compilés ou son simulateur logiciel.
Le simulateur logiciel est disponible gratuitement et sans restriction. Il a été démontré à l’occasion d’un tutorial à la conférence ABZ 2021 (voir la vidéo).
La valeur ajoutée de la CLEARSY Safety Platform est que les étudiants peuvent « animer les choses » (voir les variables de modélisation changer sur le simulateur ou les leds clignoter sur le tableau). Des cours et sessions pratiques ont été donnés dans le monde entier ces quatre dernières années et cela a été bien reçu par :
- les profils théoriques qui peuvent appliquer leurs modèles abstraits au monde physique
- par les profils systèmes embarqués / IoT qui peuvent découvrir la modélisation et la vérification formelles.
Ces cartes sont déjà utilisées pour des cours de master / master 2 en France, Allemagne, Italie, Canada et Brésil.