B TOOLS


DOWNLOAD B TOOLS


picto-b-130x130

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 to the formal proof.

B DOWNLOADS


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.

pictos-8-105x105

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