La confiance dans les systèmes complexes est aujourd'hui primordiale. Parmi les langages de modélisation dysfonctionnelle des systèmes, les chaînes de Markov sont un bon compromis entre la calculabilité des modèles et le pouvoir d'expression qu'elles apportent. Cependant, comme les chaînes de Markov rendent compte des différents états du système, leur taille est confrontée à l'explosion combinatoire. Il y a deux obstacles majeurs induits par cette explosion : la difficulté d'écrire des chaînes pour les grands systèmes à la main, et les besoins en ressources calculatoires pour leur résolution. Le premier obstacle est dépassé facilement en compilant les chaînes de Markov depuis un modèle de plus haut niveau (dans ces travaux, AltaRica 3.0 est utilisé).Dans cette thèse, nous nous sommes concentrés sur la génération partielle de chaînes de Markov, afin de dépasser le problème d'explosion combinatoire. La méthode est fondée sur l'observation que les systèmes réparables, même les plus grands, passent leur temps dans un petit nombre d'états proches de l'état nominal du système. La génération partielle utilise l'algorithme de Dijkstra, auquel est combiné un facteur de pertinence, qui permet la sélection des états les plus probables du système. Il est possible d'encadrer les valeurs des indicateurs de sûreté obtenus avec la chaîne partielle grâce à l'introduction d'une chaîne partielle avec puits.La méthode de génération partielle est entièrement implémentée et fait partie du projet AltaRica 3.0. Il est ainsi possible de calculer les indicateurs de sûreté des systèmes directement depuis un modèle AltaRica. Divers expériences ont été menées pour illustrer la faisabilité de la méthode, son passage à l'échelle, ainsi que ses points forts et ses limites. / Trustworthiness in systems is of paramount importance. Among safety modeling languages, Markov chains are a good tradeoff between the safety concepts that can be modeled and the ease of calculation. However, as they model the different states of the systems, they suffer from the state space explosion. This explosion has two drawbacks: it makes Markov chains very difficult to write by hand for large systems, and large Markov chain calculation is resource consuming. The first drawback is easily tackled by generating Markov chains from higher-level languages (such as AltaRica 3.0).In this thesis, we focused on the partial generation of Markov chains, to tackle the state space explosion of the models. This idea is based on the observation that even large repairable systems spent most of their times in a few number of states, that are close to the nominal state of the system. The partial generation is based on Dijkstra's algorithm and on a so-called relevance factor to generate only the most probable states of the Markov chain. The reliability indicators obtained with such a partial chain can be bounded with a slightly different Markov chain.The partial generation method is fully implemented in the AltaRica 3.0 project to automatically calculate the reliability indicators of a system modeled in AltaRica. Different experiments illustrate the practability of the method, as well as its strengths and weaknesses.

Les systèmes de production et de sûreté de fonctionnement sont d'une importance majeure dans l'industrie des procédés. Leurs performances impactent directement les intérêts de l'industrie. Ces systèmes ont des comportements similaires. Ces comportements peuvent être conceptualisés dans des modèles via des patterns de modélisation. La réutilisation de ces patterns permet de rendre le processus de modélisation à la fois simplifiée et plus efficace.Dans cette thèse, nous proposons un ensemble varié de patterns de modélisation. Ils sont classés en fonction de leur usage, ce qui reflète le fonctionnement d'un pattern de modélisation. Les patterns sont présentés sous forme d’un catalogue. Sur la base de l'étude de nombreux systèmes de production et de sécurité, vingt-quatre (24) patterns de modélisation sont introduits. Chaque pattern est représenté par un ensemble d'éléments structurés. Nous proposons une méthodologie basée sur les patterns pour l'analyse des performances des systèmes de production et de sûreté de fonctionnement.Pour tester la pertinence des patterns de modélisation suggérés, nous avons mené des études expérimentales sur un ensemble de systèmes de production et de sûreté. Tous les systèmes de validation sont extraits de la littérature. Ces systèmes traitent la majorité des difficultés de modélisation détectées auparavant. Une comparaison est effectuée entre les résultats obtenus en utilisant la modélisation basée sur les patterns et ceux rapportés dans la littérature. / Production and safety systems are crucial in the process industry. Their performances affect significantly the industry interests. These systems have common behaviors. Such behaviors can be captured in models via modeling patterns. By reusing modeling patterns, the modeling process can be simplified and made more efficient.In this thesis, we propose a versatile set of modeling patterns. They are classified according to their purpose, which reflects what a modeling pattern works for. Modeling patterns are exhibited as a catalog. Based on reviewing numerous production and safety systems, twenty-four (24) modeling patterns are introduced. Each pattern is illustrated with a set of structured items. We propose a pattern-based methodology for performance analysis of production and safety systems.To test the applicability of proposed modeling patterns, we conducted experimental studies on a set of production and safety systems. All systems are extracted from the literature. These systems are declared to cover most of modeling difficulties. Comparisons are performed between the results obtained using modeling patterns and those reported in the literature.

