Analyses de sûreté de fonctionnement multi-systèmes
168 pages
Français

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Analyses de sûreté de fonctionnement multi-systèmes

-

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
168 pages
Français
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Sous la direction de Pierre Bieber, Marc Zeitoun
Thèse soutenue le 23 novembre 2009: Bordeaux 1
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 fonctionnement 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 raffinement dans le cadre de la conception de modèles AltaRica : un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification du raffinement 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.
-AltaRica
-Méthodes formelles
-Raffinement
-Conception/validation d'architecture
-Sûreté de fonctionnement des systèmes
This thesis links two fields : 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 refinement notion in the AltaRica modelling process : a detailed model refines an abstract model if the abstract model simulates the detailed model. The AltaRica model refinement verification 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.
-AltaRica
-Formal methods
-Re?nement
-System design/validation
-Safety engineering
Source: http://www.theses.fr/2009BOR13885/document

Sujets

Informations

Publié par
Nombre de lectures 50
Langue Français
Poids de l'ouvrage 1 Mo

Extrait

oN 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
2009Analyses 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 raffinement dans le cadre de la conception de modèles AltaRica :
un modèle détaillé raffine un modèle abstrait si le modèle abstrait simule le modèle détaillé. La vérification
du raffinement 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, raffinement, conception/validation d’architecture, sûreté de
fonctionnement des systèmes
Multi-system safety analyses
Abstract : This thesis links two fields : 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 refinement notion in the AltaRica modelling process : a detailed
model refines an abstract model if the abstract model simulates the detailed model. The AltaRica model
refinement verification 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, refinement, system design/validation, safety engineering
Équipe Méthodes formelles - Modélisation et Vérification
Laboratoire Bordelais de Recherche en Informatique
351 cours de la Libération F-33405 Talence cedex
34REMERCIEMENTS
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 difficiles.
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 scientifique 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éflé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
5ses 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 difficulté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 fier 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 afin 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û

  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents