Outil pour la méthode formelle B permettant de développer
des logiciels prouvés sans défaut
QU’EST-CE QUE
LA MÉTHODE B ?
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.
+ 20 Heures de vidéos
Ce cours introduit la méthode B : les concepts de base depuis les machines B jusqu'à la preuve mathématique avec le prouveur de l'Atelier-B.
Modèles B & Event-B
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.
Basic & Advanced
training
Introduction vidéos
Ces vidéos : Elles présentent l'outil et son utilisation pratique, pour à la fois le développement logiciel et la modélisation de systèmes.
Training resources
Articles & B models
Collection de modèles formels et d'articles. Ces ressources permettent d'améliorer ses compétences en modélisation, preuve et génération de code.
ATELIER B,
PRÉSENTATION
L’Atelier B est l’outil industriel qui permet une utilisation opérationnelle de la méthode formelle B pour des développements de logiciels prouvés sans défaut (logiciel formel) ou pour valider des propriétés de sécurité d’un système.
Il est disponible en 4 versions :
1- Atelier B Community Edition
2- Atelier B Professional Edition
3- Atelier B T2 Certified Edition
4- Atelier B CSP Educational Version
L’Atelier B Community Edition est une version entièrement fonctionnelle de l’Atelier B mise à jour tous les 2 ans. Téléchargeable gratuitement depuis ce site, il est utilisable librement.
L’Atelier B Professional Edition est régulièrement mis à jour et dispose de fonctionnalités exclusives comme un traducteur Ada, un contrôleur de cohérence de projet (Project Checker), et des outils de preuve de règles mathématiques. Il est utilisable dans un cadre industriel nécessitant un support étroit mais aussi dans un cadre académique. Il est accessible sur demande au travers d’un contrat de maintenance.
L’Atelier B T2 Certified Edition, au travers de sa certification T2, permet de développer des logiciels critiques conformes à la norme EN 50128 et de valider des propriétés systèmes conformes à la norme EN 50129 pour des applications de niveau SIL4. Un outil de rejeu, le Certifier, permet de garantir la conformité aux normes des projets développés avec un Atelier B récent. Il est accessible sur demande dans un cadre industriel et dispose des mêmes exclusivités que l’Atelier B Professional Edition.
L’Atelier B CSP Educational Version est une version particulière l’Atelier B Community Edition de qui permet de programmer un contrôleur sécuritaire (la CLEARSY Safety Platform) intégré à une carte électronique de démonstration. Il permet de s’initier à la programmation d’applications critiques de contrôle-commande.
L’Atelier B est notamment utilisé pour le développement des automatismes sécuritaires des différents métros développés dans le monde par Alstom, Siemens, etc. pour la certification selon la norme “Critères Communs” et le développement de micro-circuits par l’industrie des semi-conducteurs et pour garantir la sécurité des systèmes.
ll est utilisé sur d’autres secteurs comme celui de l’automobile pour la modélisation des principes de fonctionnement de l’électronique embarquée sur 3 modèles de voiture.
MÉTHODE B,
POUR DES LOGICIELS FIABLES
Ce site a pour but de présenter les différents travaux et sujets de réflexion de CLEARSY sur la MÉTHODE B : Méthode formelle avec preuve de développement logiciel, supportée par l’Atelier B. Ces travaux et sujets de réflexion sont étroitement liés à des projets ou produits industriels qui sont commercialisés par CLEARSY ou développés par/pour d’autres entreprises industrielles.
Cette méthode, développée depuis le début des années 1990, permet de construire de nombreux logiciels de part le monde, notamment dans le domaine du transport ferroviaire, comme le système de contrôle de vitesse par balise des trains Français, le pilote automatique du métro de Pékin ou les automatismes fixes de la navette automatique de l’aéroport Charles de Gaulle