Industrie Mag - Le journal de l'industrie.

Logiciel d’ingénierie dirigée par les modèle, l’Atelier B permet à l’utilisateur d’élaborer les plans généraux du logiciel voulu, d’en affiner le modèle et de générer son code source.

Basé sur la "méthode B"

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 attendu. C’est ce qu’on appelle une méthode formelle et dans le cas précis, 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.

Support des systèmes d’expoitation 64 bits et support des grappes d’ordinateurs serveurs

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.

Générateur novateur d’obligations de preuve

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. ClearSy fournit également une capacité pour l’utilisateur à ajouter de nouveaux critères de vérification que le générateur appliquera.

Amélioration du moteur de raffinement automatisé

Par ailleurs, le moteur de raffinement automatisé, nommé Bart, 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, les capacités d’expression sur les nombres non entiers (et leurs équivalents informatiques concrets), ont été également améliorées, en unifiant leurs expressions avec celles des nombres entiers, apportant 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.

http://www.clearsy.com