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.
Considérée comme un leader de la méthode B, CLEARSY a dispensé depuis le lancement des formations B en 2014 plus 6250 heures de formation et formé plus de de 250 personnes.
En 2023, 100% de participants sont satisfaits, dont 92% de très satisfait.
La certification a été délivrée au titre de la catégorie d’action suivante: ACTIONS DE FORMATION
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.
