Génération de scénarios de tests pour la vérification de systèmes répartis : application au système européen de signalisation ferroviaire (ERTMS), Generation of test scenarios for distributed system checking : application to the European Railway Traffic Management System (ERTMS)

Sana Jabri

Description

Sous la direction de El Miloudi El koursi, Pascal Yim
Thèse soutenue le 22 juin 2010: Ecole Centrale de Lille
Dans les années 90, la commission européenne a sollicité la mise au point d’un système de contrôle commande et de signalisation ferroviaire commun à tous les réseaux des états membres : le système ERTMS « European Railway Traffic Management System ». Il s’agit d’un système réparti complexe dont le déploiement complet est long et coûteux. L’objectif global consiste à diminuer les coûts de validation et de certification liés à la mise en œuvre de ce nouveau système en Europe. La problématique scientifique réside dans la modélisation formelle de la spécification afin de permettre la génération automatique des scénarios de test. Les verrous scientifiques, traités dans cette thèse, sont liés d’une part à la transformation de modèle semi-formel en modèle formel en préservant les propriétés structurelles et fonctionnelles des constituants réactifs du système réparti, et d’autre part à la couverture des tests générés automatiquement. Les constituants sont sous la forme de boîte noire. L’objectif consiste à tester ces derniers à travers la spécification ERTMS. Nous avons développé une approche de modélisation basée sur le couplage de modèles semi-formels (UML) et de modèles formels (Réseaux de Petri). Ce couplage se fait à travers une technique de transformation de modèles. Nous avons développé ensuite une méthode de génération automatique de scénarios de test de conformité à partir des modèles en réseaux de Petri. Les scénarios de test ont été considérés comme une séquence de franchissement filtrée puis réduite du réseau de Petri interprété représentant la spécification. Ces scénarios ont été exécutés sur notre plateforme de simulation ERTMS
-Système ERTMS
-Interopérabilité ferroviaire
-Modélisation objet UML
-Transformation de modèles
-Modélisation formelle
-Génération de scénarios de test
European Union set up a European rail traffic management system “ERTMS” to ensure, with high level of safety, train operation on different European networks. As the full deployment of this system is long and expensive, evolutions are necessary and raise other technological challenges. The goal is to determine how to use ERTMS specifications to produce test scenarios. This work presents methods, models and tools dedicated to the generation of test scenarios for the validation of ERTMS components based on functional requirements. The development of ERTMS system requires adequate methods for Modelling and evaluating its behavior. Evaluation and certification of the system can be done by generating test scenarios applying formal methods. The Unified Modelling Language (UML) is a widely accepted Modelling standard in industry. However, it is a semi-formal language and it does not allow verification of system behavior. In this case, formal models like Petri Net can be used. These methods are used in order to formalize ERTMS specification. Tests scenarios are generated on the basis of Petri net models. One scenario is considered like a firing sequence in the reachability graph of the Petri net. Then, test scenarios are applied on ERTMS platform simulator in order to check the components and to give test verdicts. Finally, the approach, developed in this document, has been applied to ERTMS components in order to demonstrate the validation and certification costs reduction and also to minimize the upgrade and retrofit constraints and validation cost
-ERTMS system
-Railway interoperability
-UML Object Modeling
-Model transformation
-Formal modeling
-Test scenarios generation
Source: http://www.theses.fr/2010ECLI0006/document

Sujets

• Interopérabilité ferroviaire

Informations

• Publié par: Thesee
• Nombre de lectures: 54
• Langue: Français
• Poids de l'ouvrage: 5 Mo

Extrait

ECOLE CENTRALE DE LILLE

N° d’ordre : 123

THESE

Présentée en vue d’obtenir le grade de


DOCTEUR

En

AUTOMATIQUE ET INFORMATIQUE INDUSTRIELLE

Par

Sana JABRI


DOCTORAT DELIVRE PAR L’ECOLE CENTRALE DE LILLE


Titre de la thèse :

GENERATION DE SCENARIOS DE TESTS POUR LA VERIFICATION DE SYSTEMES
REPARTIS : APPLICATION AU SYSTEME EUROPEEN DE SIGNALISATION
FERROVIAIRE (ERTMS)

Soutenue le 22 Juin 2010 devant le jury d’examen :


