Méthode B

La méthode B est une méthode de développement de logiciels basée sur B , une méthode formelle assistée par outil basée sur une notation machine abstraite , utilisée dans le développement de logiciels informatiques .

B a été développé à l'origine dans les années 1980 par Jean-Raymond Abrial en France et au Royaume-Uni . B est lié à la notation Z (également créée par Abrial) et prend en charge le développement de code de langage de programmation à partir de spécifications. B a été utilisé dans les principales applications de systèmes critiques pour la sécurité en Europe (comme les lignes automatiques 14 et 1 du métro parisien et la fusée Ariane 5 ). Il dispose d'un support d'outils robuste et disponible dans le commerce pour la spécification , la conception , la preuve et la génération de code .

Par rapport à Z, B est légèrement plus bas niveau et plus axé sur le raffinement du code plutôt que sur une simple spécification formelle . Il est donc plus facile d'implémenter correctement une spécification écrite en B qu'en Z. En particulier, il existe un bon support d'outils pour cela. Le même langage est utilisé dans la spécification, la conception et la programmation. Les mécanismes incluent l'encapsulation et la localité des données.

Par la suite, une autre méthode formelle appelée Event-B a été développée sur la base de la méthode B, supportée par la plateforme Rodin. Event-B est une méthode formelle destinée à la modélisation et à l'analyse au niveau système. Les caractéristiques d'Event-B sont l'utilisation de la théorie des ensembles pour la modélisation, l'utilisation du raffinement pour représenter les systèmes à différents niveaux d'abstraction et l'utilisation de preuves mathématiques pour vérifier la cohérence entre ces niveaux de raffinement.

La notation B s'appuie sur la théorie des ensembles et la logique du premier ordre afin de spécifier différentes versions de logiciels couvrant le cycle complet de développement du projet.

Dans la première version, la plus abstraite, appelée Abstract Machine , le concepteur doit spécifier l'objectif de la conception.

• Ensuite, lors d'une étape de raffinement, ils peuvent compléter la spécification afin de clarifier l'objectif ou de rendre la machine abstraite plus concrète en ajoutant des détails sur les structures de données et les algorithmes qui définissent comment l'objectif est atteint.
• La nouvelle version, appelée Refinement , devrait s'avérer cohérente et inclure toutes les propriétés de la machine abstraite.
• Le concepteur peut utiliser des bibliothèques B afin de modéliser des structures de données ou d'inclure ou d'importer des composants existants.

• Le raffinement se poursuit jusqu’à ce qu’une version déterministe soit obtenue : l’ Implémentation .
• Durant toutes les étapes de développement, la même notation est utilisée et la dernière version peut être traduite dans un langage de programmation pour la compilation.

Le B-Toolkit est un ensemble d'outils de programmation conçus pour prendre en charge l'utilisation du B-Tool, est un interpréteur mathématique basé sur la théorie des ensembles, dans le but de prendre en charge la méthode B. Le développement a été initialement entrepris par Ib Holm Sørensen et d'autres, chez BP Research, puis chez B-Core (UK) Limited.

La boîte à outils utilise une interface X Window Motif personnalisée pour la gestion de l'interface graphique et fonctionne principalement sur les systèmes d'exploitation Linux , Mac OS X et Solaris .

Le code source du B-Toolkit est désormais disponible.

Développé par ClearSy, Atelier B est un outil industriel qui permet l'utilisation opérationnelle de la Méthode B pour développer des logiciels éprouvés sans défaut (logiciels formels). Deux versions sont disponibles : 1) Community Edition accessible à tous sans aucune restriction ; 2) Maintenance Edition réservée aux seuls détenteurs de contrats de maintenance. Atelier B a été utilisé pour développer des automatismes de sécurité pour les différents métros installés dans le monde par Alstom et Siemens , ainsi que pour la certification Critères Communs et le développement de modèles de systèmes par ATMEL et STMicroelectronics .

La plateforme Rodin est un outil qui prend en charge Event-B. Rodin est basé sur un IDE logiciel Eclipse ( environnement de développement intégré ) et fournit un support pour le raffinement et la preuve mathématique . La plateforme est open source et fait partie du framework Eclipse. Elle est extensible à l'aide de plug-ins de composants logiciels . Le développement de Rodin a été soutenu par les projets de l'Union européenne DEPLOY (2008-2012), RODIN (2004-2007) et ADVANCE (2011-2014).

BHDL fournit une méthode pour la conception correcte des circuits numériques , combinant les avantages du langage de description matérielle VHDL avec la formalité de B.

L'APCB ( en français : Association de Pilotage des Conférences B ) a organisé des réunions liées à la méthode B. Elle a organisé des conférences ZB avec le Z User Group et des conférences ABZ, notamment sur les machines à états abstraits (ASM) ainsi que sur la notation Z.

• Le B-Book : Attribuer des programmes à des significations , Jean-Raymond Abrial , Cambridge University Press , 1996. ISBN 0-521-49619-5 .
• La méthode B : une introduction , Steve Schneider, Palgrave Macmillan , série Cornerstones of Computing, 2001. ISBN 0-333-79284-X .
• Ingénierie logicielle avec B , John Wordsworth, Addison Wesley Longman , 1996. ISBN 0-201-40356-0 .
• Le langage et la méthode B : un guide pour le développement formel pratique , Kevin Lano , Springer-Verlag , série FACIT, 1996. ISBN 3-540-76033-4 .
• Spécification en B : Une introduction à l'aide de la boîte à outils B , Kevin Lano , World Scientific Publishing Company , Imperial College Press , 1996. ISBN 1-86094-008-0 .
• Modélisation en événement-B : ingénierie système et logicielle , Jean-Raymond Abrial , Cambridge University Press , 2010. ISBN 978-0-521-89556-9 .

Les conférences suivantes ont explicitement inclus la Méthode B et/ou l'Evénement-B :

• Conférence Z2B, Nantes , France , 10–12 octobre 1995
• Première conférence B, Nantes, France, 25-27 novembre 1996
• Deuxième conférence B, Montpellier , France, 22-24 avril 1998
• ZB 2000, York , Royaume-Uni , 28 août – 2 septembre 2000
• ZB 2002, Grenoble , France, 23-25 ​​janvier 2002
• ZB 2003, Turku , Finlande , 4-6 juin 2003
• ZB 2005, Guildford , Royaume-Uni, 2005
• B 2007, Besançon , France, 2007
• B, de la recherche à l'enseignement, Nantes, France, 16 juin 2008
• B, de la recherche à l'enseignement, Nantes, France, 8 juin 2009
• B, de la recherche à l'enseignement, Nantes, France, 7 juin 2010
• ABZ 2008, British Computer Society , Londres , Royaume-Uni, 16-18 septembre 2008
• ABZ 2010, Orford , Québec , Canada , 23-25 ​​février 2010
• ABZ 2012, Pise , Italie , 18-22 juin 2012
• ABZ 2014, Toulouse , France, 2-6 juin 2014
• ABZ 2016, Linz , Autriche , 23-27 mai 2016
• ABZ 2018, Southampton , Royaume-Uni, 2018
• ABZ 2020, Ulm , Allemagne , 2021 (retardé en raison de la pandémie de COVID-19 )
• ABZ 2021, Ulm, Allemagne, 2021