Méthode B

Carte Commune · n° 245052

La méthode B est une méthode formelle qui permet le raisonnement sur des systèmes complexes ainsi que le développement logiciel. La méthode B permet de modéliser de façon abstraite le comportement et les spécifications d'un logiciel dans le langage de B, puis par raffinements successifs d'aboutir à un modèle concret dans un sous-ensemble du langage B transcodable en Ada ou en C, exécutables par une machine concrète. Elle permet de formaliser le système et son environnement de manière abstraite, puis par raffinements successifs, de rajouter les détails au modèle du système. Une activité de preuve formelle permet de vérifier la cohérence du modèle abstrait et la conformité de chaque raffinement avec le modèle supérieur (prouvant ainsi la conformité de l'ensemble des implémentations concrètes avec le modèle abstrait). On distingue : le B classique tel qu'il est défini dans le B Book de 1996. L'outil logiciel de support est l'atelier B ou le B-Toolkit. le B événementiel qui est une évolution...

Lire sur Wikipédia · Image Joris Rehm, CC BY-SA 3.0