Remerciez-le!

Remerciez @Admin pour avoir partagé cet document gratuitement, de la manière la plus simple, en partageant sur les réseaux sociaux.

2020/2021 Table des matières 1 Introduction :..................................

2020/2021 Table des matières 1 Introduction :..................................................................................................................................2 2 Éléments du langage de la méthode B............................................................................................4 2.1.1 Opérations arithmétiques :..............................................................................................4 2.1.2 Les ensembles.................................................................................................................4 2.1.3 Les formules...................................................................................................................5 2.1.4 Relations et fonctions.....................................................................................................6 3 Historique de B :.............................................................................................................................8 4 OBJECTIFS DE LA MÉTHODE B :.............................................................................................9 5 Cas d’utilisation :..........................................................................................................................10 6 AVANTAGES ACTUELS DE LA MÉTHODE B VIS-À-VIS D'AUTRES MÉTHODES :.......10 7 LIMITES DE B :..........................................................................................................................11 8 Les outils :....................................................................................................................................11 9 Exemples :....................................................................................................................................12 10 Principe du raffinage :..............................................................................................................13 11 Conclusion :..............................................................................................................................14 12 -Références Bibliographiques –................................................................................................14 1 Introduction : C’est une méthode de spécification formelle qui permet, grâce à un langage adéquat, d’exprimer très rigoureusement les propriétés exigées dans un cahier des charges. Il est alors possible de prouver de manière automatisée que ces propriétés sont non ambiguës, cohérentes et non contradictoires. Cela nous permet de garantir ensuite par preuve mathématique que ces propriétés sont respectées au fur et à mesure des étapes de conception. Ainsi, cette méthode formelle et la preuve qui lui est associée permettent :  D’obtenir des spécifications techniques et des cahiers des charges système clairs, structurés, cohérents et sans ambiguïté,  De développer des logiciels garantis contractuellement sans défauts, Dans des domaines tels que le temps réel, les automatismes industriels, les protocoles de communication, les protocoles cryptographiques, l’informatique embarquée… La « méthode formelle B » évoque traditionnellement l’ensemble comprenant : le langage B, le raffinement, la preuve et les outils associés. Un développement B débute par l’écriture d’un modèle concret, reprenant tous les aspects du besoin. Les principales données sont manipulées par le système et sont décrites ainsi que les propriétés fondamentales de ces données. Des services assurent les transformations de ces données tout en préservant leurs propriétés. Le modèle B ainsi obtenu constitue 2 une spécification de ce que devra réaliser le système. Le modèle B est ensuite transformé (« raffiné » dans le vocabulaire B), jusqu’à obtenir une implantation logicielle complète du logiciel. Au final, nous aboutissons alors à un modèle concret, prouvé et sans défaut, transcodable dans le langage C ou Ada. La méthode formelle B est donc « une démarche de construction prouvée (dite correcte), sur la base du langage B, du raffinement et de la preuve ». 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 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. D'un point de vue purement théorique, l'objectif de la méthode B est de prouver qu'il n'y a pas d'écart entre la spécification et le code exécuté.Alors que les méthodes basées sur des tests permettent juste d'affirmer que les testeurs n'en ont pas trouvé ; et ce, quel que soit le niveau d'automatisation de la génération des scénarios de tests et les moyens mis en œuvre. Ainsi, le manque de temps et de moyen (forte contrainte dans l'industrie), conduira à un programme inutilisable (car non prouvé), là où les méthodes concurrentes conduisent à des programmes « beugués ». De ce fait, l'utilisateur final ou le commanditaire peut avoir une grande confiance dans le programme. -Il utilise son propre langage formel. Au niveau de la spécification, il s'agit d'un langage logique basé sur une version simplifiée ad hoc de la théorie des ensembles. Ce choix est un peu arbitraire mais peut se justifier par les arguments suivants :  Il est important de pouvoir décrire des ensembles, des relations et des fonctions (ce sont les concepts centraux dans les modélisations objet),  La théorie des ensembles est bien établie dans la culture mathématique,  La théorie des ensembles permet de construire les objets mathématiques évolués (entiers, arbres, ...) à partir d'un ensemble réduit de composants de base,  La théorie des ensembles permet une écriture concise de notions évoluées. 3 2 Éléments du langage de la méthode B 2.1.1 Opérations arithmétiques : 2.1.2 Les ensembles 2.1.2.1 Construction d'ensemble 2.1.2.2 Composition d'ensembles 4 2.1.2.3 Autres constructions 2.1.3 Les formules 2.1.3.1 Formules de base e1 et e2 représentent des expressions quelconques (entiers, ensembles, paires ...), n1 et n2 sont des expressions qui représentent des entiers. 2.1.3.2 Formules ensemblistes Dans le tableau suivant, e représente une expression tandis que E, E1 et E2 représentent des ensembles. 2.1.3.3 Formules composées Dans le tableau suivant, F, F1 et F2 représentent des formules. 5 2.1.4 Relations et fonctions 2.1.4.1 A.4.1 Relations E, E1 et E2 représentent des ensembles tandis que R, R1 et R2 représentent des relations. Ensembles définis à partir de relations 6 2.1.4.2 Fonctions Image d'une fonction Si f est une fonction et e1 ∈ dom(f) alors f(e1) représente l'unique expression e2 telle que e1 ¿→ e2 ∈ f. Si E est un ensemble alors f(E) représente l'image de E par la relation f, c'est-à-dire l'ensemble des y pour lesquels il existe x tel que x ¿→ y ∈ f ou encore l'ensemble des f(x) pour x∈ E ∪ dom(f). 2.1.4.3 Séquences Dans le tableau suivant, s1 et s2 représentent des séquences, e, e1, ..., en des expressions quelconques. 7 3 Historique de B : Le langage B a été conçu par J.R.Abrial, qui était un des principaux concepteurs de Z dans les années 1980, avec le concours de G. Laffitte, F. Mejia et I. Mc Neal. Il est fondé sur les travaux scientifiques de E.W. Dijkstra, C.A.R. Hoare, C.B. Jones, C. Morgan, He Jifeng (du Programming Research Group Université d'Oxford). B s'inscrit dans une longue filiation de recherches fondamentales :  1949 Alan M. Turing, Checking a large routine, Cambridge University  1967 Robert Floyd, Assigning meanings to programs, AMS  1969 C.A.R. Hoare, An axiomatic basis for computer programming, CACM  1972 D.L. Parnas, A Technique for Software Module Specification with Examples, CACM  1975 Edsger Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, CACM  1981 David Gries, The Science of Programming, Springer, 1981  1986 Roland Backhouse, Program Construction and Verification, Prentice-Hall, 1986  1986 Cliff B. Jones, Systematic Software Development using VDM, Prentice-Hall  1988 C.A.R. Hoare, Jifeng He, Natural transformations and data refinement, PRG, Oxford  1990 C. Morgan, Programming from Specifications, Prentice-Hall  1996 J.R. Abrial, , Cambridge University Press La première conférence sur le B a eu lieu en France à Nantes les 25,26,27 novembre en 1996. La méthode B a été utilisé avec succès pour plusieurs applications industrielles. On peut citer le développement du logiciel embarqué pour la ligne 14 du métro parisien (METEOR) qui a été modélisé, prouvé et généré à partir de spécifications formelles B. En 2005, la RATP décide d'automatiser la ligne 1 et fait de nouveau appel à la méthode B pour le logiciel embarqué. Depuis 1995, de nombreux pilotes automatiques de métros ont été développés, notamment Barcelone, Delhi, Lausanne, Madrid, New York, Pékin (à l'occasion des Jeux Olympiques), Séoul ou encore Singapour. Le pilote automatique de canton de la navette de l'aéroport Charles de Gaulle fait partie des développements B. Enfin plusieurs métros en cours de développement ou de rénovation font appel à la méthode B pour le développement de logiciels embarqués : Istanbul, Le Caire, Milan, Sao Paulo, Shangai ou encore Toronto. En 1996, J.R. Abrial publie l'ouvrage The B-Book, Assigning programs to meanings. Il publie en 2010 un autre ouvrage sur le B événementiel : Modeling in Event-B, Hardback. UTILISATEURS DE LA MÉTHODE B : LES uploads/s3/ final-macsi.pdf