Archives de l’auteur : ClearSy

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 … Continuer la lecture

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 … Continuer la lecture

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 … Continuer la lecture

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