Méthode B

{{#ifeq:||Un article de Ziki, l'encyclopédie libre.|Une page de Ziki, l'encyclopédie libre.}}
Révision datée du 9 octobre 2023 à 12:22 par >GuiGeek (Titre et expaces manquantes)
(diff) ← Version précédente | Voir la version actuelle (diff) | Version suivante → (diff)

Modèle:Confusion Modèle:Méta bandeau d'avertissement{{#ifeq:||{{#ifeq:||[[{{#ifexist:Catégorie:Article à vérifier{{#if:informatique|/informatique}}|Catégorie:Article à vérifier{{#if:informatique|/informatique}}|Catégorie:Article à vérifier}}|Méthode B]]{{#if:décembre 2016||}}}}|}}

La méthode B est une méthode formelle qui permet le raisonnement sur des systèmes complexes<ref name="clicknprove">Modèle:Article</ref> 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<ref>Jean-Raymond Abrial, The B-Book, Assigning Programs to Meanings, Cambridge University Press, 1996, Modèle:ISBN </ref>. L'outil logiciel de support est l'atelier B ou le B-Toolkit <ref name="atelierb">http://www.atelierb.eu/ : un outil de développement en B</ref>, <ref name="btoolkit">http://www.b-core.com/btoolkit.html : un outil de développement en B</ref>.
  • 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<ref name="atelierb" />.
  • 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<ref>http://rodin-b-sharp.sourceforge.net/ : Le projet Rodin qui a pour objectif de développer une plate-forme de développement ouverte</ref>.
Fichier:Click'n'prove project view.png
Vue d'un projet et d'une machine dans Click'n'Prove.
Fichier:Click'n'prove proof interaction.png
Travail sur une preuve dans Click'n'Prove.
Fichier:Screen rodin.png
Travail sur une preuve dans Rodin.

Historique de B

Le langage B a été conçu par J.R.Abrial, qui était un des principaux concepteurs de Z dans les années 1980, avec le concours de G. Laffitte, F. Mejia et I. Mc Neal. Il est fondé sur les travaux scientifiques de E.W. Dijkstra, C.A.R. Hoare, C.B. Jones, C. Morgan, He Jifeng (du 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

La première conférence sur le B a eu lieu en France à Nantes les 25, 26 et Modèle:Date- 1996.

La méthode B a été utilisé avec succès pour plusieurs applications industrielles. On peut citer le développement du logiciel embarqué pour la ligne 14 du métro parisien (METEOR) qui a été modélisé, prouvé et généré à partir de spécifications formelles B. En 2005, la RATP décide d'automatiser la ligne 1 et fait de nouveau appel à la méthode B pour le logiciel embarqué. Depuis 1995, de nombreux pilotes automatiques de métros ont été développés, notamment Barcelone, Delhi, Lausanne, Madrid, New York, Pékin (à l'occasion des Jeux Olympiques), Séoul ou encore Singapour. Le pilote automatique de canton de la navette de l'aéroport Charles de Gaulle fait partie des développements B. Enfin plusieurs métros en cours de développement ou de rénovation font appel à la méthode B pour le développement de logiciels embarqués : Istanbul, Le Caire, Milan, Sao Paulo, Shangai ou encore Toronto.

En 1996, J.R. Abrial publie l'ouvrage The B-Book, Assigning programs to meanings. Il publie en 2010 un autre ouvrage sur le B événementiel : Modeling in Event-B, Hardback.

Objectifs de B

D'un point de vue purement théorique, l'objectif de la méthode B est de prouver qu'il n'y a pas d'écart entre la spécification et le code exécuté.

Alors que les méthodes basées sur des tests permettent juste d'affirmer que les testeurs n'en ont pas trouvé ; et ce, quel que soit le niveau d'automatisation de la génération des scénarios de tests et les moyens mis en œuvre.

Ainsi, le manque de temps et de moyens (forte contrainte dans l'industrie), conduira à un programme inutilisable (car non prouvé), là où les méthodes concurrentes conduisent à des programmes "bugués".

De ce fait, l'utilisateur final ou le commanditaire peut avoir une grande confiance dans le programme. Cette confiance est en particulier essentielle, voire obligatoire, dans le secteur des transports, notamment en aéronautique avec la norme DO-178B ou en ferroviaire (CENELEC EN 50128) car la sécurité des usagers est primordiale.

B couvre la spécification, la conception par raffinements successifs, l'architecture en couches et la traduction en code source (exemple : Ada, C) ; cela permet la mise en œuvre d'optimisations de "haut niveau" ; par exemple :

  • d'écrire les propriétés des éléments à sélectionner dans un ensemble (de contrainte à faire respecter à un train) de manière compréhensible du client final,
  • d'implémenter cette recherche de manière efficace d'un point de vue temps d'exécution (grâce à toute sorte d'optimisations très éloignées de la spécification initiale, notamment du pré-calcul des informations constantes ou des tables de recherches "inversées")
  • de prouver ensuite que la spécification est respectée quelle que soit la branche du code parcourue (y compris dans les cas atypiques mais qui finiront par arriver)

B ne couvre pas la génération du programme exécutable final (exemple .exe) et donc l'optimisation bas niveau, laissant cela aux compilateurs spécialisés.

Exemples

Un exemple de machine abstraite et de son raffinement

Nous avons utilisé la notation ASCII de B:

  • « : » représente l'appartenance ensembliste
  • « <: » l'inclusion
  • « & » le "et" logique
  • « :: » le "devient appartient" (un choix indéterministe d'un élément d'un ensemble)
  • les « || » la substitution parallèle.
  • « NAT » correspond quant à lui à l'ensemble des entiers naturels.

<syntaxhighlight lang="text"> 

MACHINE
	swap
VARIABLES
	xx, yy
INVARIANT
	xx : NAT & yy : NAT
INITIALISATION
	xx :: NAT ||
	yy :: NAT
OPERATIONS
	echange =
	BEGIN
		xx := yy
	||	yy := xx
	END
END

/* La substitution séquencement est interdite dans
   les machines abstraites, ceci afin de forcer à l'abstraction */
REFINEMENT
	swapR
REFINES
	swap
VARIABLES
	xr, yr, zr
INVARIANT
	xr= xx & yr = yy & zr : NAT
INITIALISATION
	xr, yr, zr:= 0, 0, 0
OPERATIONS
	echange =
	BEGIN
		zr := xr
	;	xr := yr
	;	yr := zr
	END
END

</syntaxhighlight>

Un exemple d'utilisation de primitives de composition de machines, le SEES et l'INCLUDES

<syntaxhighlight lang="text"> 

MACHINE
	trucM4(AA, maxe)
/* machine paramétrée par un SET et un scalaire */
CONSTRAINTS
	maxe : 5..10 &
	card(AA) >maxe
VARIABLES
	var
INVARIANT
	var <: AA &
	card(var) < maxe +1
INITIALISATION
	var := {}
OPERATIONS
	trucM1op =
		ANY ens WHERE ens <: AA & card(ens) < maxe+ 1 THEN
			var := ens
		END
END
MACHINE
	trucM5(AA,maxe)
CONSTRAINTS
	maxe : 5..10 & card(AA)> maxe
INCLUDES
	tien.trucM4(AA, maxe), mon.trucM4(AA, maxe)
OPERATIONS
	optrucM2 =
		BEGIN
		tien.trucM1op ||
		mon.trucM1op
		END
END

</syntaxhighlight>

Conférences internationales sur B

Références

Modèle:Références

Bibliographie

  • Recensement bibliographique au format BibTeX (lien externe)
  • The B Book, Assigning Programs to Meanings, Cambridge University Press, Cambridge, 1996, Modèle:ISBN, ouvrage fondateur de la méthode B.
  • Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control, LNCS, Springer, 1997
  • Steve Schneider, The B-method, an introduction, Palgrave, 2001, Modèle:ISBN (lien externe)
  • E. Sekerinski and K. Sere (editors ), Case Studies Using the B Method, Springer, Modèle:ISBN
  • John Wordsworth, Software Engineering with B, Addison-Wesley, Modèle:ISBN
  • Kevin Lano, The B Language and Method: A guide to Practical Formal Development, Springer Verlag London Ltd., Modèle:ISBN
  • Henri Habrias et al., Spécification formelle avec B, Hermes Lavoisier, Modèle:ISBN ([1])
  • J.R. Abrial, Extending B without changing it in H. Habrias (edit), First B Conference, p. 160-170, 1996
  • J.R. Abrial, Cours d'introduction à B, Etudes de cas et Cours Logique et Preuve, Cassettes vidéo, diffusées par le département informatique de l'I.U.T. de Nantes, 1997
  • J.R. Abrial, Modeling in Event-B, Hardback, Cambridge University Press, 2010, Modèle:ISBN ([2])
  • J.R. Abrial, The B Book en chinois http://www.china-pub.com/19779

Articles connexes

Modèle:Autres projets

  • B-Toolkit, outil développé par la société B-Core

Liens externes

Les outils

  • ABTools Another B Tool : suite d'outils B développé avec ANTLR
  • Atelier B : outil industriel permettant une utilisation opérationnelle de la méthode B pour des développements logiciels.
  • B4free est la version gratuite [obsolète] du cœur de l'atelierB, s'utilise avec Click'n Prove. Il est remplacé depuis Modèle:Date- par la version communautaire de l'Atelier B.
  • Bart : outil de raffinement automatique
  • Brama Outil de modélisation graphique appliqué aux méthodes formelles. B.
  • ComenC Traducteur de modèles B vers le langage C.
  • CompoSys Méthode et outil pour des descriptions formelles de systèmes.
  • RODIN, plateforme B-évènementiel basée sur Eclipse
  • ABtools
  • BATCAVE
  • BRILLANT: projet de développement open-source d'outils supportant la méthode B.
  • jBtools
  • DumBeX Traducteur de notation B vers \LaTeX


Modèle:Portail

Récupérée de « https://wiki.trucsazeb.re:443/index.php?title=Méthode_B&oldid=109381 »