Accueil | Actualités B | La Méthode B | Travaux R&D | Preuve Formelle | Publications | Conférences | B, les différents langages | Projets Open Source | Outils B | Documents | Liens | Contact  

Outils B en téléchargement

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

Il vous est également possible de consulter la roadmap de nos outils B en suivant ce lien :
Roadmap 2007/2008 de ClearSy...

programmation Outils B de ClearSy freelance

Atelier BAtelier B
Atelier de génie logiciel permettant de développer des logiciels prouvés sans défaut.

BEditorBEditor
Plugin Eclipse permettant d'éditer un modèle Atelier B avec colorisation des mots-clefs.

Click'n ProveClick'n Prove
Interface du prouveur interactif de l'Atelier B et de l'outil B4Free.

RODINRODIN
Plateforme ouverte pour la modélisation et la preuve de systèmes complexes en B événementiel. Il supporte les outils B suivants :

Outils RODIN

BramaBrama
Plugin Eclipse permettant d'animer un modèle événementiel à partir de la plateforme RODIN.

B2RODINB2RODIN
Plugin Eclipse permettant d'importer un modèle Atelier B, compatible B événementiel, au sein de RODIN

CompoSysCompoSys
Méthode et outil pour des descriptions formelles de systèmes. Fonctionne également sous RODIN
programmation Outils B externes à ClearSy freelance

GenesystGenesyst :
Ensemble de classes utilisant la BoB pour générer des systèmes de transitions étiquetés réprésentant le comportement exact d'une spécification ou d'un raffinement B événementiel.

La BOBLa BOB :
Ensemble de classes Java permettant de manipuler des constructions B