méthode B

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 utilisant uniquement la notion d'événements pour décrire les actions et non plus les opérations (qui sont proches des routines informatiques). Par conséquent, la méthode peut s'appliquer pour l'étude des systèmes de domaines variés, plus seulement à des programmes. On réalise alors des développements incrémentaux de systèmes prouvés. Pour cela on utilise toujours l'atelier B. * le B# (B sharp) qui est une reprise du B événementiel avec des éléments de la notation Z. L'atelier logiciel change et s'appelle Rodin.