COMPILATEUR B


PRÉSENTATION


Le compilateur B est, avec le Générateur de Théorèmes et le démonstrateur de Théorèmes, l’un des outils principaux de l’Atelier B. il permet l’analyse de la syntaxe des modèles B et de vérifier la cohérence des types et les règles de construction et de visibilité des modèles d’un projet B. Il constitue aussi une puissante librairie permettant de construire de nouvelles applications.

ON CITERA PAR EXEMPLE


logo-compilateurB

BART
> Outil de raffinement automatique. Cet outil permet d’automatiser l’implantation de machines abstraites B, en appliquant des règles de raffinement. Un outil similaire est utilisé par Siemens Transportation Systems pour le développement de pilotes automatiques de métros.

B2Ladder
> Traducteur produisant un modèle graphique Ladder (langage à contact utilisé par les automates programmables industriels) à partir d’un modèle B. Ce traducteur est spécifique à la famille d’automates Siemens S7.

Btags
> Outil générant des informations de navigation pour l’éditeur de modèles de l’Atelier B V4.0, Emacs et vi. Il accepte en entrée des machines B, des règles mathématiques utilisées pour la preuve avec Atelier B ainsi que des règles de raffinement BART.

B2Rodin
> Transformation d’un modèle B événementiel (au format textuel Atelier B) en un modèle xml Rodin.

Le référenceur croisé (CrossRef)
> Outil de génération des dictionnaires des termes.

> Les traducteurs de B vers C, ADA, High Integrity ADA (industriel).

picto-9

PROJETS OPEN SOURCE

Plus d’informations sur l’état de nos Projets Open Source.