| Titre : |
Techniques industrielles de modélisation formelle pour le transport |
| Type de document : |
texte imprimé |
| Auteurs : |
Boulanger, Jean-Louis, Directeur de publication |
| Editeur : |
Paris : Hermes Science Publications |
| Année de publication : |
2011 |
| Autre Editeur : |
Paris : Hermes Science Publications |
| Collection : |
Recherche, technologie, applications |
| Sous-collection : |
Informatique et systèmes d'information |
| Importance : |
351 p. |
| Présentation : |
ill. |
| Format : |
24 cm |
| ISBN/ISSN/EAN : |
978-2-7462-3230-3 |
| Note générale : |
Bibliogr. en fin de chapitres. - Notes bibliogr. - Glossaire. - Index |
| Langues : |
Français (fre) |
| Mots-clés : |
B (méthode formelle)
Méthodes formelles(informatique) -- Applications industrielles
Transports ferroviaires -- Automatisation
Chemins de fer -- Dispositifs de sécurité
Systèmes de transport intelligent |
| Index. décimale : |
004.4 Logiciel. Programme |
| Résumé : |
Les techniques formelles réalisent des modèles de spécifications et/ou de conception et servent à 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 mise en œuvre des logiciels au sein d'un équipement, la RATP a mis en œuvre les techniques formelles afin de démontrer que des impératifs de sécurité sont respectées par le logiciel. Cet ouvrage présente des exemples concrets de mise en œuvre 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 (ligne classique, TGV, ERTMS, fret) |
| Note de contenu : |
Au sommaire :
1. Une approche innovante et une aventure humaine au service de la sécurité ferroviaire.
2. SAET-METEOR.
3. Preuve de propriétés globales à l'aide de l'outil de preuve SIMULINK DESIGN VERIFIER.
4. Démonstration de la sécurité d'une application ferroviaire de signalisation en mode nominal et en modes dégradés.
5. Utilisation de la preuve formelle dans le CBTC (OCTYS).
6. Validation d'automatismes ferroviaires de sécurité à base de réseaux de Petri.
7. ERTMS Formal Specs : un langage dédié pour la formalisation des spécifications pour le développement d'unité bord ERTMS.
8. Synthèse et conclusions. |
Techniques industrielles de modélisation formelle pour le transport [texte imprimé] / Boulanger, Jean-Louis, Directeur de publication . - Paris : Hermes Science Publications : Paris : Hermes Science Publications, 2011 . - 351 p. : ill. ; 24 cm. - ( Recherche, technologie, applications. Informatique et systèmes d'information) . ISBN : 978-2-7462-3230-3 Bibliogr. en fin de chapitres. - Notes bibliogr. - Glossaire. - Index Langues : Français ( fre)
| Mots-clés : |
B (méthode formelle)
Méthodes formelles(informatique) -- Applications industrielles
Transports ferroviaires -- Automatisation
Chemins de fer -- Dispositifs de sécurité
Systèmes de transport intelligent |
| Index. décimale : |
004.4 Logiciel. Programme |
| Résumé : |
Les techniques formelles réalisent des modèles de spécifications et/ou de conception et servent à 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 mise en œuvre des logiciels au sein d'un équipement, la RATP a mis en œuvre les techniques formelles afin de démontrer que des impératifs de sécurité sont respectées par le logiciel. Cet ouvrage présente des exemples concrets de mise en œuvre 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 (ligne classique, TGV, ERTMS, fret) |
| Note de contenu : |
Au sommaire :
1. Une approche innovante et une aventure humaine au service de la sécurité ferroviaire.
2. SAET-METEOR.
3. Preuve de propriétés globales à l'aide de l'outil de preuve SIMULINK DESIGN VERIFIER.
4. Démonstration de la sécurité d'une application ferroviaire de signalisation en mode nominal et en modes dégradés.
5. Utilisation de la preuve formelle dans le CBTC (OCTYS).
6. Validation d'automatismes ferroviaires de sécurité à base de réseaux de Petri.
7. ERTMS Formal Specs : un langage dédié pour la formalisation des spécifications pour le développement d'unité bord ERTMS.
8. Synthèse et conclusions. |
|  |
Techniques industrielles de modélisation formelle pour le transport (2011)
