Formation B

Objectifs

• Comprendre les principes du développement d'un projet B.
• Pratiquer la construction de "bons" modèles B.
• Apprendre les notions avancées du Langage B.
• Découvrir le B événementiel.

Personnes concernées

• Toute personne désireuse d'approfondir ses connaissances sur la Méthode B.
• Toute personne devant participer à un projet B en écrivant des modèles.

Pré-Requis

• Formation B Niveau 1, ou bien la connaissance des principes de la Méthode B.
• Connaissance de base en informatique.
• Connaissances mathématiques du niveau d'un bac scientifique.

Durée

• 4 jours

Organisation

• 10 personnes au maximum par formation.
• La formation se déroule dans les locaux de ClearSy à Aix ou à Paris (sauf dispositions exceptionnelles).
• Contactez ClearSy pour connaître les dates des prochaines formations.

Tarifs

• 2.130 EUR HT par personne.
• Une réduction de 15 % est accordée pour un groupe de 3 personnes au moins, du même organisme.

Programme

Développement d'un projet

• Description du passage entre spécifications informelles et spécifications formelles. On rappelle la construction modulaire d'un projet B et on décrit les différentes sortes de liens entre les modules B, ainsi que les règles concernant ces liens. On donne une première base méthodologique afin de construire un projet B comme un assemblage de modules.

Pratique de la construction de modèles B

• Par des exercices, la signification formelle de "respecter sa spécification" est expliquée, ainsi que la manière dont elle se traduit par les obligations de preuve produites avec l'Atelier B. Ensuite, l'auditeur est amené au cours de travaux dirigés sur des exemples complets à créer les spécifications formelles à partir des prérequis informels, à procéder à la conception et à analyser comment la preuve rend impossible toute non-conformité. Les principes de rédaction des modèles pour faciliter la preuve sont étudiés.

Notions avancées de B

• Description de tous les principes avancés du Langage B qui n'ont pas été présentés ou détaillés lors de la formation de niveau 1. Il s'agit des enjeux concernant les invariants de liaison, de l'homonymie des données et de la construction des boucles.

Découverte du B Evenementiel

• Présentation des principes du B événementiel. Un TD complet permet l'étude de son application pratique, tout en examinant la signification des preuves de raffinement dans une telle modélisation. On étudie les points de repère pour bien choisir les variables abstraites et les événements, et pour bien définir leur interprétation dans la réalité.

Organisation pratique

• Plus de la moitié de la formation se déroule sous la forme de Travaux Dirigés ou de Travaux Pratiques, afin de mieux se familiariser avec la construction modulaire d'un projet B et avec les notions avancées du Langage B. A cet effet, le TP sur la modélisation et la conception d'un système de contrôle des feux de circulation d'un carrefour occupera la majorité des TP. Il est suivi du TD et TP d'étude du B événementiel.