Contact

Download B tools

 Presentation of the B method

CLEARSY makes available for the community, a set of tools developped around CLEARSY’s R&D projects.
These tools are related to the B model and formal proof. The most recent tools are only developped with C++ language, using Qt libraries and are available according to the V3 GPL License. The oldest tools, such as proof tools, use less common technologies and would require a significative effort to make documentations available – their source code has never been published – the source code of those tools will be available when they’ll be redevelopped with up to date technologies.

ATELIER B

MAIN TOOLS

SOURCE CODES OF TODAY TOOLS,
INTEGRATED TO THE CURRENT ATELIER B VERSION

ARE :

> Compilateur B
> C4B : Générateur de code C
> BART : Outil de raffinement automatique
> Interface homme-machine de l’Atelier B

NEVERTHELESS, COMPLEMENTARY TOOLS
WERE DEVELOPPED AROUND CLEARSY’S PROJECTS
THEY ALLOW TO IMPROVE THE EXPERIMENT
IN MODELLING B:

> Pro-B : model checker et animateur de modèles B
> BMotionStudio : animateur de modèles B

VARIOUS TOOLS ARE BEING DEVELOPPED
AND SHOULD BE INTEGRATED SHORTLY,
TO THE ATELIER B :

> Générateur d’obligation de preuve générique
> B4SYN : Générateur de code VHDL
> B2LIST : Générateur de code Instruction List
> RELIC : Outil de traçabilité des exigences
> Predicate B++ : Évaluateur de prédicats

More informations about "Presentation of the B method"

Copy link
Powered by Social Snap