Remerciez-le!

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

No d’ordre: 3885 THÈSE PRÉSENTÉE À L’UNIVERSITÉ BORDEAUX I ÉCOLE DOCTORALE DE M

No d’ordre: 3885 THÈSE PRÉSENTÉE À L’UNIVERSITÉ BORDEAUX I ÉCOLE DOCTORALE DE MATHÉMATIQUES ET INFORMATIQUE Par Romain Bernard POUR OBTENIR LE GRADE DE DOCTEUR SPÉCIALITÉ : Informatique Analyses de sûreté de fonctionnement multi-systèmes Soutenue le : 23 novembre 2009 Après avis de : Hubert Garavel . . . . Rapporteurs Antoine Rauzy . . . . Devant la Commission d’examen formée de : Pierre Bieber Directeur de thèse, ONERA . . . . . . . . . . . . . . . Examinateurs Jean-Philippe Domenger Professeur, Université Bordeaux 1 . . . . . . . . . . Alain Griffault Maître de Conférence, Université Bordeaux 1 Marc Zeitoun Directeur de thèse, Université Bordeaux 1 . . . Sylvain Metge Ingénieur, Airbus . . . . . . . . . . . . . . . . . . . . . . . . . François Pouzolz Ingénieur, Airbus . . . . . . . . . . . . . . . . . . . . . . . . . Hubert Garavel Directeur de Recherche, INRIA . . . . . . . . . . . . Rapporteur Antoine Rauzy Chargé de Recherche, CNRS . . . . . . . . . . . . . . Rapporteur 2009 Analyses de sûreté de fonctionnement multi-systèmes Résumé : Cette thèse se situe au croisement de deux domaines : la sûreté de fonctionnement des systèmes critiques et les méthodes formelles. Nous cherchons à établir la cohérence des analyses de sûreté de fonc- tionnement réalisées à l’aide de modèles représentant un même système à des niveaux de détail différents. Pour cela, nous proposons une notion de rafﬁnement dans le cadre de la conception de modèles AltaRica : un modèle détaillé rafﬁne un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vériﬁcation du rafﬁnement de modèles AltaRica est supportée par l’outil de model-checking MecV. Ceci permet de réaliser des analyses multi-systèmes à l’aide de modèles à des niveaux de détail hétérogènes : le système au centre de l’étude est détaillé tandis que les systèmes en interface sont abstraits. Cette approche a été appliquée à l’étude d’un système de contrôle de gouverne de direction d’un avion connecté à un système de génération et distribution électrique. Mots clés : AltaRica, méthodes formelles, rafﬁnement, conception/validation d’architecture, sûreté de fonctionnement des systèmes Multi-system safety analyses Abstract : This thesis links two ﬁelds : system safety analyses and formal methods. We aim at checking the consistensy of safety analyses based on formal models that represent a system at different levels of detail. To reach this objective, we introduce a reﬁnement notion in the AltaRica modelling process : a detailed model reﬁnes an abstract model if the abstract model simulates the detailed model. The AltaRica model reﬁnement veriﬁcation is supported by the MecV model-checker. This allows to perform multi-system safety analyses using models with heterogeneous levels of detail : the main system is detailed whereas the interfaced systems remain abstract. This approach has been applied to the analysis of a rudder control system linked to an electrical power generation and distribution system. Key words : AltaRica, formal methods, reﬁnement, system design/validation, safety engineering Équipe Méthodes formelles - Modélisation et Vériﬁcation Laboratoire Bordelais de Recherche en Informatique 351 cours de la Libération F-33405 Talence cedex 3 4 REMERCIEMENTS Je remercie Jean-Philippe Domenger d’avoir accepté de présider le jury, ainsi que mes rapporteurs Hubert Garavel et Antoine Rauzy (un merci particulier pour le soutien lors de ma présentation à Lambda- Mu). Un grand merci à Pierre Bieber qui a su gérer ma pugnacité. Cette thèse doit beaucoup à Pierre et sa connaissance des mondes académiques et industriels. Merci d’avoir toujours trouvé du temps pour répondre à mes questions et de m’avoir soutenu, tout particulièrement durant les derniers mois. Merci d’avoir compris mon attirance pour le monde industriel et d’avoir composé avec pour mener à bien ces trois années. Tes qualités humaines et ton sens de l’humour ne peuvent transparaître dans ce mémoire mais ont compté pour moi dans les moments difﬁciles. Je tiens à remercier Marc Zeitoun d’avoir accepté de diriger ma thèse. Tes qualités pédagogiques m’ont permis de comprendre des éléments théoriques qui auparavant pouvaient me poser problème. Ton sens du détail et de la vulgarisation scientiﬁque ont contribué à rendre lisible le cœur théorique de mes travaux. Merci pour les entretiens à proximité du tableau blanc qui m’ont permis de comprendre ou de réﬂéchir à ces relations qui étaient souvent très abstraites à mes yeux. Je tiens à remercier Alain Griffault pour avoir initié le master 2 Ingénierie des Systèmes Critiques qui m’a permis d’entrer en contact avec la société Airbus et de m’avoir toujours soutenu. Je me souviens t’avoir entendu dire que, à l’issue de ce master, nous serions des VRP responsables de promouvoir les méthodes formelles dans l’industrie et j’espère avoir contribué à cet objectif. Un grand merci pour les discussions dans ton bureau qui m’ont permis de mieux comprendre le monde de la recherche ou de parfaire ma connaissance d’AltaRica. Je tiens à remercier Sylvain Metge de m’avoir donné l’opportunité d’effectuer mon stage de master puis ma thèse au sein de l’entreprise Airbus. Je garde en mémoire la rigueur avec laquelle tu as lu mon mémoire de master et que je cherche à appliquer dans mon travail depuis. Nos discussions sur le championnat de football ont apporté des moments de détente au bureau d’autant plus agréables que le titre bordelais approchait. Je remercie François Pouzolz d’avoir pris la succession de Sylvain pour m’encadrer d’un point de vue industriel. Merci de m’avoir apporté ta connaissance de l’industrie pour décrypter les mécanismes de cette grande société qu’est Airbus. Merci pour toutes nos discussions sur des sujets variés au bureau et en dehors (sur le retour vers notre jolie région natale). Je tiens à remercier Charles Zamora de m’avoir accueilli chez Airbus au sein de son équipe, pour effectuer mes premiers pas dans l’industrie. Je me suis très vite senti bien intégré dans une belle équipe aux accents français, italien, espagnol, allemand et bien entendu écossais. Je n’oublierai en particulier jamais le célèbre “I’ve a joke for you” de l’ami Chris BBHH Lacey, la bonne humeur d’Alessandro “esseptionnel” Landi et les anecdotes de Michel Tchorowski. Une pensée pour Delphine Johan, la plus pressée des membres de l’équipe mais avec qui j’ai apprécié de faire des pauses-chocolat. J’ai passé quatre belles années et je remercie tous ceux qui m’ont consacré une partie de leur temps. Je remercie les membres du DTIM à l’ONERA et de l’équipe MF au LaBRI pour leur accueil. Plus particulièrement, je remercie Gérald (pour sa connaissance d’AltaRica et pour avoir bien voulu me fournir 5 ses sources LaTeX qui ont servi de modèle à la rédaction de ce mémoire) et Aymeric (pour son aide concernant MecV et sa réactivité à prendre en compte certains souhaits). Un grand merci à ma famille qui m’a toujours soutenu malgré les difﬁcultés diverses de la vie. Une pensée particulière pour ma mère (qui a stressé probablement plus que moi), pour mes sœurs Faustine et Manon, pour ma grand-mère Maïté (qui a suivi tous les travaux sans vraiment oser me dire quand elle ne comprenait pas) et mon grand-père Paul (qui pensait me voir un jour pilote mais qui, j’espère, serait ﬁer de me voir docteur autant que je le suis de ses réalisations), pour ma grand-mère Odette (qui a trouvé la plus jolie description d’un docteur en informatique : celui qui soigne les ordinateurs), pour ma tante Nadine et mon oncle Michel d’être venus assister à ma soutenance, et pour mon père (qui m’a transmis l’amour des avions). Un grand merci à mes amis Sylvie, Clément, Manu, Léo, Pib et Cec, Audrey et David, Steph, Rabah, Dine et ceux que j’oublie pour m’avoir soutenu et changé les idées aﬁn de prolonger les hauts et de tenir le coup durant les bas. Un merci argentin à mes amis Maria et Eduardo. Merci pour votre gentillesse et pour tous les souvenirs lors de ma dernière visite dans votre beau pays. Je remercie les badistes du TOAC (Sylvie et Arno, Lili, Lolo, Guigui et Dédé ...) pour leur accueil et ces bons moments passés en particulier sur les tournois. Un merci particulier pour Elo : cette année ensemble m’a permis de grandir, de découvrir Toulouse et mon intégration au club n’aurait sûrement pas été la même sans toi. Enﬁn un merci particulier pour mon cœur, ma Caro. Merci pour ton soutien durant toute la rédaction jusqu’à la soutenance. 6 TABLE DES MATIÈRES TABLE DES MATIÈRES Introduction 9 1 LA SÉCURITÉ DES SYSTÈMES AÉRONAUTIQUES 15 1.1 La sûreté de fonctionnement des systèmes dans le monde aérien . . . . . . . . . . . . . . 16 1.2 Processus actuel . . . . . . . . . . . . . . . . . . . . . . . . . . . . uploads/Geographie/ these-rbernard09fichierimportant.pdf