Méthode B

Etablissements enseignant B en France

Etablissements enseignant B en France

La méthode B est une méthode de spécification formelle capable de retranscrire de manière rigoureuse les exigences d’un cahier des charges, au moyen de preuves mathématiques, afin de prouver leurs cohérences. Ce procédé permet notamment de lever toute ambiguïté sur les propriétés initialement exprimées en langage naturel. Le langage B peut être utilisé sur des protocoles comme sur de l’informatique embarquée. De plus, la méthode B englobe toute la modélisation par la preuve d’un système, de l’écriture de son modèle à son implantation logicielle, tout en respectant les données fondamentales d’origine.

Bien que les usages de la méthode B soient divers (modélisation d’un système, formalisation de spécification …), l’objectif est le même : s’assurer de la fiabilité, de la sécurité ainsi que de l’absence de bugs informatiques d’un système par des preuves mathématiques.

La méthode B tire sa légitimité du développement d’outils approuvés et utilisés à grande échelle, dans le monde industriel comme universitaire, tels que l’Atelier B. ClearSy est détenteur de ce dernier et se charge des évolutions et de la maintenance de sa plateforme de développement. L’Atelier B constitue ainsi une référence pour le développement de logiciels prouvés.

Carte - Utilisation de la méthode B dans le monde

Les commentaires sont fermés.