Formations

CLEARSY propose des formations pour l’outil ATELIER B. C’est un outil qui permet une utilisation opérationnelle de la MÉTHODE FORMELLE B.
Il offre, au sein d’un environnement cohérent, de nombreuses fonctionnalités permettant de gérer des projets en langage B.

La “méthode formelle B” évoque traditionnellement l’ensemble comprenant :
le langage B, le raffinement, la preuve et les outils associés.

ATELIER B

FONCTIONNALITés

L’ATELIER B est un outil qui permet une utilisation opérationnelle de la MÉTHODE FORMELLE B. Il offre, au sein d’un environnement cohérent, de nombreuses fonctionnalités permettant de gérer des projets en langage B.

ATELIER B

Il s’utilise soit par l’intermédiaire d’une Interface Homme Machine au format QT, soit en utilisant directement des commandes (mode de commandes) L’Atelier B est multi-utilisateurs. Les tâches automatisables lors du développement d’un projet sont les suivantes :
• Vérifications syntaxiques des composants
• Génération automatique des obligations de preuve
• Traduction automatique des implantations B vers les langages C ou Ada.

L’Atelier B est disponible sous Windows, Linux et Mac OS.

Visitez le site de l’atelier B

Méthode b

Le B événementiel est une spécialisation de la méthode formelle B, utilisée pour décrire formellement les systèmes et raisonner mathématiquement sur leurs propriétés.

La méthode B est une méthode de spécification formelle qui permet, grâce à un langage adéquat, d’exprimer très rigoureusement les propriétés exigées dans un cahier des charges. Il est alors possible de prouver de manière automatisée que ces propriétés sont non ambiguës, cohérentes et non contradictoires.