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
B Système ou B événementiel6. Limites de B
Malgré tous ces avantages, la méthode B classique est limitée sur un certain nombre de points qui ne sont d'ailleurs pas liés à la méthode elle-même. La figure 8 donne les différentes interfaces de B avec l'environnement qui est constitué de la spécification en langage naturel (entrée de B), les entrées (informations acquises : autres logiciels, autres calculateurs, capteurs, moyens de transmission) et les sorties (informations fournies : vers autres logiciels, autres calculateurs, actionneurs ou moyens de transmission), les données et paramètres de l'application en B, les parties non-sécuritaires non-réalisées en B, le codage et la compilation pour obtenir des PROM (mémoire morte où se trouve le programme qui sera exécuté par le calculateur industriel si c'est le cas). Ces limitations signifient que la preuve ne peut porter sur ces points. Il est donc important d'en être conscient, afin de mettre en place les moyens supplémentaires nécessaires pour garantir l'ensemble.
6.1 Lien avec la spécification de plus haut niveau (souvent en langage naturel)
Nous avons déjà vu que la spécification formelle est issue de la spécification en langage naturelle. D'une part, cette dernière peut être erronée, et d'autre part, la traduction en formelle peut faire l'objet d'erreurs d'interprétation. La preuve, si elle est apportée, n'indique la correction (la validité) que par rapport à la spécification formelle. On n'est donc pas assuré que le logiciel fasse ce qui lui est effectivement demandé. On a vu qu'une analyse peut être effectuée si la preuve n'aboutit pas, de manière automatique, de manière manuelle ou après insertion de nouvelles règles, et être amené à corriger ou à compléter la spécification textuelle. Plus la spécification formelle est à un niveau élevé, meilleur c'est, car il est possible de trouver des propriétés plus globale au niveau système, sans être noyé dans un nombre important de propriétés peut-être plus simples mais dont la cohérence d'ensemble sera plus difficile à démontrer. De plus, le fait de disposer de propriétés de plus haut niveau permet de mieux maîtriser les évolutions, car celles-ci « bordent » mieux le logiciel globalement en garantissant les interfaces entre les modules logiciels eux-mêmes et le logiciel et l'extérieur.
...
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
Limites de B
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
