In 2023, the Professional version will be updated twice, through a corrective version in Q1 2023 and an evolutionary version in Q3 2023 with the display of counter-examples in the proof interface. In 2024, the T2 EN50128 and IEC 61508 certified Professional version will be made available, as well as the Community version integrating a RUST code generator.

 

List of corrections for the Professional version Q1 2023:

  • More powerful automatic checking of proof rules Packing of pup file to a project resource
  • Launching bbatch on a given workspace is made easier
  • Archiving in Windows fixed Arguments to the `bb` (loop) command in an interactive proof are now saved in the correct order.
  • Improved type inference in the B compiler
  • Fixed the Linux installer to avoid failures in newer distributions
  • Fixed constant values in the pptranssmt translator
  • The size of the horizontal scroll bar in the proof tree is now correct.
  • XML output from bbatch for the `gs` interactive prover command is now well balanced
  • The GUI does not crash when receiving corrupted XML data from bbatch as part of internal interactions; instead, it produces diagnostic information.
  • Improved assumption selection in the `pptranssmt` translator.
  • `Force(Fast)` is now handled for projects in NG mode (i.e, in `pos` format)
  • The `iterate` operator is now correctly rendered from the proof obligation view in the component editor.
  • Correction in rules created by the SMT hammer in the interactive proof.
  • Improved support for operation calls and inlined imports in NGOP
  • Fixed an encoding issue in the proof mechanism writer `ppTransSmt`
  • Added support for various B operators in the proof mechanism writer `ppTransSmt`
  • Checking for B0 conditions in the type check phase is disabled for system projects.
  • Documentation for Event-B support has been updated with closure implementations (syntax and proof obligations).
  • Error messages displayed in the component editor can be copied to the clipboard.
  • The dialog for saving interactive proofs in the `User_Pass` theory now includes checkboxes for saving to the PMM component file, the PUP component file, or the PatchProver project file.
  • Added setting to display the host name in the main window title
  • Added custom proof obligation generator for optional Event-B proof obligations
  • The user can now undo the closure of the interactive prover (if interactive proof commands have been issued).

List of corrections for the Professional version Q3 2023:

  • Display of counterexamples in the modelling and proof interface. When using the formal B method, design errors correspond to invalid proof obligations. Atelier B automatic provers are not able to identify whether a proof failure is due to a logical error, whereas SMT solvers are able to prove a first-order logic formula but also to refute it and produce a counterexample. These counterexamples can give the user valuable insights into design errors. SMT solvers have been integrated into the most recent version of Atelier B, but only to use their proof capabilities.
Publié le 30/01/2015 |

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.

Carte des logiciels B dans le monde