Les architectures des systèmes embarqués des nouvelles générations d'avions civils et militaires tendent à s'organiser autour d'une plateforme avionique constituée de calculateurs interconnectés par un réseau central. Ce type d'architecture a fait apparaitre le besoin de développer de nouvelles méthodes de conception afin d'assister le dialogue entre les concepteurs des fonctions à embarquer (commandes de vol, gestion de l'énergie, ...) et les architectes de la plateforme avionique. Il est, en particulier, primordial de s'assurer que l'allocation des ressources de la plateforme aux fonctions embarquées respecte les exigences de sûreté de fonctionnement propres aux systèmes avioniques. Dans un premier temps, un cadre général a été proposé pour modéliser et vérifier l'effet de l'allocation des ressources d'une plateforme avionique du point de la sûreté de fonctionnement. Ce cadre est fondé sur l'utilisation du langage AltaRica pour décrire formellement la propagation des défaillances au sein de systèmes embarqués et des outils associés à ce langage (model-checking, génération de séquences et d'arbres de défaillances) pour vérifier la tenue des exigences de sûreté de fonctionnement. Ce cadre a été utilisé pour étudier, d'une part, l'allocation d'équipements informatiques aux fonctions de systèmes embarqués, et d'autre part, les placements des équipements au sein de l'avion en tenant compte de risques tels que l'éclatement d'un pneu ou l'explosion d'un moteur. Dans un second temps, la génération d'allocations respectant les exigences de sûreté de fonctionnement a été étudiée. L'approche retenue est fondée sur l'expression de contraintes d'allocation sous forme d'inégalités linéaires entières et sur l'utilisation de techniques de résolution de ces contraintes. Plusieurs types de contraintes (ségrégation, co-location, exclusion, ...) sont pris en compte. De plus, des critères d'optimisation permettent de guider la résolution des contraintes de façon à proposer des allocations les plus pertinentes du point de vue des besoins des systèmes aéronautiques. Finalement, une approche intégrant les techniques de vérification et de génération a été proposée. La première étape consiste à vérifier un modèle des fonctions embarquées qui est indépendant de la plateforme avionique. Il est possible d'extraire automatiquement des contraintes d'allocation à partir des résultats de cette vérification. L'étape de résolution de contraintes génère alors une allocation sûre. Les travaux sont illustrés par deux études de cas industrielles : une fonction de suivi de terrain d'un avion de chasse et un système de génération et de distribution hydraulique d'un avion de type A320. / Abstract

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. / 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.

Les systèmes avioniques s'étoffent et se complexifient de plus en plus. Avec l'augmentation des capacités de calcul, de nouvelles architectures basées sur le partage de ressources émergent. Effectuer le diagnostic d'un système n'est désormais plus une opération anodine. L'enjeu actuel est donc de mettre en place des techniques de diagnostic performantes tout en optimisant les capacités de monitoring nécessaires.Ce mémoire donne une caractérisation basée modèle d'un système sous diagnostic, puis propose des techniques pour en évaluer les performances de diagnostic, ainsi que celles de son monitoring (relativement à ces performances). Le contexte industriel dans lequel s'inscrit cette thèse amène d'autres contraintes, notamment la prise en compte de la taille des systèmes avioniques à analyser. Cette thèse étudie alors l'applicabilité des techniques introduites dans ce contexte et en propose une adaptation. / Avionics systems become more and more complex. With the improvment of computing possibilities, new architectures based on resources sharing are growing up. Perform diagnosis of a system is no longer a trivial operation. The challenge is to develop efficient techniques of diagnosis while optimizing capabilities of monitoring required.This thesis give a model-based characterization of a system under diagnosis, and proposes techniques to assess diagnostic performances, as well as its monitoring ones (with respect to these diagnostic performances). The industrial context of this thesis brings other constraints, and in particular the need to handle the size of avionics systems to analyze. That thesis then examines the applicability of the introduced techniques to this particular context, and proposes an adaptation.

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.

Cette thèse propose des méthodes assistant la modélisation et l'évaluation qualitative de l'architecture de sûreté de fonctionnement des systèmes embarqués complexes. Ces architectures sont souvent construites à partir de motifs généraux d'architectures de systèmes correspondant à des mécanismes de sûreté récurrents comme des redondances, des détections, etc. En s'inspirant des principes des "patrons de conception" développés en génie logiciel, nous avons proposé une modélisation de ces mécanismes et des attributs permettant leur réutilisation lors des analyses de sûreté de fonctionnement. Ces analyses nécessitent de raisonner sur le comportement des systèmes en présence de pannes qui peut être modélisé à l'aide de langages formels comme AltaRica. Dans notre cas, les motifs correspondent à des abstractions d'architectures concrètes et donc requièrent une modélisation plus déclarative. Les propriétés étudiées étant en général dynamiques, nous avons choisi d'utiliser une logique temporelle pour les exprimer. Les motifs sont donc constitués d'une partie AltaRica et d'une partie propriétés. Ce type de modélisation mixte possède plusieurs intérêts, notamment lors de la conception en phase amont d'architectures de systèmes où il est possible de manipuler à la fois des parties d'un système conçues de manière détaillée et des spécifications. Elle a également pour buts de faciliter l'allocation d'exigences pour la validation d'architectures ainsi que le prototypage. Nous avons donc défini une notation mixant ces aspects opérationnels et déclaratifs.

Ce travail s'inscrit dans la continuité de l'étude du langage de description de systèmes AltaRica. Ce langage, développé au Labri, permet de modéliser des systèmes réels de manière hiérarchique. L'objectif de la thèse est d'introduire le temps quantitatif dans le but de concevoir des systèmes temps réel, c'est à dire des systèmes assujettis à des contraintes temporelles.<br />Deux extensions du langage sont proposées : une version temporisée et une hybride. Ces extensions respectent les caractéristiques du langage initial et conservent les aspects de hiérarchie, de synchronisation, de partage de variables et de priorité statique. En outre, afin d'améliorer les descriptions temps réel, de nouveaux opérateurs de modélisation, comme l'urgence et les priorités temporelles, ont été ajoutés. Nous obtenons ainsi un langage hiérarchique de haut niveau de modélisation de systèmes temps réel. <br />Une étude formelle complète a été menée sur la sémantique du langage, le pouvoir d'expression des langages AltaRica temps réel et des moyens de traductions automatiques vers des modèles classiques existants. Ces algorithmes reposent sur la notion de mise à plat de modèle, i.e. réécrire le modèle sans sous composant.<br />Enfin, le langage temporisé est implanté dans un prototype qui étant donné un modèle le met à plat puis le traduit en automate temporisé. Ainsi, certains systèmes réels ont pu être modélisés puis des propriétés ont été vérifiées à l'aide du model checker UPPAAL.

Les systèmes avioniques s'étoffent et se complexifient de plus en plus. Avec l'augmentation des capacités de calcul, de nouvelles architectures basées sur le partage de ressources émergent. Effectuer le diagnostic d'un système n'est désormais plus une opération anodine. L'enjeu actuel est donc de mettre en place des techniques de diagnostic performantes tout en optimisant les capacités de monitoring nécessaires.Ce mémoire donne une caractérisation basée modèle d'un système sous diagnostic, puis propose des techniques pour en évaluer les performances de diagnostic, ainsi que celles de son monitoring (relativement à ces performances). Le contexte industriel dans lequel s'inscrit cette thèse amène d'autres contraintes, notamment la prise en compte de la taille des systèmes avioniques à analyser. Cette thèse étudie alors l'applicabilité des techniques introduites dans ce contexte et en propose une adaptation.

Les méthodes formelles et la sûreté de fonctionnement sont deux domaines connexes qui s'intéressent à l'analyse des comportements des systèmes critiques. Ces domaines adoptent des points de vue différents mais complémentaires sur les systèmes. Les méthodes formelles considèrent le point de vue fonctionnel et adoptent, en général, une approche « vérification de programme ». Dans ce domaine on cherche en général à mettre en évidence un scénario menant le programme à un bogue, ou à générer de manière automatique des programmes sûrs (par rapport à leurs spécifications). La sûreté de fonctionnement considère plutôt les aspects dysfonctionnels des systèmes. Dans ce domaine on cherche à déterminer les scénarios prépondérants qui mènent le système à une défaillance ou à évaluer des mesures probabilistes sur ses comportements (fiabilité, disponibilité, ...).<br /><br />Les travaux présentés dans cette thèse ont été réalisés dans le cadre d'un projet industriel, AltaRica, qui ambitionne le rapprochement des méthodes formelles et<br />de la sûreté de fonctionnement. Cette unification se concrétise par le développement d'un atelier d'analyse système, l'atelier AltaRica, qui fédèrera à terme un ensemble de modèles et d'outils pour l'analyse des systèmes. Cet atelier propose une représentation unique pour la description des systèmes ; celle-ci étant destinée à être compilée vers des modèles/outils existants. Ce rapport présente le formalisme supporté par cet atelier, sa forme textuelle et graphique (le langage AltaRica), certaines propriétés de sa sémantique et quelques exemples de modélisations.<br /><br /> L'étude des scénarios de panne est un des principaux problèmes de la sûreté de<br />fonctionnement. Ce problème est généralement traité en utilisant le modèle des arbres de défaillances. Ce modèle ne permettant pas de prendre en compte le séquencement des pannes, cette thèse propose une solution au problème de l'obtention des scénarios de panne minimaux pour l'ordre des sous-mots.