Development of a generic proof obligation generator

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.

Publié dans Research, Tools | 2 commentaires

B-Method – AdaCore micro-seminar

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

Publié dans Event | Laisser un commentaire

DEPLOY project completed

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:

Publié dans Event, Research | Laisser un commentaire

Rodin 2.5 released

Rodin 2.5 is available on Sourceforge

Publié dans Tools | Laisser un commentaire

Integration of ProB

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.

Publié dans Research, Tools | Laisser un commentaire

Port & development of Brama model animator to Atelier B

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.

Publié dans Applications, Tools | Laisser un commentaire