Techniques industrielles de modélisation formelle pour le transport

Résumé

Présentation d'exemples concrets de mise en oeuvre des techniques formelles (simulation, model checking, preuve) et des méthodes formelles (méthode B, SCADE) sur des projets de transport ferroviaire de type métro et grande ligne. Les techniques formelles servent à l'analyse statique de code, à la démonstration du respect de propriété et à la bonne gestion des calculs sur les flottants.

Contributeur(s)
- Boulanger, Jean-Louis (1966-....). Directeur de publication/coordinateur/coordonnateur
Éditeur(s)
- Hermès science publications-Lavoisier
Date
- impr. 2011
Notes
- Notes bibliogr. Glossaire. Index
Langues
- Français
Description matérielle
- 1 vol. (351 p.) : ill. ; 24 cm
Collections
- Informatique et systèmes d'information
Sujet(s)
ISBN
- 978-2-7462-3230-3
Indice
- 629 Transports
Quatrième de couverture
- Informatique et Systèmes d'Information
  Les techniques formelles réalisent des modèles de spécifications et/ou de conception servant à l'analyse statique de code, à la démonstration du respect de propriété, à la bonne gestion des calculs sur les flottants, etc.
  Dès la première introduction des logiciels au sein d'un équipement, la RATP a mis en oeuvre les techniques formelles afin de démontrer que des impératifs de sécurité sont respectés par le logiciel.
  Cet ouvrage présente des exemples concrets de mise en oeuvre des techniques (simulation, model-checking, preuve) et des méthodes formelles (méthode B, SCADE) sur des projets de transport ferroviaire de type métro et grande-ligne (ligne classique, TGV, ERTMS ou fret).
