OUTILS B


OUTILS B EN TÉLÉCHARGEMENT


picto-b-130x130

CLEARSY met à disposition de la communauté un ensemble d’outils développés dans le cadre de projets R&D.
Ces outils sont relatifs à la modélisation B et à la preuve formelle.

B EN TÉLÉCHARGEMENT


CLEARSY met à disposition de la communauté un ensemble d’outils développés dans le cadre de projets R&D.
Ces outils sont relatifs à la modélisation B et à la preuve formelle. Les outils les plus récents sont développés de manière systématique en C++, utilisant les librairies Qt et sont mis à disposition selon la licence GPL V3.Les outils les plus anciens, comme les outils de preuve, utilisent des technologies moins courantes et demanderaient donc un effort plus grand de documentation – leur code source n’a pas été publié – on préfèrera mettre à disposition les sources de ces outils lorsqu’ils seront re-développés avec des technologies d’actualité.

pictos-8-105x105

ATELIER B


MAIN TOOLS

LES OUTILS AUJOURD’HUI DISPONIBLES
SOUS FORME DE CODE SOURCE, ET INTÉGRÉS
À LA VERSION COURANTE DE L’ATELIER B,
SONT :

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

PAR AILLEURS, DES OUTILS COMPLÉMENTAIRES,
DÉVELOPPÉS EN DEHORS DE CLEARSY,
PERMETTENT D’AMÉLIORER L’EXPÉRIENCE,
DE MODÉLISATION EN B :

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

PLUSIEURS OUTILS SONT EN COURS
DE DÉVELOPPEMENT OU D’INDUSTRIALISATION,
ET DEVRAIENT ÊTRE INTÉGRÉS PROCHAINEMENT,
À L’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