CLEARSY met à disposition une nouvelle version publique de l’Atelier B. Il s’agit d’un atelier de génie logiciel, c’est à dire un logiciel permettant de concevoir des logiciels.
Plus exactement, il s’agit d’ingénierie dirigée par les modèles puisque l’Atelier B permet de faire les plans généraux du logiciel voulu, et ainsi de décrire ce qu’on en attend. Il permet ensuite de raffiner ce plan, que l’on appelle un modèle du logiciel, pour décrire comment le logiciel doit réaliser ses tâches. Une fois le modèle complet, l’Atelier B permet de générer la description complète du logiciel : son code source.
La grande force de l’Atelier B est qu’il permet de faire cela en décrivant mathématiquement le modèle et de démontrer rigoureusement (mathématiquement) que le comportement prévu sera celui qu’on attend. C’est ce qu’on appelle une méthode formelle et dans notre cas il s’agit de la « méthode B« , ainsi nommée en hommage à Nicolas Bourbaki, le pseudonyme d’un groupe de mathématiciens français.
Les améliorations techniques de cette nouvelle version sont le support des systèmes d’exploitation 64 bits et l’arrivée du support des grappes d’ordinateurs serveurs. Ces serveurs permettent de distribuer la somme de calcul qui est nécessaire pour démontrer les modèles, ce qui permet aux utilisateurs d’avoir un retour rapidement, même pour les modèles complexes. Le support du 64 bits permet quant à lui d’installer plus aisément l’Atelier B sur des ordinateurs modernes qui fonctionnent en manipulant des données de 64 bits de taille.
Côté fonctionnalité, la grande nouveauté est l’arrivée d’un générateur novateur d’obligations de preuve. Les obligations sont en fait les critères de vérification d’un modèle. Ce sont elles qui seront démontrées mathématiquement. Le nouveau générateur apporte une traçabilité complète entre le modèle et les obligations, cela permet de relier une obligation avec la partie du modèle qu’elle concerne. Cette information est cruciale pour analyser rapidement un problème de conception. Nous fournissons aussi une capacité pour l’utilisateur à ajouter de nouveaux critères de vérification que le générateur appliquera.
Citons aussi une amélioration du moteur de raffinement automatisé (nommé Bart). Ce moteur permet d’obtenir automatiquement les plans détaillés à partir d’un plan général et d’un ensemble de règles qui peuvent être enrichies par l’utilisateur. Cela permet de capitaliser sur l’activité de conception détaillée, ce qui augmente la productivité des utilisateurs. L’amélioration de cette nouvelle version supprime un blocage qui devait auparavant être résolu manuellement. Nous avons ajouté une nouvelle notion supplémentaire dans la façon de définir les règles qui supprime complètement l’apparition des blocages.
Enfin, nous avons amélioré les capacités d’expression sur les nombres non entiers (et leurs équivalents informatiques concrets) en unifiant leurs expressions avec celles des nombres entiers. Ceci apporte une meilleure lisibilité des modèles.
L’Atelier B est utilisé par de grands industriels pour réaliser des logiciels sécuritaires, dans le cadre de la réalisation de systèmes répondant aux normes les plus strictes en terme de sûreté de fonctionnement.