Président M. Armand TOGUYENI, Professeur à l’Ecole Centrale de Lille
Rapporteur M. Abderrafiâa KOUKAM, Professeur à l’Université de Technologie de Belfort-Montbéliard
M. Christos PYRGIDIS, Professeur à Aristotle University of Thessaloniki Rapporteur
Membre Mme. Nathalie DUQUENNE, « Project Officer in European Railway Agency »
Membre M. Alexandre GIRARDI, Chef du département certification à Multitel
Membre M. Thomas BOURDEAUD’HUY, Maître de conférences à l’Ecole Centrale de Lille
M. Etienne LEMAIRE, Ingénieur de recherche à l’INRETS Membre
Directeur de thèse M. El Miloudi EL KOURSI, Directeur d’Unité de recherche ESTAS à l’INRETS
Co-directeur de thèse M. Pascal YIM, Directeur Open Technologies


Thèse préparée dans les Laboratoires LAGIS de l’Ecole Centrale de Lille et ESTAS de l’INRETS
LAGIS., UMR 8146 – École Centrale de Lille
ESTAS, 20 Rue Elisée Reclus, INRETS
Ecole Doctorale SPI 072

tel-00584308, version 1 - 8 Apr 2011

tel-00584308, version 1 - 8 Apr 2011




AAAA mmmmoooonnnn ppppaaaappppaaaa aaaaddddoooorrrréééé
Tu es mon maître et mon idole. J’espère être à la hauteur de tout ce que tu m’apporte dans la
vie. Ton soutien sans faille et ta confiance en moi m’ont permis d’arriver là où je suis.


AAAA mmmmaaaa mmmmaaaammmmaaaannnn cccchhhhéééérrrriiiieeee
C’est grâce à ton amour, ton affection, ta protection et ton soutien que j’ai pu réussir et
surmonter les moments difficiles. Que ce travail soit la reconnaissance de tous tes sacrifices.


A mes sœurs et à mon petit frère
Vous êtes le rayon de soleil de ma vie. Je vous suis reconnaissante pour votre amour, votre
soutien, votre joie de vivre et surtout notre complicité.


A mes amies Meriem et Insaf
A mon ami David
Vous comptez énormément pour moi…


A toute ma famille & mes amis.







Ce qui se conçoit bien s’énonce clairement et les
mots pour le dire arrivent aisément
N.Boileau, L’Art poétique



tel-00584308, version 1 - 8 Apr 2011

tel-00584308, version 1 - 8 Apr 2011



Remerciements






Je tiens d’abord à remercier El Miloudi EL KOURSI de m’avoir accueillie au sein de l’équipe
de recherche ESTAS afin d’accomplir mes travaux de thèse, de m’avoir guidée dès les
premiers jours et de m’avoir soutenue dans les moments difficiles. Je le remercie vivement
pour ses conseils avisés et ses lectures attentives de mon mémoire.
J’adresse aussi un grand merci à Pascal YIM, qui a su m’orienter dans les bonnes directions.
J’exprime ma profonde reconnaissance à Thomas BOURDEAUD’HUY pour avoir dirigé mes
travaux de thèse, pour sa passion, ses conseils, pour m’avoir consacré une partie importante
de son temps et pour m’avoir aidée à améliorer mon travail. Il a su garder le cap lorsque
personnellement je doutais.
Je remercie tout particulièrement Etienne LEMAIRE, qui a dirigé mes travaux de thèse, m’a
fait découvrir le monde ferroviaire, m’a guidée depuis mon stage de Master jusqu’à la fin de
ma thèse, et m’a aidée à avancer dans chaque étape de mon travail. Je lui suis reconnaissante
pour toutes ses explications concernant le système ERTMS.
El Miloudi, Pascal, Thomas et Etienne, vous m’avez invitée à une grande aventure que vous
avez conduite d’une main de maître en instaurant un climat de confiance, de patience,
d’amitié et de bienveillance. Ce travail est aussi le vôtre.
***
Les travaux développés dans cette thèse ont été financés par une bourse INRETS et Région
Nord Pas de Calais. Je les remercie de m’avoir donné la chance de réaliser ma thèse dans de
très bonnes conditions. Je remercie également le groupe CISIT (Campus International on
Safety and Intermodality in Transportation) qui contribue à la prééminence de la région
dans le secteur des transports et dont l’INRETS est membre.


tel-00584308, version 1 - 8 Apr 2011Je remercie sincèrement mes rapporteurs : Messieurs Christos PYRGIDIS et Abderrafiâa
KOUKAM qui ont accepté de plancher sur ce travail. Ils ont su tirer sa qualité vers le haut à
travers leurs précieuses remarques.
Je remercie également les membres du Jury : M. Armand TOGUYENI, Mme. Nathalie
DUQUENNE et M. Alexandre GIRARDI d’avoir bien voulu participer à la soutenance.
***
Je remercie chaleureusement tous les membres de l’INRETS, permanents, doctorants et
stagiaires. J’ai toujours adoré notre ambiance « familiale » et les discussions très ouvertes sur
divers thèmes. Il m’est particulièrement agréable de remercier : mon amie Meriem pour son
soutien, ses encouragements et pour les belles années que nous avons passées ensemble à
ESTAS ; mon ami Olivier.L et sa famille (Chris, Orlane et Sélène) pour les bons moments que
j’ai partagés avec eux ; ma collègue Nathalie pour son aide et sa compréhension ; mes
collègues Philippe, Sonia, Georges, Greg, Isabelle, Olivier.D, Victor, Valérie, Latifa, Bernard,
Daniel, pour leur amitié et leur soutien ; enfin mes collègues doctorants Ahmed, François,
Nizar, Malik et Sabrine pour les joies et les peines que j’ai partagées avec eux.
***
Une pensée particulière va vers mes parents Rafika et Abdelhamid, ma sœur Asma et mon
frère Mohamed dont l’éloignement est très pesant mais tout aussi motivant. Leurs sacrifices
m’ont permis d’arriver là où je suis et leur fierté est un carburant infini d’avancement et de
dépassement de soi. Je vous remercie de votre affection et de votre soutien inconditionnel
dans mes choix de carrières. Vous me faites grandir chaque jour.
Je remercie particulièrement mon père pour ses lectures attentives de mon mémoire et ma
mère pour ses bons petits plats qui m’ont encouragée à finir ma rédaction.
Un grand merci à mes deux familles Boukahla et Jabri d’avoir cru en moi. Je remercie en
particulier ma tante Bchira pour son amour, ses encouragements et ses bons gâteaux ; ma
tante Rawda, mes oncles Samir et Mustapha pour leur soutien et leur confiance en moi ; ma
tante Souad et mon oncle Mohamed pour tout leur support pendant mes années d’études
primaires et secondaires ; mes cousines et mes grands-mères pour tout leur amour.
***
J’exprime ma profonde gratitude envers ma deuxième famille en France : Ghislaine, Nadine,
Delphine et Fabien.L, Léonard ; Delphine et David.N, Mathilde, Maelle ; Martine et Jacques
pour leur accueil, leurs encouragements et tous les bons moments que nous avons partagés
ensemble lors d’une sortie ou autour d’un bon repas.
tel-00584308, version 1 - 8 Apr 2011***
Je remercie sincèrement mon amie Insaf qui m’a soutenue durant mes années de thèse, m’a
toujours encouragée et m’a rendue confiance en moi dans les moments difficiles. Je
m’adresse aussi à mes amis de longue date (Mariem.D, Randa.M, Anis.F) pour les remercier
de leur soutien. Je remercie enfin mes amis en France qui grâce à eux je me suis toujours
sentie en famille (Aymen, Benoit, Mélanie, Maxime, Agnès, Maelle, Yoann, Caroline, Anaïs,
Pierres Yves, Meriem.H, Tarik.H, Sanaa.B, Sihem.B, Tarik.C, Hamza.H, Ibrahim.H…)
***
Enfin, je remercie David, qui a tout partagé avec moi ces dernières années, pour son soutien
permanent, sa compréhension, sa patience et pour avoir supporté mes humeurs, souvent
angoissés ces derniers temps.


tel-00584308, version 1 - 8 Apr 2011
tel-00584308, version 1 - 8 Apr 2011Table des matières I

Table des matières


INTRODUCTION GENERALE ....................................................................................................................... 8

1 CONTEXTE ET PROBLEMATIQUE ..................................................................................................... 19
1.1 INTRODUCTION .................................................................................