Tables des matières
- - Techniques industrielles de modélisation formelle pour le transport
  - Jean-Louis Boulanger
  - Hermes Science
  - Lavoisier
  - Introduction15
  - Jean-Louis Boulanger
  - Chapitre 1. Une approche innovante et une aventure humaine au service de la sécurité ferroviaire21
  - Sylvain Fioroni
  - 1.1. Introduction21
  - 1.2. OCTYS - Open Control of Train Interchangeable and Integrated System23
  - 1.3. PMI - Poste de manoeuvre informatisé26
  - 1.4. Conclusion28
  - 1.5. Bibliographie28
  - Chapitre 2. SAET-METEOR31
  - Jean-Louis Boulanger
  - 2.1. Introduction31
  - 2.2. Présentation du SAET-METEOR32
  - 2.2.1. Décomposition du SAET-METEOR33
  - 2.2.2. Fonctions anticollision37
  - 2.2.3. Restrictions39
  - 2.3. Processus de réalisation de l'industriel39
  - 2.3.1. Contexte historique39
  - 2.3.2. Aspect matériel40
  - 2.3.3. Aspect logiciel43
  - 2.3.3.1. La méthode B43
  - 2.3.3.2. Processus de développement basé sur la méthode B47
  - 2.3.3.3. Application générique et application spécifique48
  - 2.3.3.4. Génération des données51
  - 2.3.4. Bilan des processus54
  - 2.4. Processus de vérification et de validation mis en place par la RATP55
  - 2.4.1. Cadre55
  - 2.4.2. Méthodologie RATP55
  - 2.4.3. Vérification réalisée par la RATP56
  - 2.4.3.1. Contexte56
  - 2.4.3.2. Dossier de principe59
  - 2.4.3.3. Modélisation61
  - 2.4.3.4. Architecture du modèle67
  - 2.4.3.5. Technique de vérification des modèles73
  - 2.4.3.6. Limite de la vérification par simulation77
  - 2.4.3.7. Validation du modèle78
  - 2.4.3.8. Bilan de la modélisation80
  - 2.4.4. Validation80
  - 2.4.4.1. Contexte80
  - 2.4.4.2. Validation des logiciels génériques81
  - 2.4.4.3. Validation des données84
  - 2.4.5. Bilan de l'activité RATP90
  - 2.5. Bilan de l'approche globale91
  - 2.6. Conclusion92
  - 2.7. Annexe94
  - 2.8. Bibliographie99
  - Chapitre 3. Preuve de propriétés globales à l'aide de l'outil de preuve Simulink Design Verifier103
  - Véronique Delebarre, Jean-Frédéric Etienne
  - 3.1. Introduction103
  - 3.2. Méthode de vérification ou de preuve104
  - 3.2.1. Vérification de modèle107
  - 3.2.1.1. Intérêt et positionnement des méthodes de vérification de modèle en regard du cycle de développement107
  - 3.2.1.2. Classes de propriétés cible109
  - 3.2.2. Méthodes formelles et preuve de correction109
  - 3.2.2.1. Preuve automatisée110
  - 3.2.2.2. Réécriture111
  - 3.2.2.3. Description formelle et méthodes de raffinement112
  - 3.2.3. Couplage entre modèles et outils de preuve113
  - 3.3. Mise en oeuvre de l'outil Simulink Design Verifier115
  - 3.3.1. Rappels sur l'environnement de modélisation et de vérification MATLAB115
  - 3.3.1.1. Simulink/Embedded Matlab115
  - 3.3.1.2. Simulink Design Verifier116
  - 3.3.2. Cas d'étude122
  - 3.3.3. Modélisation125
  - 3.3.3.1. Représentation des données126
  - 3.3.3.2. Opérateurs du modèle128
  - 3.3.3.3. Modélisation de l'environnement129
  - 3.3.3.4. Modélisation des propriétés129
  - 3.3.4. Modélisation131
  - 3.4. Retour d'expérience et aspects méthodologiques132
  - 3.4.1. Règles de modélisation et contrôle de convergence132
  - 3.4.2. Phase de preuve unitaire133
  - 3.4.3. Preuve de propriétés globales135
  - 3.4.3.1. Décomposition des propriétés en sous lemmes135
  - 3.4.3.2. Preuves par induction136
  - 3.4.3.3. Autres techniques supplémentaires137
  - 3.4.3.4. Modification du modèle137
  - 3.4.4. Mise en évidence de contre-exemples138
  - 3.5. Bilan de l'expérimentation et conclusions138
  - 3.5.1. Modèle SIMULINK138
  - 3.5.2. Preuves réalisées139
  - 3.5.3. Démarche incrémentale de vérification139
  - 3.6. Apports de la méthodologie en regard du référentiel normatif EN50128140
  - 3.7. Bibliographie142
  - Chapitre 4. Démonstration de la sécurité d'une application ferroviaire de signalisation en mode nominal et en modes dégradés par la preuve formelle145
  - Jean-Marc Mota, Evguenia Dmitrieva, Amel Mammar, Paul Caspi, Salimeh Behnia, Nicolas Breton, Pascal Raymond
  - 4.1. Rappel du contexte145
  - 4.1.1. Introduction145
  - 4.1.2. Contexte147
  - 4.2. Description du cas d'application et de son périmètre148
  - 4.2.1. Architecture fonctionnelle du système PMI149
  - 4.2.2. Sous-système MEI150
  - 4.2.3. Vérification du logiciel MEI avec et sans preuve152
  - 4.2.4. Périmètre de la vérification154
  - 4.3. Modélisation du système complet155
  - 4.3.1. Modèle de l'application155
  - 4.3.2. Propriétés de sécurité157
  - 4.3.2.1. Arbres de scénarios : raffinement des événements redoutés157
  - 4.3.2.2. Arbres de défaillance158
  - 4.3.2.3. Modélisation générique à base d'automate159
  - 4.3.3. Modèle de l'environnement160
  - 4.3.3.1. Généralités160
  - 4.3.3.2. Temps logique des réactions161
  - 4.3.3.3. Modèle de l'environnement162
  - 4.3.3.4. Modélisation de la causalité : le jeu parallèle163
  - 4.3.3.5. Exemple d'expression d'hypothèse164
  - 4.3.3.6. Modélisation guidée par les contre-exemples165
  - 4.3.3.7. Démonstration des propriétés de sécurité168
  - 4.4. Atelier de preuve formelle169
  - 4.4.1. Modélisation du système170
  - 4.4.2. Chaîne d'analyse non certifiée170
  - 4.4.3. Chaîne d'analyse certifiée171
  - 4.4.4. Moteur d'analyses certifiables174
  - 4.4.5. Qualification de l'atelier de preuve175
  - 4.5. Cas d'application176
  - 4.6. Retour d'expérience179
  - 4.6.1. Modélisation de l'environnement180
  - 4.6.2. Preuve versus test181
  - 4.6.3. Limites182
  - 4.7. Conclusion et perspectives183
  - 4.8. Bibliographie184
  - Chapitre 5. Utilisation de la preuve formelle dans le CBTC (OCTYS)187
  - Christophe Tremblin, Pierre Lesoille, Omar Rezzoug
  - 5.1. Introduction187
  - 5.2. Présentation CBTC OCTYS188
  - 5.2.1. OCTYS188
  - 5.2.2. Mission du CBTC189
  - 5.2.3. Architectures du CBTC190
  - 5.3. L'équipement contrôleur de zone192
  - 5.3.1. Présentation192
  - 5.3.2. Modèle SCADE193
  - 5.3.2.1. Le modèle générique193
  - 5.3.2.2. Le modèle instancié195
  - 5.4. Historique de la mise en place de la solution196
  - 5.5. Solution technique et mise en oeuvre198
  - 5.5.1. Rédaction des propriétés198
  - 5.5.2. Deux principes de base de rédaction d'une propriété200
  - 5.5.2.1. Objectif : garantir d'abord la sécurité200
  - 5.5.2.2. Rester modulaire201
  - 5.5.3. Topologies de test202
  - 5.5.4. Premières analyses202
  - 5.5.4.1. Taille du modèle à analyser203
  - 5.5.4.2. Gestion de l'environnement204
  - 5.5.5. Processus de traitement d'une propriété206
  - 5.5.5.1. Analyse d'une contre-exemple208
  - 5.5.5.2. Analyse d'un contre-exemple d'induction210
  - 5.5.5.3. Partition de la propriété212
  - 5.5.6. Non régression213
  - 5.6. Résultats215
  - 5.7. Pistes d'améliorations216
  - 5.8. Conclusion216
  - 5.9. Bibliographie217
  - Chapitre 6. Validation d'automatismes ferroviaires de sécurité à base de réseaux de Petri219
  - Marc Antoni
  - 6.1. Introduction219
  - 6.1.1. Note au lecteur219
  - 6.1.2. Résumé219
  - 6.2. Problématique221
  - 6.2.1. Introduction221
  - 6.2.2. Un contexte métier, le ferroviaire221
  - 6.2.3. Déterminisme versus probabilisme pour une gestion sûre des systèmes informatiques critiques223
  - 6.2.3.1. De la constitution du système réel223
  - 6.2.3.2. Du déterminisme224
  - 6.2.3.3. Du probabilisme230
  - 6.2.3.4. De l'inter relation233
  - 6.2.3.5. Des couches système234
  - 6.2.3.6. Des trois niveaux de système critique235
  - 6.2.3.7. Du système de base237
  - 6.2.3.8. Du système déterministe238
  - 6.2.3.9. De la maîtrise de la pérennité d'un système240
  - 6.2.4. Un axe majeur : la validation formelle243
  - 6.3. Sécurité ferroviaire : notions fondamentales243
  - 6.3.1. De la maîtrise de propriétés de sécurité et des postulats244
  - 6.3.1.1. La signalisation244
  - 6.3.1.2. Le système ferroviaire246
  - 6.3.2. Aspects à considérer en vue de réaliser une validation formelle250
  - 6.3.2.1. Indépendances et indépendances faibles250
  - 6.3.2.2. Postulats de fonctionnement251
  - 6.3.2.3. Propriétés de sécurité et incompatibilités252
  - 6.3.2.4. Propriétés de non surabondance252
  - 6.3.2.5. Synthèse253
  - 6.4. Méthode de validation formelle des systèmes informatiques critiques255
  - 6.4.1. Le module d'enclenchement des postes modernes255
  - 6.4.1.1. Principes de conception du module d'enclenchement255
  - 6.4.1.2. Conséquences pour la preuve257
  - 6.4.2. Langage de spécification AEFD258
  - 6.4.2.1. Un langage de spécification interprétable258
  - 6.4.2.2. Graphe et transitions260
  - 6.4.2.3. Règles d'écriture264
  - 6.4.2.4. Etats accessibles et combinatoire265
  - 6.4.3. Méthode de preuve par assertions266
  - 6.4.3.1. Principe266
  - 6.4.3.2. Automatisation de la preuve269
  - 6.4.3.3. Outillage pour la réalisation de la preuve275
  - 6.5. Applications à un poste réel277
  - 6.5.1. Introduction277
  - 6.5.2. Présentation du plan de voie et du programme du poste277
  - 6.5.3. Propriétés de sécurité et postulats278
  - 6.5.4. Exploration et validation formelle du fonctionnel applicatif du poste278
  - 6.6. Conclusion282
  - 6.6.1. D'un point de vue général282
  - 6.6.2. De l'usage de la méthode283
  - 6.6.3. D'un point de vue universitaire285
  - 6.6.4. Du point de vue de l'industrie ferroviaire286
  - 6.6.5. Du modèle et de l'implémentation287
  - 6.7. Bibliographie288
  - Chapitre 7. ERTMS Formal Specs : un langage dédié pour la formalisation des spécifications pour le développement d'unité bord ERTMS291
  - Laurent Ferier, Stanislas Pinte, Darius Blasband, Svitlana Lukicheva
  - 7.1. Introduction291
  - 7.2. Contexte292
  - 7.2.1. ERTMS292
  - 7.2.2. Spécification ERTMS - TSI et subsets293
  - 7.2.3. Spécification ERTMS - TSI et subsets293
  - 7.2.4. Défis inhérents aux spécifications ERTMS294
  - 7.3. Description d'EFS295
  - 7.3.1. Caractéristiques295
  - 7.3.1.1. Traçabilité296
  - 7.3.1.2. Compréhensibilité297
  - 7.3.1.3. Raisonnement sur le modèle299
  - 7.3.1.4. Testabilité300
  - 7.3.1.5. Interopérabilité303
  - 7.3.2. Processus de modélisation303
  - 7.3.2.1. Création des tests304
  - 7.3.2.2. Données historiques304
  - 7.3.3. Implémentation ou génération de code305
  - 7.3.4. Effort de modélisation305
  - 7.4. Conclusion306
  - 7.5. Travail futur306
  - 7.6. Bibliographie307
  - Chapitre 8. Synthèse et conclusions309
  - Jean-Louis Boulanger
  - 8.1. Introduction309
  - 8.2. Les méthodes formelles et la norme EN 50128310
  - 8.2.1. Système E/E/EP310
  - 8.2.2. Domaine ferroviaire311
  - 8.2.3. Prise en compte des techniques et méthodes formelles313
  - 8.2.3.1. Définitions314
  - 8.2.3.2. Spécification des exigences du logiciel315
  - 8.2.3.3. Modèle323
  - 8.2.3.4. Architecture du logiciel325
  - 8.2.3.5. Conception du logiciel326
  - 8.2.3.6. Codage329
  - 8.2.3.7. Vérification et validation338
  - 8.3. Modélisation339
  - 8.4. Conclusion340
  - 8.5. Bibliographie340
  - Glossaire345
  - Index349
Origine de la notice:
- FR-751131015