L’utilisation des méthodes formelles dans un contexte industriel ne peut être envisagée sans l’aide d’outils. L’Atelier B est l’un d’eux. Il a été constitué grâce aux efforts conjoints de plusieurs entreprises voulant utiliser la méthode B : les constructeurs Alstom et Matra Transport International, la SSII Stéria, la RATP et la SNCF. Il permet une utilisation opérationnelle de la méthode B sur des projets d’envergure et a déjà été mis en ?”uvre, entre autres, sur le projet Météor (quatorzième ligne du métro parisien, entièrement automatisée). Il comprend un générateur automatique de preuves destiné à générer les conditions de validation qui rendent corrects les modèles abstraits, un “prouveur” qui se charge de prouver automatiquement les énoncés résultants, et un traducteur qui, lui, transforme le dernier niveau de raffinement du modèle B en langage de programmation traditionnel. LAtelier B intègre aussi un analyseur lexical, un analyseur syntaxique et un vérificateur de type.
🔴 Pour ne manquer aucune actualité de 01net, suivez-nous sur Google Actualités et WhatsApp.
