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

De
Publié par

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
Publié le : jeudi 27 octobre 2011
Lecture(s) : 47
Nombre de pages : 168
Voir plus Voir moins

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ûrement pas été la même
sans toi.
Enfin un merci particulier pour mon cœur, ma Caro. Merci pour ton soutien durant toute la rédaction
jusqu’à la soutenance.
6TABLE 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 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2 LE LANGAGE ALTARICA ET SES OUTILS 27
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2.2 Le langage AltaRica . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
2.3 Les outils de modélisation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
2.4 Les langages pour les analyses de sûreté de fonctionnement de systèmes . . . . . . . . . . 44
3 LES ANALYSES DE SÉCURITÉ FONDÉES SUR LES MODÈLES 49
3.1 Modèle de propagation de défaillances . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
3.2 Modèle étendu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
3.3 Combinaison de modèles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61
4 LE RAFFINEMENT POUR ALTARICA 65
4.1 Définitions initiales . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66
4.2 Bisimulation interfacée . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72
4.3 Simulation interfacée . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
4.4 Simulation quasi-branchante interfacée . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90
4.5 Le raffinement AltaRica comparé . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
4.6 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5 UTILISATION DU RAFFINEMENT POUR LE DÉVELOPPEMENT DE SYSTÈMES SÛRS 109
5.1 Modélisation pour le raffinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 110
5.2 Spécialisation du raffinement pour la sûreté de fonctionnement des systèmes . . . . . . . . 119
5.3 Expérimentation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 131
5.4 Préservation d’exigences quantitatives . . . . . . . . . . . . . . . . . . . . . . . . . . . . 148
5.5 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149
Conclusion 151
Annexes 157
A ABRÉVIATIONS 157
B BOUNDARY BRANCHING SIMULATION INTERFACÉE 159
7TABLE DES MATIÈRES
C RELATIONS MECV 161
C.1 Masquage des événements instantanés . . . . . . . . . . . . . . . . . . . . . . . . . . . . 161
C.2 Test des états accessibles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
C.3 Simulation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162
C.4 Simulation quasi-branchante . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 163
D BIBLIOGRAPHIE 165
8INTRODUCTION
ièmeDepuis le début du XX siècle, le transport aérien ne cesse de se développer. Tout d’abord réservé au
transport de marchandises et de courrier, l’avion s’est depuis démocratisé permettant à chacun de voyager
à travers le monde. Outre le nombre de vols, la capacité des avions a augmenté. Ces facteurs expliquent
que le nombre de passagers transportés par avion augmente chaque année (+8,5% en 2005, +5% en 2006
et +7% en 2007). Cette évolution a deux conséquences :
– l’augmentation du nombre d’avions dans le ciel accroît les risques de collision en vol ;
– la capacité croissante des avions commerciaux implique un accroissement du nombre de victimes
possibles en cas d’accident.
De plus, tout avion qui s’écrase peut causer des pertes humaines tant à bord (les passagers et membres
d’équipage) qu’au sol en cas d’accident en zone habitée. Tous ces risques font que la sécurité est une
préoccupation majeure de l’industrie aéronautique. Les grands constructeurs se sont entendus pour exclure
la sécurité des domaines de concurrence et collaborent à l’amélioration des méthodes de travail dans ce
domaine.
Afin d’établir et de garantir un niveau de sécurité acceptable, des autorités de certification définissent
des exigences que chaque avion doit satisfaire pour obtenir une autorisation de voler. Chaque construc-
teur doit démontrer que l’avion fabriqué est conforme aux exigences des autorités en charge du pays de
production, puis aux exigences des autorités du pays d’immatriculation.
Le souci constant d’amélioration de la sécurité a permis de réduire le nombre d’accidents (cf. figure
0.1) et a ainsi contribué à faire de l’avion un des moyens de transport les plus sûrs.
FIG. 0.1: Passagers décédés par an pour 100 millions de miles passager, sur des vols commerciaux,
hors actes de malveillance intentionnelle (source : EASA Annual Safety Review 2008)
Schématiquement, un avion est composé d’une structure, appelée fuselage, et d’équipements, dits sys-
tèmes embarqués, permettant de contrôler l’avion. Les principales causes d’accidents sont l’erreur humaine
(d’un pilote ou du contrôleur aérien), les défaillances liées à la structure et les défaillances de systèmes em-
barqués. Nous nous intéressons à ces dernières qui font l’objet de différentes analyses.
9INTRODUCTION
Toute entreprise cherche constamment à optimiser ses coûts de conception pour améliorer les rende-
ments. Dans le cas de la production d’avions, cela revient à :
– réduire les masses et coûts des systèmes embarqués afin d’augmenter la charge utile et de réduire les
coûts de fabrication ;
– améliorer les processus pour réduire les temps de conception et, par conséquent, les délais de livrai-
son aux clients.
Afin de limiter les équipements embarqués, certains systèmes, autrefois indépendants, peuvent aujour-
d’hui partager des ressources. Par exemple, le transfert des données peut désormais, sur les avions A380 et
B787, être assuré par un réseau embarqué partagé par un grand nombre de systèmes. L’étude permanente
de nouvelles solutions techniques justifie le fait que l’avion est un moyen de transport à la pointe de la tech-
nologie. Néanmoins, les systèmes, s’ils peuvent désormais remplir plusieurs fonctions, s’avèrent de plus en
plus complexes et donc difficiles à analyser par les méthodes traditionnelles. Analyser des systèmes plus
complexes en un délai plus court contraint les avionneurs à étudier de nouvelles méthodes pour supporter
les analyses de sûreté de fonctionnement des systèmes.
Les modèles formels comme réponse au besoin d’évolution
L’utilisation des modèles formels dans l’industrie représente une évolution majeures des méthodes de
travail. Un modèle est une représentation abstraite d’un objet : seules les informations pertinentes pour
l’étude à mener sont prises en compte dans la spécification de l’objet.
Le développement de l’informatique a vu la création de langages formels, chacun défini par :
– une syntaxe : un lexique et une grammaire (règles d’écriture) permettent de décrire certains aspects
(propres à chaque langage) d’un système de façon compacte et compréhensible par tout connaisseur
du langage ;
– une sémantique : interprétation de la description faite par l’ordinateur.
Un modèle formel est une traduction de la spécification d’un objet dans un langage formel. Les out-
ils informatiques associés au langage formel, permettent d’étudier certaines caractéristiques d’un objet
sans avoir à le fabriquer. Ainsi, par exemple, un système peut être simulé pour en étudier son comportement.
Les modèles formels présentent de nombreux avantages pour l’industrie. Lorsque plusieurs interlocu-
teurs partagent des informations, formaliser ces dernières permet de prévenir toute interprétation pouvant
conduire à une mauvaise compréhension. De plus, les outils de modélisation tirent profit de la puissance de
calcul des ordinateurs pour traiter de grandes quantités de données, là où un ingénieur devrait choisir les
calculs à effectuer.
Cependant, l’utilisation de modèles modifie l’organisation du temps de travail : la sélection des infor-
mations à modéliser et la validation du modèle constituent la part prépondérante du travail contrairement à
la production de résultats qui, étant en partie automatisée, s’effectue plus rapidement que par les méthodes
classiques. Dès lors, les modèles formels ne présentent un intérêt, pour motiver une évolution des pratiques,
que s’ils garantissent un gain :
– de temps, tout en préservant la qualité des résultats ;
– de précision des résultats, sans allonger le temps de travail.
A ce jour, dans l’aéronautique, les modèles s’avèrent utiles pour étudier l’aérodynamique du fuselage
ou l’installation des systèmes embarqués au sein de l’avion et sont intégrés au processus de développement
de certains logiciels embarqués. Dans le domaine des analyses de sûreté de fonctionnement des systèmes,
la société Dassault Aviation a, en 2005, démontré que les commandes de vol de son Falcon 7X étaient con-
formes aux exigences des autorités à l’aide de modèles réalisés en langage AltaRica. Ce langage, développé
avec le Laboratoire Bordelais de Recherche en Informatique (LaBRI) pour supporter les analyses de sûreté
de fonctionnement des systèmes, fait l’objet d’expérimentations internes par la société Airbus depuis 4 ans.
Des contraintes à résoudre pour une industrialisation de l’approche
La conception d’un système suit un processus incrémental : une spécification abstraite est progressive-
ment enrichie jusqu’à obtenir un niveau de détail suffisant pour procéder à la fabrication des composants du
10

Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.

Diffusez cette publication

Vous aimerez aussi