Remerciez-le!

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

These rbernard09fichierimportant

No d ? ordre 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 Après avis de novembre Hubert Garavel Rapporteurs Antoine Rauzy Devant la Commission d ? examen formée de Pierre Bieber Jean-Philippe Domenger Alain Gri ?ault Marc Zeitoun Sylvain Metge François Pouzolz Hubert Garavel Antoine Rauzy Directeur de thèse ONERA Professeur Université Bordeaux Ma? tre de Conférence Université Bordeaux Directeur de thèse Université Bordeaux Ingénieur Airbus Ingénieur Airbus Directeur de Recherche INRIA Chargé de Recherche CNRS Examinateurs Rapporteur Rapporteur C CAnalyses 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 fonctionnement réalisées à l ? aide de modèles représentant un même système à des niveaux de détail di ?é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 di ?erent 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 cours de la Libération F- Talence cedex C CREMERCIEMENTS 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 à LambdaMu Un grand