Présentation
Auteur(s)
-
Jacques valancogne : IMdR - Membre du Conseil scientifique du CSFRS (Conseil supérieur de la Formation et de la Recherche stratégiques)
Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.
Lire l’articleINTRODUCTION
L'objectif de cet article ne vise pas à ce que le lecteur puisse tout connaître sur la méthode B ; ce serait impossible et prétentieux. The B-BOOK – Assigning Programs to Meanings de Jean-Raymond ABRIAL, l'inventeur de la méthode B, qui est à la base du langage B, possède déjà plus de 750 pages et est basé sur de nombreuses connaissances en mathématiques et en logique ; de plus, de nombreuses formations sur la méthode B existent aujourd'hui. L'objectif se limitera à donner des éclairages pour mieux porter une appréciation sur une telle méthode en essayant d'en comprendre les principaux concepts. Il n'est donc pas question de trop développer les aspects mathématiques, bien que ceux-ci soient essentiels. Le propos restera toujours assez général, en simplifiant volontairement parfois pour rester compréhensible.
Cet article est réservé aux abonnés.
Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
DOI (Digital Object Identifier)
Présentation
Méthode B et le processus de réalisation des logicielsArticle inclus dans l'offre
"Sécurité et gestion des risques"
(483 articles)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
3. Principes de la méthode B
Il y a seulement quelques décennies, l'unique formalisme utilisé dans un logiciel était celui du code, qui était obligatoire si l'on voulait que la machine comprenne ce qu'on lui demandait d'exécuter ! Pour donner une définition simple, la méthode B est une méthode pour spécifier, concevoir, coder et prouver des logiciels de manière rigoureuse et progressive.
3.1 Principes généraux de la méthode B
Cette méthode utilise un langage mathématique unique tout au long du processus de conception afin de permettre la vérification de chaque étape à l'aide de preuves mathématiques. La difficulté de la vérification de toutes les transformations qui font passer de la spécification initiale au code (voir B0) qui sera transformé dans un langage classique, se trouve par là même résolue. C'est une méthode progressive, le langage lui-même prenant en compte l'aspect preuve, un modèle supplémentaire n'est donc pas nécessaire.
La méthode B est donc plus qu'un langage de programmation car elle introduit en elle-même la possibilité de vérification. En effet, il n'est pas nécessaire de réaliser une modélisation supplémentaire et d'effectuer une comparaison pour vérifier si ce qui a été fait est correct. Bien appliqué (nous verrons ce que cela signifie), B est un langage intrinsèquement sûr. On peut comparer le concept utilisé dans la méthode au concept de sécurité intrinsèque (false-safe ) qui a cours au niveau de la sécurité du matériel.
la sécurité intrinsèque suit la règle suivante : toute défaillance ou ensemble de défaillances qui pourrait se révéler contraire à la sécurité doit être détectée par la conception même du système de manière à positionner l'état du système dans un état sûr. Pour un logiciel, la preuve, si elle ne peut être faite, montre que celui-ci a probablement une anomalie.
Les bases mathématiques sur lesquelles est fondée la méthode apportent la rigueur et la notation proposée élimine les ambigüités bien connues du langage naturel, source d'erreur parfois très grave. La vérification mathématique de chaque étape est si étroitement imbriquée qu'il est impossible de séparer les choix de conception du processus de vérification garantissant...
Cet article est réservé aux abonnés.
Il vous reste 95 % à découvrir.
Déjà abonné ? Se connecter
Principes de la méthode B
Article inclus dans l'offre
"Sécurité et gestion des risques"
(483 articles)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
BIBLIOGRAPHIE
-
(1) - ABRIAL (J.-R.) - The B-book assigning programs to meanings (ouvrage fondateur de la méthode B). - Cambridge University Press (1996).
-
(2) - BEHM (P.) - Formal development of safety critical software of METEOR (ligne 14 du Métro Parisien mise en service en 1998). - First B Conference, Nantes (1996).
-
(3) - BEHM (P.), DESFORGES (P.), MEIJA (F.) - Application de la méthode B dans l'industrie ferroviaire. - ARAGO 20.
-
(4) - LANO (K.) - The B language and method : a guide to practical formal development FACIT. - Springer Verlag, London Ltd. (1996).
-
(5) - LANO (K.), HAUGHTON (H.) - Specification in B : an introduction using the B toolkit imperial college press. - London (1996).
-
(6) - WORDSWORTH (J.) - Software engineering with B. - Addison-Wesley (1996).
-
...
DANS NOS BASES DOCUMENTAIRES
Cet article est réservé aux abonnés.
Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Article inclus dans l'offre
"Sécurité et gestion des risques"
(483 articles)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
