Méthode B - Définition et Explications

Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs est disponible ici.

La méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite dans le langage de 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é (Le terme d'activité peut désigner une profession.) de preuve formelle permet de vérifier la cohérence du modèle abstrait et la conformité de chaque raffinement (En informatique, le raffinement consiste à avoir une approche de conception où on affine à chaque étape le niveau de détails ; le but étant d'atteindre le niveau de granularité. On appelle aussi cette approche,...) avec le modèle supérieur (prouvant ainsi la conformité de l'ensemble (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme un tout », comme...) des implantations concrètes avec le modèle abstrait).

On distingue le :

  • B classique tel qu'il est définit dans le B Book de 1996 [1]. L'outil (Un outil est un objet finalisé utilisé par un être vivant dans le but d'augmenter son efficacité naturelle dans l'action. Cette augmentation se traduit par la simplification des actions entreprises, par une plus grande...) logiciel (En informatique, un logiciel est un ensemble d'informations relatives à des traitements effectués automatiquement par un appareil informatique. Y sont inclus les instructions de traitement, regroupées sous...) de support est l'atelierB [2].
  • 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). Du coup la méthode peut s'appliquer sur des systèmes variés comme de l'électronique et non plus seulement des programmes. On réalise alors des développements incrémentaux de systèmes prouvés. Pour cela on utilise toujours l'atelierB [2] mais conjointement avec Click'n'Prove [3]
  • 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[4].
Vue d'un projet et d'une machine dans Click'n'Prove.
Vue (La vue est le sens qui permet d'observer et d'analyser l'environnement par la réception et l'interprétation des rayonnements lumineux.) d'un projet (Un projet est un engagement irréversible de résultat incertain, non reproductible a priori à l’identique, nécessitant le concours et l’intégration d’une grande...) et d'une machine dans Click'n'Prove.
Travail sur une preuve dans Click'n'Prove.
Travail sur une preuve dans Click'n'Prove.

Historique de B

B, déjà une longue histoire (source : cours vidéo (La vidéo regroupe l'ensemble des techniques, technologie, permettant l'enregistrement ainsi que la restitution d'images animées, accompagnées ou non de son, sur...) 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.
  • Fondé sur les travaux scientifiques de E.W. Dijkstra, C.A.R. Hoare, C.B. Jones, C. Morgan, He Jifeng (Programming Research Group Université (Une université est un établissement d'enseignement supérieur dont l'objectif est la production du savoir (recherche), sa conservation et sa transmission (études supérieures). Aux États-Unis, au moment...) 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 (Edsger Wybe Dijkstra (né à Rotterdam le 11 mai 1930, mort à Nuenen le 6 août 2002) est un mathématicien et informaticien néerlandais du XXe siècle.), Guarded commands, nondeterminacy and formal derivation of programs, CACM
  • 1981 David Gries, The Science (La science (latin scientia, « connaissance ») est, d'après le dictionnaire Le Robert, « Ce que l'on sait pour l'avoir appris, ce que l'on tient pour vrai...) of Programming, Springer, 1981
  • 1986 Roland Backhouse, Program Construction and Verification, Prentice-Hall, 1986
  • 1986 Cliff B. Jones, Systematic Software Development (Development est une revue scientifique bimensuelle à comité de lecture couvrant tous les champs de la génétique évolutive du développement allant de la biologie...) using VDM, Prentice-Hall
  • 1988 C.A.R. Hoare, Jifeng He, Natural (Natural est un langage de programmation semi-compilé, édité par la société allemande Software AG.) 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 (La Régie autonome des transports parisiens (RATP) est une entreprise publique désignée par le STIF pour assurer la gestion du métro et d'autres transports urbains de Paris et de sa proche...) de la ligne de métro (Un métro, apocope du terme métropolitain lui-même abréviation de chemin de fer métropolitain, est un chemin de fer urbain souterrain le plus souvent, sur viaduc quelquefois, au sol rarement.) 14 (METEOR). Le logiciel critique (Un système critique est un système dont une panne peut avoir des conséquences dramatiques, tels des morts ou des blessés graves, des dommages matériels importants, ou des conséquences graves...) 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 (La méthode B est une méthode formelle de développement logiciel qui permet de modéliser de façon abstraite dans le langage de B le comportement d'un programme, puis par raffinements successifs,...).

Objectifs de B

  • Formaliser la spécification,
  • Expliciter la conception,
  • Simplifier la programmation (La programmation dans le domaine informatique est l'ensemble des activités qui permettent l'écriture des programmes informatiques. C'est une étape importante de la conception de...).

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 (L’architecture peut se définir comme l’art de bâtir des édifices.) en couches,
  • La génération du code exécutable.

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.

 
 MACHINE 
 swap 
 VARIABLES 
 xx, yy 
 INVARIANT 
 xx: NAT & yy: NAT 
 INITIALISATION 
 xx:: NAT || 
 yy:: NAT 
 OPERATIONS 
 echange = 
 BEGIN 
 xx:= yy || 
 yy:= xx 
 END 
 END 
 /* noter que la substitution séquencement est interdite dans 
 les machines abstraites. Ceci afin de forcer à l'abstraction ( 
 En philosophie, l'abstraction désigne à la fois une opération qui consiste a isoler par la pensée une ou plusieurs qualités d'un objet concret pour en former une représentation...) */ 
 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 
 

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

 
 MACHINE 
 trucM4(AA, maxe) 
 /* machine paramétrée par un SET et un scalaire (Un vrai scalaire est un nombre qui est indépendant du choix de la base choisie pour exprimer les vecteurs, par opposition à un pseudoscalaire, qui est un nombre qui peut dépendre de la base.) */ 
 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 
 

Conférences internationales sur B

Cet article vous a plus ? Partagez-le sur les réseaux sociaux avec vos amis !
Page générée en 0.055 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique