Remerciez-le!

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

N° d’ordre : 184 ÉCOLE CENTRALE DE LILLE T H È S E pour l’obtention du Doctorat

N° d’ordre : 184 ÉCOLE CENTRALE DE LILLE T H È S E pour l’obtention du Doctorat de l’École Centrale de Lille Spécialité : Automatique, Génie informatique, Traitement du Signal et Images présentée par Ahmed Mekki Titre de la thèse : Contribution à la Spéciﬁcation et à la Vériﬁcation des Exigences Temporelles Proposition d’une extension des SRS d’ERTMS niveau 2 Soutenue le 18 avril 2012 devant le jury d’examen Président & Rapporteur M. Walter Schön Professeur des Universités, UTC-Compiègne Rapporteur M. Kamel Barkaoui Professeur des Universités, CNAM-Paris Examinateurs M. El-Miloudi El-Koursi Directeur de Recherche, IFSTTAR-Villeneuve d’Ascq M. David Gouyon Maître de Conférences, CRAN-Nancy M. Eric Rutten Chargé de Recherche (HDR), INRIA-Rhône-Alpes Encadrant M. Mohamed Ghazel Chargé de Recherche, IFSTTAR-Villeneuve d’Ascq Directeur M. Armand Toguyéni Professeur des Universités, LAGIS-École Centrale de Lille Thèse préparée au laboratoire ESTAS de l’Institut Français des Sciences et Technologies des Transports, de l’Aménagement et des Réseaux (IFSTTAR). Laboratoire LAGIS de l’École Centrale de Lille École Doctorale SPI 072 (Lille I, Lille III, Artois, ULCO, UVHC, EC Lille) PRES Université Lille Nord-de-France 1 Ahmed MEKKI Ahmed MEKKI 2 À ma grande-mère Bournia 3 Ahmed MEKKI Ahmed MEKKI 4 Remerciements Les travaux de thèse présentés dans ce manuscrit ont été réalisés à l’institut français des sciences et technologies des transports (IFSTTAR) à Villeneuve d’Ascq. Je voudrais saisir cette opportunité pour remercier IFSTTAR de m’avoir oﬀert cette expérience magniﬁque. La recherche scientiﬁque est un métier magique et c’est un bonheur de l’avoir commencé ici. C’est avec toute ma gratitude que j’exprime ici mes plus vifs remerciements à Mohamed Ghazel, qui a bien voulu accepter d’encadrer ce travail de thèse. Sans sa disponibilité malgré sa charge de travail, sa patience, les conseils qu’il m’a prodigués tout au long de ces trois ans, ses mots d’encouragement, ce travail n’aurait pas pu, sans doute, être mené à son terme. Merci. J’exprime ma profonde reconnaissance et remerciement à Armand Toguyéni pour avoir dirigé mes travaux de thèse, pour sa passion, ses conseils et pour m’avoir aidé à améliorer mon travail. Malgré ses responsabilités administratives qui s’ajoutent à sa charge du travail d’ensei- gnement, d’encadrement et de recherche, il a toujours su trouver du temps pour discuter. Merci. Je remercie chaleureusement Florent Peres, qui a suivi de près une partie de ce travail, sans qui cette partie n’existerait pas sous cette forme. Ses observations judicieuses et ses remarques ont été des plus déterminantes dans la conduite de ces travaux et dans la forme ﬁnale qu’ils ont pris. Remerciements à Monsieur Kamel Barkaoui, professeur des universités au CNAM-Paris, et à Monsieur Walter Schön, professeur des universités à l’université de technologie de Compiègne, pour avoir accepté de rapporter ma thèse. Je remercie également tous les membres du jury pour avoir bien voulu participer à ma soutenance : Monsieur Eric Rutten, directeur de recherche à l’INRIA Rhône-Alpes„ Monsieur David Gouyon, maître de conférences au CRAN-Nancy, et Monsieur El-Miloudi El-Koursi, directeur de recherche à l’IFSTTAR-Villeneuve d’Ascq et directeur de l’unité ESTAS. Mes remerciements vont également à tous les personnels du centre IFSTTAR-Villeneuve d’Ascq pour la gentillesse et la convivialité dont ils ont fait preuve et qui ont rendu mon séjour très agréable parmi eux. Remerciements à tous les doctorants, post-doctorants, du IFSTTAR-Villeneuve d’Ascq. Merci donc à Nizar, Sana, Nedim, Sabrine, Jing, Khaled, Stephen et Nesrine, ainsi que à tous mes amis : Khaled M., Issam, Mahmoud D., Mahmoud B., Mamoudou K., Ahmed S. et Abdessalem. J’ai une pensée toute particulière pour mon confrère Youness à qui je souhaite de terminer le plus rapidement possible et dans les meilleures conditions ses travaux de thèse. Je lui souhaite bonne continuation tout au long du chemin qu’il a choisi d’emprunter après sa thèse. Dans ces moments importants, je pense très fort à ma famille. Tout ça n’aurait jamais été possible sans le soutien inconditionnel de mes parents Saïda et Tijani, qui ont toujours cru en moi. Merci pour avoir fait de moi ce que je suis à présent. Merci à tous mes sœurs et mes frères. Remerciements pour m’avoir toujours soutenu dans mes entreprises et dans les moments diﬃciles. Une pensée toute particulière pour mon frère Habib pour son soutien inconditionnel durant mes études universitaires à Monastir, à Tunis et à Lille. J’exprime ma profonde gratitude envers ma deuxième famille en France : ma tante Aïcha, 5 Ahmed MEKKI mon oncle Hassen, Atef, Hanan et Fayçal pour leur accueil, leurs encouragements et tous les bons moments que nous avons partagés ensemble. Merci inﬁniment à Sophie et Zobeir Lafhaj pour m’avoir accueilli à Lille. Merci à toutes les personnes, qui m’ont toujours soutenu et encouragé au cours de la thèse, et que je n’ai pas citées ici et qui se reconnaîtront à travers ces quelques lignes. Mention spéciale au printemps Arabe. Je ne peux pas passer sans remercier les jeunes arabes qui acceptent de mourir aﬁn d’être les maîtres de leurs destins. De Sidi Bouzid en Tunisie à Benghazi en Libye, de la place de la Libération (“Tahrir”) en Égypte à Deraa en Syrie, les peuples arabes, trop longtemps opprimés, se sont soulevés pour briser les chaines imposées par des dictatures néo-féodales et pour que triomphe la liberté, l’égalité et la justice. Une pensée spéciale à celle qui n’a eu le temps de dire un dernier au revoir, ma grande-mère Bournia. Ce n’est qu’une fois qui ne sont plus là que l’on se rend compte à quel point certaines personnes qu’on aime tiennent une place si importante dans nos vies. C’est à son âme que je dédie ce travail, elle qui n’aura pu voir son achèvement. Tu me manques. Ahmed MEKKI 6 Table des matières 1 Introduction : problématique et contributions 19 1.1 Contexte et problématique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 1.1.1 Ingénierie système . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 1.1.2 Ingénierie des exigences . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 1.1.3 Problématique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 1.1.3.1 Méthodes de spéciﬁcation . . . . . . . . . . . . . . . . . . . . . . . . . 24 1.1.3.2 Techniques de vériﬁcation . . . . . . . . . . . . . . . . . . . . . . . . . 25 1.1.3.3 En pratique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 1.2 Contributions de la thèse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 1.2.1 Étape de spéciﬁcation des exigences temporelles . . . . . . . . . . . . . . . 27 1.2.1.1 Une nouvelle classiﬁcation des exigences temporelles . . . . . . . . . 27 1.2.1.2 Grammaire de spéciﬁcation . . . . . . . . . . . . . . . . . . . . . . . . 27 1.2.1.3 Analyse de la cohérence . . . . . . . . . . . . . . . . . . . . . . . . . . 27 1.2.2 Modélisation du comportement : transformation de modèles . . . . . . . 28 1.2.3 Étape de vériﬁcation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1.2.3.1 Vériﬁcation par observateur . . . . . . . . . . . . . . . . . . . . . . . . 29 1.2.3.2 Base de patterns d’observation . . . . . . . . . . . . . . . . . . . . . . 29 1.2.4 Proposition d’intégration du passage à niveau aux spéciﬁcations d’ERTMS niveau 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1.3 Plan de la thèse . . . . . . . . . . . . . . . . . uploads/Geographie/ these-ahmed-mekki.pdf