Bibliographie & annexes
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.
L'expertise technique et scientifique de référence
DOI (Digital Object Identifier)
Cet article fait partie de l’offre
Sécurité et gestion des risques
(475 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Présentation
Limites de B5. Avantages actuels de la méthode B vis-à-vis d'autres méthodes
La méthode B, qui n'est pas la seule méthode formelle, ni probablement la plus efficace sur l'ensemble des aspects rencontrés dans les projets, présente des avantages certains sur de nombreux points. On dispose d'abord d'une méthode unique pour spécifier, concevoir et prouver. Il n'est donc pas nécessaire de modéliser la spécification du logiciel pour la prouver, une telle modélisation pouvant conduire à des contradictions liées soit à l'interprétation qui en a été faite, soit aux limites et aux contraintes du modèle lui-même. L'efficacité s'est révélée grande pour des logiciels pas spécialement simples, et cette efficacité a tendance à s'améliorer à mesure que l'on conçoit d'autres systèmes compte tenu de l'expérience acquise. Cette expérience peut porter sur les architectures et l'organisation des modules, l'accumulation de nouveaux théorèmes plus performants augmentant le pourcentage de preuves réalisées automatiquement, sur un meilleur choix de stratégie de preuve facilitant la preuve, sur la réutilisation partielle ou totale de machines sur étagères.
La garantie par les preuves est sans commune mesure avec le fait de tracer les exigences et d'en vérifier les transformations successives. Le principe même de la preuve intégrée directement dans la conception impose nécessairement une grande rigueur et précision dans l'écriture du langage. L'intégration de la qualité à la conception est un atout important. On obtient de manière générale un logiciel bien construit et une architecture saine car la preuve se révèle souvent impossible lorsque l'objet à prouver n'est pas construit de manière suffisamment simple.
Des preuves peuvent être faites à chaque étape en commençant par le niveau le plus abstrait, ce qui permet d'être sûr au plus tôt, alors que, dans le développement d'un logiciel classique, on attend la fin des tests d'intégration pour être sûr de la qualité du développement sans d'ailleurs être assuré que la spécification relative aux différents niveaux d'intégration est correcte. Dans les deux cas, dans un développement en B ou dans un développement classique, la validation fonctionnelle reste indispensable. Cela signifie qu'une erreur à ce niveau peut coûter très chère.
Le nombre d'itérations nécessaire pour obtenir un logiciel correct est beaucoup plus faible dans le développement formel que dans un développement classique, ce...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Sécurité et gestion des risques
(475 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
Avantages actuels de la méthode B vis-à-vis d'autres méthodes
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
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Sécurité et gestion des risques
(475 articles en ce moment)
Cette offre vous donne accès à :
Une base complète d’articles
Actualisée et enrichie d’articles validés par nos comités scientifiques
Des services
Un ensemble d'outils exclusifs en complément des ressources
Un Parcours Pratique
Opérationnel et didactique, pour garantir l'acquisition des compétences transverses
Doc & Quiz
Des articles interactifs avec des quiz, pour une lecture constructive
