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
(476 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
Principes de la méthode B2. Petit panorama des méthodes de fiabilisation des logiciels
Il existe de nombreuses méthodes (et outils associés) qui permettent d'améliorer la fiabilité des logiciels. Ces méthodes sont basées sur un formalisme parfois complexe qui autorise un niveau plus ou moins pertinent de vérification. Elles peuvent porter sur une phase particulière du cycle de développement ou sur l'ensemble des phases, sur certaines propriétés (statiques ou dynamiques) ou sur l'ensemble des propriétés du logiciel. L'effort est fonction bien entendu du champ sur lequel porte les méthodes. Un contrôle de type (comme le font la plupart des langages de programmation) est d'un apport moindre qu'une analyse statique, qui elle-même est moins efficace qu'une vérification par modèle ou qu'une abstraction automatisée. Le maximum de confiance est obtenu sur des logiciels développés avec un langage sur lequel on peut effectuer directement la preuve de théorèmes.
Pour éviter des erreurs sur le logiciel, on peut, pour chaque phase de la conception, disposer de plusieurs principes de solutions. Nous avons vu que les erreurs sont issues des transformations que l'on effectue successivement sur les exigences (transformations directes et/ou allocations). Pour vérifier qu'une transformation/allocation faisant passer de l'état i à l'état i + 1 a bien été effectuée, on peut :
-
1) comparer, en utilisant la transformation inverse du résultat, T (i + 1) · T1 (i + 1) à l'état initial T (i) ;
-
2) comparer, en utilisant une transformation analogue mais présentant une forme différente (un modèle de la transformation), T (i + 1) à T′ (i + 1) ;
-
3) s'assurer que la transformation est intrinsèquement sûre en y apportant une preuve mathématique.
Mais à une étape donnée de la réalisation du logiciel, il existe des méthodes plus ou moins complètes qui prennent en compte partiellement ou totalement les caractéristiques ou propriétés de l'exigence transformée. Certaines méthodes concernent plus l'aspect dynamique et comportemental, d'autres l'aspect statique dans lequel certaines se limitent à vérifier le typage (de variable par exemple), d'autres des caractéristiques générales (non division par zéro par exemple), d'autres enfin portent sur des caractéristiques plus spécifiques à l'application.
D'autres méthodes sont basées...
L'expertise technique et scientifique de référence
Cet article fait partie de l’offre
Sécurité et gestion des risques
(476 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
Petit panorama des méthodes de fiabilisation des logiciels
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
(476 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
