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 12/12/2012 |

L’Atelier B 4.1.0 est disponible au téléchargement, pour une utilisation par tous sans restriction.  Cette version corrige 385 anomalies  et propose 56 améliorations (voir les notes de version pour un descriptif précis des améliorations les plus importantes).

Parmi celles-ci, on notera :

  • Ajout du type de projet « génération de données »
  • Support amélioré des entiers : choix de la valeur maximale implémentable (MAXINT) sur 16, 32 ou 64 bits, les littéraux entiers ne sont plus limités (BIGINT).
  • Support des nombres réels
  • Support expérimental des nombres flottants
  • Support des nombres littéraux en hexadécimal.
  • Nouveau générateur de code C, C4B, avec profils de traduction et génération de makefile
  • Localisation de l’interface graphique en Anglais, Français, Japonais et Portugais.
  • Support de l’unicode. Les identificateurs, chaines de caractères et commentaires peuvent contenir des caractères non ASCII.
  • Ajout d’une vue graphique pour le status des composants (points de vue preuve, obligations de preuve).
  • Exécution de tâches de preuve multiples en parallèle : déclencher la même action de preuve plusieurs fois conduira à l’exécution en parallèles de ces actions. Des informations supplémentaires (ordre d’exécution des actions sont affichées sur la vue graphique).
  • Amélioration de l’éditeur textuel intégré : Ctrl-D pour supprimer une ligne, meilleure indentation, ajout de la liste des fichiers ouverts récemment, paramètrage de la colorisation syntaxique, navigation dans le modèle (saut vers la définition, vers l’abstraction, vers le rafinement).
  • Ajout d’une fonctionnalité de recherche dans tous les fichiers du projet, de type grep, autorisant l’emploi d’expression régulière
  • Outil de preuve de règles : amélioration de la signalisation de l’état de vérification des règles
  • Affichage des règles rechargées lors de l’utilisation de la commande « pc »
  • Le prouveur interactif affiche désormais les branches de preuve en attente. Il est alors possible de savoir avec précision où l’on en est de la démonstration interactive.
  • Génération des obligations de preuve de couverture et d’exclusivité : ces obligations de preuve permettent de démontrer la couverture d’un modèle événementiel, et d’affirmer ou d’infirmer qu’au plus un événement est ouvert dans chaque état d’un modèle événementiel.
  • Outil de validation des règles mathématiques ajoutées par l’utilisateur. Cet outil propose une interface unique pour la gestion et la validation des règles mathématiques. Il est par ailleurs possible de saisir des démonstrations manuelles qui seront sauvegardées dans le corps du fichier pmm sous la forme de commentaires. L’outil fournit une vue synthétique par projet et par composant, ainsi que la possibilité de générer un rapport de validation.
  • Correcteur orthographique pour les commentaires de l’éditeur de modèles B : les mots mal orthographiés sont identifiés. Un menu contextuel permet de choisir une correction parmi plusieurs possibilités. Les langages pré-installés sont l’Anglais (GB, US) et le Français (France, Belgique, Canada).
  • Les règles mathématiques affichées dans la vue « Theory List » sont maintenant triées en fonction selon leur applicabilité (les gardes qui sont vérifiées sont affichées en gras)
  • L’éditeur de modèles B indique désormais si le fichier en cours d’édition a été modifié par ailleurs.