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 04/10/2016 |

Le projet LCHIP (Low Cost High Integrity Plateform) vise à faciliter le développement de systèmes sécuritaires (logiciel critiques) jusqu’au niveau SIL 4 qui constitue le niveau le plus élevé en matière d’exigence de sûreté.

Le projet LCHIP combine un environnement de développement complet en langage B (mathématique) à une plateforme d’exécution des logiciels sécurisée en temps réel. L’environnement de développement permet de générer ainsi que de prouver mathématiquement et automatiquement du logiciel critique. Employé sur des logiciels à algorithmique bornée, il va jusqu’à étendre les fonctionnalités de l’Atelier B (langage B). La plateforme à bas coût qui lui est associée pour l’exécution des  logiciels, est sécurisée en temps réel afin de garantir un niveau de sûreté maximal. « Cette combinaison technologique divise par dix le coût de la plateforme sécurisée », précise Thierry Lecomte spécialiste de l’Atelier B chez CLEARSY.

CLEARSY spécialiste du développement de systèmes sécuritaires et éditeur de l’Atelier B est à l’initiative du projet LCHIP. Celui-ci est soutenu par le Fonds unique interministériel (FUI) un programme destiné à soutenir la recherche appliquée (FUI 21). Co-Labellisé par les pôles de compétitivité Systematic Paris-Région, I-Trans et SCS (Solutions communicantes sécurisées), le projet LCHIP est développé au sein d’un consortium animé par CLEARSY au titre de porteur du projet. « Mais l’intégration transparente à des langages métier (autre que B) favorisera l’exploitation de la technologie en dehors du consortium », insiste Thierry Lecomte. 

Alors que le déploiement d’applications sûres à haut niveau de criticité reste limité pour des raisons économiques, la technologie LCHIP va permettre d’améliorer la sécurité des citoyens en en démocratisant l’usage. Et c’est la SNCF membre du consortium qui en évaluera la technologie, grâce à des cas d’études significatifs du domaine ferroviaire.

Congrès Lambda Mu organisé par l’IMDR (Institut de la Maitrise des Risques) du 11 au 13 octobre à St-Malo. La communication de Thierry Lecomte « « Biprocesseur et preuve formelle pour automatismes SIL4 » est programmée le jeudi 13 à 14h. Retrouvez également CLEARSY sur son stand toute la durée du congrès.