Méthode B - B-Method

La méthode B est une méthode de développement logiciel basée sur B , une méthode formelle assistée par un outil basée sur une notation machine abstraite , utilisée dans le développement de logiciels informatiques . Il 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 des systèmes critiques pour la sécurité en Europe (comme les lignes automatiques 14 et 1 du métro de Paris et la fusée Ariane 5 ). Il prend en charge des outils robustes et disponibles 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'une en Z. En particulier, il existe une bonne prise en charge des outils pour cette. Le même langage est utilisé dans les spécifications, la conception et la programmation. Les mécanismes incluent l' encapsulation et la localisation des données.

Par la suite, une autre méthode formelle appelée Event-B a été développée. L'événement-B est considéré comme une évolution de B (également connu sous le nom de B classique). C'est une notation plus simple, plus facile à apprendre et à utiliser. Il est livré avec un support d'outil sous la forme de l' outil Rodin .

Les principaux composants

La notation B dépend de la théorie des ensembles et de la logique du premier ordre afin de spécifier différentes versions du logiciel qui couvrent le cycle complet de développement du projet.

Machine abstraite

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

Raffinement

  • Ensuite, lors d'une étape de raffinement, il peut 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, qui s'appelle Raffinement , 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 pour modéliser des structures de données ou pour inclure ou importer des composants existants.

Mise en œuvre

  • Le raffinement se poursuit jusqu'à ce qu'une version déterministe soit atteinte : l' Implémentation .
  • Pendant 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.

Logiciel

B-Boîte à outils

Le B-Toolkit , développé par Ib Holm Sørensen et al. , est une collection d'outils de programmation conçus pour prendre en charge l'utilisation du B-Tool, un interpréteur mathématique basé sur la théorie des ensembles, aux fins d'une méthodologie formelle de génie logiciel connue sous le nom de méthode B.

La boîte à outils utilise une interface X Window Motif personnalisée pour la gestion de l'interface graphique et s'exécute principalement sur les systèmes d' exploitation Linux , Mac OS X et Solaris . Il a été développé par la société britannique B-Core (UK) Limited.

Le code source du B-Toolkit est maintenant disponible.

Atelier B

Développé par ClearSy, l'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 (logiciel formel). Deux versions sont disponibles : Community Edition accessible à tous sans aucune restriction, Maintenance Edition réservée aux titulaires d'un contrat de maintenance.

Il est utilisé pour développer les automatismes de sécurité des 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 .

Livres

  • The B-Book: Assigning Programs to Meanings , 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 .
  • Génie logiciel 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 utilisant la boîte à outils B , Kevin Lano , World Scientific Publishing Company , Imperial College Press , 1996. ISBN  1-86094-008-0 .
  • Modélisation dans Event-B: System and Software Engineering , Jean-Raymond Abrial , Cambridge University Press , 2010. ISBN  978-0-521-89556-9 .

Conférences

  • Conférence Z2B, Nantes, France, oct. 10-12 1995
  • Première conférence B, Nantes, France, nov. 25-27 1996
  • Deuxième conférence B, Montpellier, France, ap. 22-24 1998,
  • ZB'2000, York, Royaume-Uni, 28 août, 2 sept. 2000,
  • ZB'2002, Grenoble, France, 23-25 ​​janv. 2002,
  • ZB'2003, Turku, Finlande, 4-6 juin. 2003
  • ZB'05, 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
  • Conférence ABZ : ABZ 2008, British Computer Society, Londres, Royaume-Uni, 16-18 septembre 2008
  • Conférence ABZ : ABZ 2010,Oxford, Québec, Canada, 23-25 ​​février 2010
  • Conférence ABZ : ABZ 2012, Pise, Italie, 18-22 juin 2012
  • Conférence ABZ : ABZ 2014, Toulouse, France, 2-6 juin 2014
  • Conférence ABZ : ABZ 2016, Linz, Autriche, 23-27 mai 2016

Voir également

  • APCB (Association de Pilotage des Conférences B)
  • BHDL

Les références

Liens externes

  • Méthode B.com : ce site est conçu pour présenter différents travaux et sujets concernant la méthode B, une méthode formelle avec preuve
  • Atelier B.eu : L'Atelier B est un atelier d'ingénierie système, qui permet de développer des logiciels garantis sans défaut
  • Site B Grenoble

Cet article est basé sur du matériel extrait du Dictionnaire gratuit en ligne de l'informatique avant le 1er novembre 2008 et incorporé sous les termes de "relicensing" de la GFDL , version 1.3 ou ultérieure.