Bibliographie & annexes
Présentation
English
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
(477 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
Applications industrielles
English
8. Autres aspects de B
8.1 Liens avec la spécification en langage naturel
Indépendamment du niveau d'abstraction choisi, pour écrire un modèle formel, un processus général est à appliquer, comprenant le choix des entités mathématiques les plus aptes à représenter ce que l'on veut représenter, l'énoncé des lois statiques ou dynamiques qui vont régir le comportement voulu ou observé du système. Plus le niveau est abstrait, plus le choix des entités mathématiques est délicat. Une spécification formelle ne doit pas, en principe, formaliser des traitements, mais des propriétés si l'on veut que cela présente un intérêt important en évitant les erreurs de haut niveau.
HAUT DE PAGE8.2 Peut-on utiliser d'autres méthodes avec B pour un même développement ?
Nous avons vu que B est une méthode complète qui évite des modélisations, et donc des formalismes supplémentaires pour vérifier ou valider. B Système permet de plus de traiter des spécifications de haut niveau. Si nous prenons l'exemple d'UML ou de SYSML, est-il intéressant de les utiliser à haut niveau puis B ou vice versa ? La réponse est négative car, d'une part, il est nécessaire de maîtriser deux formalismes différents et, d'autre part, il faut effectuer des vérifications au niveau du passage d'un modèle à l'autre. Si l'on commence par du B, il faut continuer en B (sauf si des parties ne sont pas critiques ou pas complexes) et si l'on débute par UML, il vaut mieux continuer jusqu'au bout en UML tout en ayant conscience de ses limites.
HAUT DE PAGE8.3 Bénéfice de la seule formalisation
L'utilisation du formel est intéressant, non seulement pour concevoir une solution, mais aussi pour clarifier et enlever les ambigüités par une formalisation descriptive ; cela suppose une retraduction du formel en langage naturel pour être compréhensible par ceux qui connaissent le système, mais pas forcément la méthode B. Notons aussi qu'il est intéressant de modéliser à plusieurs niveaux de raffinement prouvés entre eux pour faire le lien avec les différents niveaux de représentation naturelle pour décrire...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Sécurité et gestion des risques
(477 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
Autres aspects 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
(477 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
