Mise en oeuvre de la méthode B

Résumé

Présentation d'un modèle, la méthode B, pour analyser et vérifier le comportement d'un logiciel. Cette méthode formelle s'appuie sur la preuve de propriétés qui, sur la base d'une spécification et de la notion de raffinement, permet d'aller jusqu'à la production automatique de code. Avec des exemples en avionique et systèmes manufacturiers.

Contributeur(s)
- Boulanger, Jean-Louis (1966-....). Éditeur scientifique
Éditeur(s)
- Hermès science publications
- Lavoisier
Date
- DL 2013
Langues
- Français
Description matérielle
- 1 vol. (420 p.) : ill. ; 24 cm
Collections
- Informatique et systèmes d'information
Sujet(s)
ISBN
- 978-2-7462-3810-7
Indice
- 681.2 Programmation (généralités)
Quatrième de couverture
- Informatique et Systèmes d'Information
  La mise en place d'un logiciel sans défaut reste primordiale pour plusieurs domaines qui requièrent des applications dites de sécurité comme les transports. La réalisation d'un modèle formel est l'approche la plus efficace pour atteindre l'objectif du zéro défaut, que ce soit en termes de temps ou de maîtrise de la complexité. Ce modèle permet d'analyser et de vérifier le comportement d'un logiciel.
  Cet ouvrage présente la méthode B, une méthode formelle s'appuyant sur la preuve de propriétés qui, sur la base d'une spécification et de la notion de raffinement, permet d'aller jusqu'à la production automatique de code.
  Différents outils découlant de cette méthode ainsi que des exemples concrets d'utilisations industrielles de différentes tailles sont aussi exposés dans des domaines tels que l'avionique ou les systèmes manufacturiers.
Tables des matières
- - Mise en oeuvre de la méthode B
  - Jean-Louis Boulanger
  - Hermes Science
  - Lavoisier
  - Introduction13
  - Jean-Louis Boulanger
  - Chapitre 1. Présentation de la méthode B19
  - Jean-Louis Boulanger
  - 1.1. Introduction19
  - 1.2. La méthode B21
  - 1.2.1. La notion de machine abstraite22
  - 1.2.2. Des machines aux implémentations30
  - 1.3. Vérification et validation34
  - 1.3.1. Vérification interne34
  - 1.4. Méthodologie39
  - 1.4.1. Développement en couche39
  - 1.4.2. Rôle de la décomposition dans la composition des OPs41
  - 1.4.3. Cycle de développement d'un projet B41
  - 1.5. Retour d'expérience44
  - 1.5.1. Quelques chiffres44
  - 1.5.2. Quelques utilisations44
  - 1.6. Conclusion48
  - 1.7. Bibliographie49
  - Chapitre 2. L'Atelier B53
  - Thierry Lecomte
  - 2.1. Introduction53
  - 2.2. Le raffinement automatique55
  - 2.3. La génération de code57
  - 2.4. La preuve et l'animation de modèle60
  - 2.5. Mouvement vers l'open-source61
  - 2.6. Bibliographie62
  - Chapitre 3. Outils B65
  - Jean-Louis Boulanger
  - 3.1. Introduction65
  - 3.2. Principes généraux66
  - 3.3. L'Atelier B67
  - 3.3.1. Gestion de projet67
  - 3.3.2. Vérification du typage et génération des OP69
  - 3.3.3. Génération de code70
  - 3.3.4. Prouveur72
  - 3.3.5. Qualification des outils74
  - 3.4. Les outils open source75
  - 3.4.1. Présentation75
  - 3.4.2. ABTools76
  - 3.5. Conclusion96
  - 3.6. Bibliographie96
  - Chapitre 4. La méthode B à Siemens99
  - Daniel Dolle
  - 4.1. Introduction99
  - 4.1.1. Siemens Industry Mobility99
  - 4.1.2. Le système CBTC101
  - 4.1.3. Quelques caractéristiques des logiciels B103
  - 4.1.4. Le calculateur cible104
  - 4.2. Processus de développement avec B105
  - 4.2.1. Développement105
  - 4.2.2. Spécification informelle106
  - 4.2.3. Formalisation de la spécification107
  - 4.2.4. Raffinement et codage111
  - 4.2.5. Preuve116
  - 4.3. Activité de contrôle118
  - 4.3.1. Revue de développement118
  - 4.3.2. Activité de test120
  - 4.3.3. Activité de validation sécuritaire120
  - 4.4. Sous la dalle de marbre123
  - 4.4.1. Traduction B vers Ada123
  - 4.4.2. Modèle abstrait - modèle concret : quelques nuances125
  - 4.4.3. Calcul fonctionnel avec contrôle sécuritaire126
  - 4.4.4. Configuration129
  - 4.4.5. Limitations131
  - 4.5. Raffinement automatique132
  - 4.5.1. Historique132
  - 4.5.2. Principes de fonctionnement133
  - 4.5.3. Raffinement interactif135
  - 4.6. Conclusion136
  - 4.7. Bibliographie138
  - Chapitre 5. Applications industrielles de la modélisation avec la méthode B139
  - Thierry Lecomte
  - 5.1. Introduction139
  - 5.2. Les systèmes de contrôle-commande pour le pilotage de portes palières142
  - 5.3. La sécurité des composants micro-électroniques152
  - 5.4. Conclusion158
  - 5.5. Bibliographie158
  - Chapitre 6. Vérification formelle de données pour les systèmes paramétrables161
  - Mathieu Clabaut
  - 6.1. Introduction161
  - 6.1.1. Systerel161
  - 6.1.2. Vérification des données162
  - 6.1.3. Systèmes paramétrés163
  - 6.2. Les données dans le cycle de développement164
  - 6.2.1. Identification des données et de leurs propriétés165
  - 6.2.2. Modélisation165
  - 6.2.3. Validation des propriétés165
  - 6.2.4. Production des données166
  - 6.2.5. Vérification des propriétés sur les données166
  - 6.2.6. Intégration des données166
  - 6.3. Vérification des données167
  - 6.3.1. Vérification manuelle168
  - 6.3.2. Vérification algorithmique168
  - 6.3.3. Vérification formelle169
  - 6.4. Exemple de mise en oeuvre176
  - 6.4.1. Présentation176
  - 6.4.2. Modélisation des propriétés176
  - 6.4.3. Extraction de données179
  - 6.4.4. Outillage179
  - 6.5. Processus SSIL4180
  - 6.6. Conclusion180
  - 6.7. Bibliographie180
  - Chapitre 7. BCARe : contrôle automatique des règles ajoutées à Siemens SAS IC MOL181
  - Karim Berkani, Mélanie Jacquel, Eric Le Lay
  - 7.1. Résumé181
  - 7.2. Introduction181
  - 7.3. Description du processus de validation des règles ajoutées183
  - 7.3.1. Activité de preuve184
  - 7.3.2. Règles184
  - 7.3.3. Validation d'une règle186
  - 7.4. Outils de validation BCARe188
  - 7.4.1. BCARe : un environnement pour la validation de règle188
  - 7.4.2. Check_blvar189
  - 7.4.3. Chaine_verif197
  - 7.5. Preuve des lemmes de validation BCARe203
  - 7.5.1. Preuve automatique avec L_tac204
  - 7.5.2. Evaluation et tests210
  - 7.6. Conclusion212
  - 7.7. Bibliographie213
  - Chapitre 8. B-RAIL : d'UML à B pour la modélisation d'un passage à niveau215
  - Jean-Louis Boulanger
  - 8.1. Introduction215
  - 8.2. Première idée de la problématique216
  - 8.3. Gestion des exigences217
  - 8.3.1. Exigences217
  - 8.3.2. Recommandation, exigence et propriété219
  - 8.3.3. Ingénierie des exigences222
  - 8.4. Présentation de la notation UML et de la méthode B230
  - 8.4.1. La notion UML230
  - 8.4.2. La méthode B233
  - 8.4.3. Bilan234
  - 8.5. Etape 1 : acquisition du besoin234
  - 8.5.1. Extraction des exigences234
  - 8.5.2. Identification des risques237
  - 8.5.3. Identification du service rendu238
  - 8.6. Etape 2 : environnement et analyse des risques241
  - 8.6.1. Identification de l'environnement241
  - 8.6.2. Description de l'univers244
  - 8.6.3. Défaillance de l'environnement246
  - 8.6.4. Maintenance251
  - 8.6.5. Impact de l'environnement sur le système251
  - 8.6.6. Bilan256
  - 8.7. Etape 3 : décomposition en composants255
  - 8.7.1. Sélection des exigences255
  - 8.7.2. Architecture256
  - 8.7.3. Comportement257
  - 8.8. Etape 4 : vérification259
  - 8.8.1. Introduction259
  - 8.8.2. Description des modèles formels261
  - 8.9. UML2B261
  - 8.10. Conclusion262
  - 8.11. Bibliographie263
  - Chapitre 9. Event B267
  - Dominique Mery, Neeraj Kumar Singh
  - 9.1. Présentation267
  - 9.2. Structure de ce chapitre268
  - 9.3. Modélisation et vérification d'un système268
  - 9.3.1. Modélisation268
  - 9.3.2. Propriétés de sûreté271
  - 9.4. Event B : un langage de modélisation274
  - 9.4.1. Eléments de base d'un modèle Event B275
  - 9.4.2. Propriétés d'invariance en Event B277
  - 9.4.3. Raffinement des événements278
  - 9.4.4. Structures des machines et des contextes en Event B280
  - 9.5. Développement d'un algorithme séquentiel283
  - 9.5.1. Construction d'un algorithme de calcul de la somme par raffinement et transformation de modèles en algorithme283
  - 9.5.2. Développement d'un algorithme séquentiel avec le patron de développement appel-événement293
  - 9.6. Développement d'un algorithme réparti300
  - 9.6.1. Modélisation des algorithmes répartis300
  - 9.6.2. Eléments du patron de développement302
  - 9.7. Outils307
  - 9.7.1. Atelier B307
  - 9.7.2. La plateforme Rodin307
  - 9.8. Conclusion et perspective308
  - 9.8.1. Applications à des cas d'études308
  - 9.8.2. Conclusion et perspectives309
  - 9.9. Bibliographie309
  - Chapitre 10. B étendu aux flottants : est-ce suffisant pour prouver un logiciel avionique ?315
  - Jean-Louis Dufour
  - 10.1. Introduction315
  - 10.2. Motivation315
  - 10.3. Les entiers et les origines ferroviaires de la méthode B317
  - 10.3.1. Le projet SACEM317
  - 10.3.2. Le besoin d'une méthode logicielle en rupture317
  - 10.3.3. Le processeur codé et les entiers318
  - 10.3.4. Les limites de la logique de Hoare et la naissance du B319
  - 10.3.5. Le tableau de chasse du B, et encore les entiers !320
  - 10.3.6. L'influence bénéfique du fail-safe sur la complexité320
  - 10.4. Le contexte avionique : les flottants et la complexité321
  - 10.5. Une fausse bonne idée : la séparation entre calculs entiers et flottants323
  - 10.6. Les flottants IEEE 754325
  - 10.6.1. Périmètre du standard325
  - 10.6.2. Les flottants ont un comportement complexe327
  - 10.6.3. Les infinis et les « non-nombre »328
  - 10.7. Philosophie de l'extension aux flottants329
  - 10.7.1. Vision globale329
  - 10.7.2. Les nombres réels330
  - 10.7.3. Les flottants concrets331
  - 10.7.4. Les flottants abstraits332
  - 10.8. Retour sur les propriétés intéressantes à prouver333
  - 10.8.1. Les spécifications avioniques sont complexes334
  - 10.8.2. Peut-on abstraire les données vectorielles ?335
  - 10.8.3. L'écart entre spécifications algorithmiques et pré-conditions des procédures feuille335
  - 10.8.4. Les intégrateurs et la formalisation des bornes système336
  - 10.9. Conclusion337
  - 10.10. Annexe : la confusion entre débordement, infini et paramètre illégal338
  - 10.10.1. Présentation de la problématique338
  - 10.10.2. La confusion entre débordement et infini338
  - 10.10.3. La confusion entre infini et paramètre illégal341
  - 10.11. Bibliographie342
  - Chapitre 11. Usage pragmatique du B : la puissance du formel sans ses lourdeurs345
  - Christophe Metayer, François Bustany et Mathieu Clabaut
  - 11.1. Introduction345
  - 11.2. Maquetter un modèle formel : dans quel but ?345
  - 11.3. Tendre vers une approche inspirée des méthodes agiles ?347
  - 11.4. Lancer les activités de validation simultanément à celles du développement347
  - 11.5. Quelles performances pour un logiciel développé en B ?348
  - 11.6. Recours à l'infini : découplage entre réflexion algorithmique et problématique de programmation351
  - 11.7. Mise en oeuvre industrielle du B événementiel354
  - 11.8. B logiciel et B événementiel356
  - 11.9. Conclusion357
  - 11.10. Bibliographie357
  - Chapitre 12. Brillant/BCaml : une plateforme d'outils libres pour la méthode B359
  - Samuel Colin, Dorian Petit
  - 12.1. Qu'est-ce que Brillant/BCaml ?359
  - 12.2. Organisation360
  - 12.3. Fonctionnalités362
  - 12.3.1. Le noyau historique362
  - 12.3.2. Manipulations de code364
  - 12.3.3. Preuve de spécifications B364
  - 12.4. Perspectives365
  - 12.5. Bibliographie366
  - Chapitre 13. Faisabilité de l'utilisation des méthodes formelles pour les systèmes manufacturiers369
  - Pascal Lamy, Philippe Charpentier, Jean-François Petin, Dominique Evrot
  - 13.1. Introduction369
  - 13.2. Présentation du besoin370
  - 13.3. Les méthodes choisies et leur description sommaire372
  - 13.3.1. La méthode B372
  - 13.3.2. Spécification avec SysML et vérification formelle par model-checking373
  - 13.4. Description de la machine : la presse mécanique à embrayage-frein375
  - 13.4.1. Description de la presse375
  - 13.4.2. Description sommaire des modes de fonctionnement377
  - 13.4.3. Description sommaire des moyens de protection378
  - 13.4.4. Particularités de l'automate378
  - 13.5. Démarche suivie pour la conception, la validation et la génération du logiciel à l'aide de la méthode B378
  - 13.5.1. Rédaction d'un cahier des charges compatible B378
  - 13.5.2. Modèle B : spécification et conception381
  - 13.5.3. Génération d'un code C et simulation384
  - 13.5.4. Génération du code pour l'automate et validation384
  - 13.5.5. Bilan de l'utilisation de la méthode B387
  - 13.6. Formalisation des exigences et propriétés à l'aide de SysML et vérification de modules unitaires par model-checker388
  - 13.6.1. Vue d'ensemble du processus de conception pour les systèmes manufacturiers388
  - 13.6.2. Modélisation des exigences390
  - 13.6.3. Modélisation des architectures fonctionnelles et organiques394
  - 13.6.4. Traçabilité des exigences397
  - 13.6.5. Développement et vérification des composants logiciels de commande399
  - 13.6.6. Discussion402
  - 13.7. Conclusion sur l'utilisation des techniques formelles dans le domaine manufacturier404
  - 13.8. Bibliographie405
  - Conclusion407
  - Glossaire413
  - Index417
Origine de la notice:
- Electre