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).
Il est disponible en 2 versions :
1- Version communautaire accessible à tous sans limitation,
2- Version maintenue accessible aux possesseurs d’un contrat de maintenance.
Il est utilisé pour le développement des automatismes sécuritaires des différents métros développés dans le monde par Alstom, Siemens, etc. et d’autre part, pour la certification selon la norme “Critères Communs” et le développement de micro-circuits par l’industrie des semi-conducteurs.
ll a été 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. L’Atelier B est utilisé dans le secteur de l’aéronautique et de l’aérospatial.
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