Méthode_B

Un article de Wikipedia.y-project.com.

La méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite en langage B le comportement d'un programme, puis par raffinements successifs, d'aboutir à un modèle concret, sous-ensemble du langage transcodable en Ada ou en C.

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 implantations concrètes avec le modèle abstrait).

On distingue le « B classique » du « B événementiel », ce dernier étant proche des « Actions Systems ».

Sommaire 1 Historique de B 2 Objectifs de B 3 B méthode formelle 4 Couverture de B 5 Liens internes 6 Conférences internationales sur B 7 Bibliographie 8 Liens externes

[] Historique de B

B, déjà une longue histoire (source : cours vidéo de J.R. Abrial)

• A été conçu par J.R.Abrial (un des principaux concepteurs de Z dans les années 80).

• Concours de : G. Laffitte, F. Meija et I. Mc Neal.

• Basé sur les travaux scientifiques de E.W. Dijkstra, C.A.R. Hoare, C.B. Jones, C. Morgan, He Jifeng (Programming Research Group Université d'Oxford).

B s'inscrit dans une longue filiation de recherches fondamentales :

• 1949 Alan M. Turing, Checking a large routine, Cambridge University
• 1967 Robert Floyd, Assigning meanings to programs, AMS
• 1969 C.A.R. Hoare, An axiomatic basis for computer programming,
  CACM
• 1972 D.L. Parnas, A Technique for Software Module Specification with Examples, CACM
• 1975 Edsger Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, CACM
• 1981 David Gries, The Science of Programming, Springer, 1981
• 1986 Roland Backhouse, Program Construction and Verification, Prentice-Hall, 1986
• 1986 Cliff B. Jones, Systematic Software Development using VDM, Prentice-Hall
• 1988 C.A.R. Hoare, Jifeng He, Natural transformations and data refinement, PRG, Oxford
• 1990 C. Morgan, Programming from Specifications, Prentice-Hall
• 1996 J.R. Abrial, The B-Book, Assigning programs to meanings, Cambridge University Press
• 1996 25-26-27 novembre, First B conference in Nantes (France)

Et présente également plusieurs utilisation industrielles exemplaires dont :

• 1998 Mise en service par la RATP de la ligne de métro 14 (METEOR). Le logiciel critique embarqué a été modélisé, prouvé et généré à partir de spécifications formelles B.
• 2005 La RATP décide d'automatiser la ligne 1 (La défense/Vincennes) et d'utiliser à nouveau la méthode B.

[] Objectifs de B

• Formaliser la spécification,
• Expliciter la conception,
• Simplifier la programmation.

[] B méthode formelle

• Car toutes les activités sont validées par des preuves formelles.

[] Couverture de B

B couvre :

• La spécification,
• La conception par raffinements successifs,
• L'architecture en couches,
• La génération du code exécutable.

[] Liens internes

[] Conférences internationales sur B

• Après la conférence Z2B de Nantes (oct. 10-12 1995) ,
• puis la première conférence B de Nantes (nov. 25-27 1996),
• puis la deuxième à Montpellier (avril 22-24 1998),
• il y a eu des conférences à peu près tous les 18 mois, ZB'2000 à York (U.K.) 28 août, 2 sept. 2000), ZB'2002 Grenoble (F) (23-25 janv. 2002), ZB'2003, Turku (Finlande) (4-6 juin), ZB'05, Guildford (U.K.)

[] Bibliographie

• Recensement bibliographique au format BibTeX (lien externe)
• Jean-Raymond Abrial, The B-Book, Assigning Programs to Meanings , Cambridge University Press, 1996, ISBN 0521496195
• Steve Schneider, The B-method, an introduction, Palgrave, 2001, ISBN 033379284X (lien externe)
• E. Sekerinski and K. Sere (editors ), Case Studies Using the B Method, Springer, ISBN : 0-52149619-5
• John Wordsworth, Software Engineering with B, Addison-Wesley, ISBN : 0201403560
• Kevin Lano, The B Language and Method: A guide to Practical Formal Development, Springer Verlag London Ltd., ISBN : 3-540-76033-4
• Henri Habrias et al., Introduction à la méthode B, Lavoisier Hermes, 2001, ISBN 2746203022 (lien externe)

[] Liens externes

• https://gna.org/projects/brillant/ : projet de développement open-source d'outils supportant la méthode B.
• http://www.atelierb.societe.com/ : l'outil de développement en B.
• http://b4free.com/ : B4free est la version gratuite (pour les universitaires) du c?ur de l'atelierB, s'utilise avec la Balbulette.
• http://www.loria.fr/~cansell/cnp.html : le site de la balbulette (Click'n'Prove en Anglais), interface xemacs gratuite pour B4free.
• http://www.clearsy.com/html/b.htm : la société assurant le développement de cet outil.
• http://www-lsr.imag.fr/B/ : le site B de Grenoble.
• http://rodin-b-sharp.sourceforge.net/ : Le projet Rodin qui a pour objectif de développer une plate-forme de développement ouverte.
• http://vl.fmnet.info/b/ : The B-Method (L'information en anglais).
• Qui enseigne B dans le monde ?

 
Le Texte ci-dessus est disponible sous GNU Free Documentation License.
La source est wikipedia http://fr.wikipedia.org/wiki/Méthode B