Atelier B proof obligation generator was developped in the early 90′s. Developped with the prolog-like “theory language”, this tool is very sensible to modifications and difficult to adapt to language extensions/modifications. The idea is to develop a generic proof obligation generator that can:

• support both B and event-B proof obligations
• be easily modifiable/extandable, to generate specific proof obligations.

Developments started in 2011, within the framework of the CERCLES-2 R&D project.

Jean Louis Dufour (Sagem Défense & Sécurité, ), will come to the AdaCore Paris offices to give a 101 introduction to the B-Method (June 26, 2012 – Paris, France)

Source: adacore internal seminar

Started in February 2008, the DEPLOY project,  probably the biggest Formal Method project ever funded by the European Community, completed in April 2012. During more than 4 years, 86 researchers and engineers from 14 partners have collaborated to the development, improvement and assessment of the Rodin platform, plugins, and educational materials, while sharing the common objective of easing its adoption by Industry.

A company, Rodin Tools Ltd, has been created recently as a Not for Profit Company taking over responsibility for the Rodin toolset at the end of DEPLOY.

Several resources are available:

• DEPLOY publications, reports, tutorials and projects/models, developed by the project members, for a total of 280 items.
• DEPLOY technology transfer wiki containing all user’s documentation for the Rodin platform.
• Rodin User’s Handbook.
• Industrial assessment reports
• Open repository of evidence for adopting Formal Methods in industry

Rodin 2.5 is available on Sourceforge

ProB model-checker is being integrated in Atelier B 4.0, in order to provide additional proof power and animation capabilities to Atelier B.

With the help of Pr. Michael Leuschel, a MacOS prototype has been developped, allowing to animate and model-check a B model from Atelier B 4.0. At that occasion, a generic interfacing mechanism has been developped and will be enriched and improved in the future. This mechanism is described in the GUI_Project section. ProB 1.3.0+ is now self integrating with AtelierB 4.0, at model level. Ongoing developments at University of Dusseldorf for integration at proof obligation level.

Atelier B 4.0 natively supporting event B, animating such models is mandatory. 

The Brama  animator has been ported on Atelier B 4.0 environment: the predicateB predicate evaluator has been ported to C++ and connected with B-Compiler.