Retour au site du LAAS-CNRS

Résumé

Les travaux présentés dans ce mémoire ont pour objectif de définir une stratégie appropriée pour le test de logiciels critiques orientés-objet. La stratégie de test que nous préconisons s'appuie sur la complémentarité de données de test statistique et déterministe. Les entrées de test statistiques sont générées automatiquement à partir de l'information présente dans les diagrammes d'état UML ; en complément, les entrées de test déterministes ciblent des points singuliers du domaine déntrée. Cette stratégie mixte s'intègre dans un environnement commercial de modélisation (Rose RealTime) permettant ainsi la génération automatique à la fois des entrées de test statistiques et des sorties attendues. Le pouvoir défficacité de cette stratégie mixte est évalué par une technique d'injection de fautes logicielles, appelée analyse de mutation. Dans ce cadre, un outil d'analyse de mutation pour programmes Java a été développé sur les bases d'une idée originale, associant analyse syntaxique et réflexivité pour l'injection de différents types de fautes (traditionnelles et orientées-objet). Ces travaux théoriques sont illustrés sur une étude de cas industrielle du domaine avionique. Les résultats expérimentaux confirment la pertinence de l'approche élaborée et montrent son efficacité prometteuse vis-à-vis de la recherche de fautes. Ces mesures défficacité sont complétées par une étude comparative de l'approche proposée avec une approche déterministe utilisée expérimentalement chez ROCKWELL-COLLINS.

Abstract

A Statistical Approach for Testing Object-Oriented Critical Software : Experimentation on an Avionics Software ABSTRACT: This dissertation is concerned with the goal of defining an appropriate strategy for testing objectoriented critical software. The proposed test strategy combines statistical and deterministic testing. The statistical test case input values are automatically generated from the information collected in UML state diagrams; in addition, deterministic input values target singular points of the input domain. The mixed strategy is integrated in a commercial modeling environment (Rose RealTime), facilitating the automated generation of both statistical input values and the associated expected outputs. The fault revealing power of this strategy is assessed using a software fault injection technique, called mutation analysis. In this framework, a mutation analysis tool for Java programs has been developed on the basis of an original idea, dealing with syntactic analysis and reflection for the injection of different types of faults (traditional and object-oriented). This theoretical work is illustrated on an industrial case study from the avionics domain. Experimental results confirm the adequacy of the proposed approach and show its high efficiency from a fault-revealing standpoint. These efficiency measures are augmented by a comparative study between the proposed approach and a deterministic approach used experimentally at ROCKWELL-COLLINS.

Mots-Clés / Keywords

Object-oriented software; Mutation analysis; Probabilistic generation; Software testing; Java; UML; Logiciels orientés-objet; Analyse de mutation; Génération probabiliste; Test du logiciel;

Résumé

La généralisation des systèmes multiprocesseurs non spécialisés et multi-performants, ayant plusieurs niveaux d'accomplissement du service et destinés à des applications variées, a donné naissance à ce que nous appelons des systèmes multiprocesseurs à usage multiple. Ce mémoire est consacré à la modélisation de tels systèmes et l'évaluation de leurs mesures de sûreté de fonctionnement et de performabilité. Nous proposons une méthode générale permettant d'évaluer ces mesures, de façon générique, pour toute une gamme de systèmes à usage multiple. Cette méthode est basée sur une idée originale : séparer explicitement les aspects inhérents à l'architecture du système et les aspects relatifs au service tel qu'il est perçu par les applications des utilisateurs. Le modèle global construit avec cette méthode est ainsi composé de deux parties : a) un modèle architectural décrivant le comportement de l'architecture support, incluant ses composants matériels et logiciels et leurs interactions et b) un modèle du service exprimant les besoins en service des applications utilisant cette architecture. La méthode est structurée en quatre étapes et la construction des deux modèles est régie par un ensemble de règles et de recommandations. Cette méthode est appliquée à la modélisation d'un système multiprocesseur à usage multiple réel mettant en ¿uvre une mémoire partagée distribuée. Cette architecture sert de référence pour la conception d'architectures plus évoluées. Nous montrons comment réutiliser le modèle et les résultats obtenus pour l'architecture de référence afin d'évaluer les mesures de ces architectures évoluées. Nous présentons enfin l'ensemble des résultats et montrons comment ils peuvent servir à la fois au constructeur et aux utilisateurs de tels systèmes.

Abstract

The generalization of gracefully degradable and application-independent multiprocessor systems has led to what we refer to as multipurpose multiprocessor systems. This dissertation is devoted to the modelling of such systems and to the evaluation of their dependability and performability measures. We have developed a general modelling method based on an original idea: the explicit separation of architectural concerns from those related to the service provided to the users. The overall model built with this method is thus composed of two different parts: an architectural model describing the behavior of system hardware and software components and a service model dedicated to user needs from the service point of view. The construction of the two models is governed by a set of rules and recommendations. We illustrate the method on a real multipurpose multiprocessor system with a distributed shared memory. This architecture can serve as the reference architecture for the design of more complex, enhanced versions of the system. We show how to reuse the model and the results obtained for the reference architecture to evaluate measures for these enhanced architectures. Finally, we discuss the results and show how they can serve the system manufacturer as well as its users

Mots-Clés / Keywords

Distributed shared memory; Multipurpose systems; Multiprocessor systems; Modular modelling; Generalized Stochastic Petri Nets; Performability; Dependability evaluation; Mémoire partagée distribuée; Systèmes à usage multiple; Systèmes multiprocesseurs; Modélisation modulaire; Réseaux de Petri stochastiques généralisés; Performabilité; Evaluation de la sûreté de fonctionnement;

Résumé

Les travaux présentés dans ce mémoire définissent un cadre théorique pour le test de logiciels développés selon la méthode formelle B. Les tests visent à révéler les fautes dues à une mauvaise compréhension ou à une mauvaise modélisation d'un besoin fonctionnel, et complètent ainsi les preuves effectuées pendant le développement formel. Un développement B peut être vu comme une série d'étapes durant lesquelles des modèles de plus en plus concrets de l'application sont construits, le code final pouvant être considéré comme une version compilée du modèle le plus concret. Le cadre théorique de test que nous avons défini est un cadre unifié, indépendant du fait que les résultats de test soient obtenus de l'animation des modèles ou de l'exécution du code. Ce cadre est explicitement lié à la notion du raffinement des modèles B : pour une entrée de test, l'acceptation des résultats fournis par un modèle implique l'acceptation des résultats fournis par les raffinements corrects de celui-ci. Nous définissons ensuite une approche d'analyse structurelle des modèles B. En poursuivant le cadre unifié, notre objectif est de définir des stratégies de couverture qui soient applicables à la fois à un modèle abstrait et à un modèle concret. Ceci a nécessité d'unifier pour les modèles B deux catégories de critères : ¿ critères de couverture des spécifications orientées modèle basés sur la couverture des prédicats avant-après ; ¿ critères classiques de couverture structurelle des programmes basés sur la couverture du graphe de contrôle. A partir de cette unification, nous avons défini un ensemble de critères, ordonnés selon la relation d'inclusion, qui complètent les critères existants.

Abstract

The work presented in this dissertation concerns the definition of a theoretical framework for testing software developed within the B formal method. The test aims to reveal specification faults due to a misunderstanding or a misrepresentation of a functional requirement, and thus complement the proofs performed during the formal development process. The B development process can be seen as a series of steps during which successively more concrete models of the system are constructed, the final code being considered as a compiled version of the most concrete model. The theoretical framework that we have defined is a unified framework, independent of the fact that the results are obtained by animation of models or by execution of the final code. The framework is explicitly related to the notion of refinement of B models: for a given test input, the acceptance of the results of a given model implies the acceptance of the results of its correct refinements. We then define an approach to structural analysis of B models. Following the unified framework, our aim is to define coverage strategies applicable to abstract models as well as to concrete ones. This has required the unification of two categories of criteria for B models: ¿ coverage criteria defined for model oriented specifications based on the coverage of before-after predicates; ¿ classical structural coverage criteria of programs based on the coverage of control flow graphs. From this unification, we have defined a set of criteria, ordered according to the inclusion relation, that complete the existing hierarchy of criteria.

Mots-Clés / Keywords

Méthode B; Test du logiciel; Validation de modèles formels; Oracle de test; Analyse structurelle; Critères de couverture; B method; Software testing; Validation of formal models; Test Oracle; Structural analysis; Coverage criteria;

Résumé

L'objectif de cette thèse est la conception et l'implémentation d'un protocole à métaobjets adapté à la tolérance aux fautes d'objets Corba. En effet, il n'existe pas, à ce jour, de protocole à métaobjets satisfaisant dans ce contexte. Le protocole que nous définissons permet, d'une part, le contrôle du comportement et de l'état interne des objets Corba, et d'autre part, le contrôle des liens entre clients et serveur ainsi qu'entre objets et métaobjets, le tout de façon dynamique. L' implémentation proposée est adaptée à l'utilisation d'une plateforme Corba standard grâce à l'utilisation de langages ouverts et de réflexivité à la compilation : ces outils permettent de personnaliser le processus de compilation afin d'exhiber à l'exécution les informations nécessaires aux mécanismes de tolérance aux fautes. Un autre avantage de la réflexivité à la compilation est de permettre, de façon simple, d'assurer le respect de conventions de programmation grâce au filtrage du code source des applications. Ce protocole, bien intégré à Corba, tire également profit, lorsque c'est possible, des éléments réflexifs fournis par le support d'exécution du langage. C'est le cas avec Java, par exemple, qui permet la sérialisation des objets, grâce à ses aspects réflexifs limités. Lorsque le support du langage n'est pas réflexif, comme pour C++ par exemple, la réflexivité à la compilation permet également de mettre en ¿uvre des techniques de sauvegarde et de restauration de l'état des objets ; état complet et état partiels peuvent être contrôlés par les métaobjets. Les différentes propriétés de ce protocole à métaobjets sont illustrées par une proposition d'architecture Corba permettant d'intégrer à l'application des mécansimes de tolérance aux fautes de manière très flexible. Les propriétés de cette approche sont une bonne séparation entre l'application et les mécanismes non-fonctionnels implémentés dans les métaobjets, l'aspect dynamique du lien entre objets et métaobjets, la composabilité et la réutilisation des mécanismes ainsi que la transparence pour l'utilisateur. Enfin, ce protocole à métaobjets est suffisamment générique pour tirer parti de l' ouverture, au sens de la réflexivité, des logiciels de base (système d'exploitation et middleware) de la plateforme.

Abstract

The goal of this dissertation is to design and implement a metaobject protocol adapted to fault-tolerance in Corba applications. No currently available metaobject protocol is satisfying in this context. We define a protocol that enables dynamic control of both the behaviour and internal state of Corba objects and of clients/servers and objects/metaobjects links. The implementation we propose is well adapted to a standard Corba platform thanks to the use of open languages and compile-time reflection: these tools allow the compilation process to be customized in order to obtain information that is necessary to fault-tolerance mechanisms. Another benefit of compile-time reflection is to enable, in a simple way, to enforce programming conventions thanks to the filtering of application source code. This protocol, well integrated with Corba, can also benefit from reflective properties of the underlying language runtime, such as the limited reflection provided by Java for object serialization. When the language runtime is not reflective, as for C++, compile-time reflection can be used to implement methods for saving or restoring the internal state of objects; both complete or partial state can be controlled by metaobjects. The various properties of this metaobject protocol are illustrated in an architecture proposal which allows fault-tolerance mechanisms to be integrated to the application in a flexible manner. This approach offers useful properties such as separation of concerns between the application and the non-functional mechanisms implemented as metaobjects, dynamicity of links between objects and metaobjects, composability and reuse of mechanisms and user transparency. Finally, this metaobject protocol is sufficiently generic to take advantage of any openness, in a reflective sense, of the platform's underlying software (operating system and middleware).

Mots-Clés / Keywords

Tolérance aux fautes; Réflexivité; Corba; Protocole à métaobjets; Architectures; Dependability; Reflection; Metaobject protocols;

Résumé

L'utilisation de micronoyaux du commerce s'impose aujourd'hui dans le cadre de la conception de systèmes, même soumis à de fortes contraintes de sûreté de fonctionnement, comme une approche de plus en plus attractive. Les travaux présentés dans ce mémoire ont pour objectif de proposer des réponses aux interrogations soulevées par cette nouvelle tendance. Nous développons une méthode d'évaluation et d'amélioration des propriétés de sûreté de fonctionnement d'un micronoyau du commerce. Tout d'abord, nous justifions la pertinence de l'injection de fautes pour la caractérisation des modes de défaillance d'un micronoyau. Nous présentons les lignes directrices qui ont conduit au développement d'un outil d'évaluation par injection de fautes, pour l'aide à la conception de micronoyaux : MAFALDA. Par la suite, nous utilisons MAFALDA pour l'analyse du micronoyau commercial Chorus/ClassiX. À partir des leçons tirées de cette étude, nous proposons des recommandations pour améliorer les propriétés de sûreté de fonctionnement du micronoyau, selon le point de vue du fournisseur et des développeurs de systèmes. Ensuite, nous développons une approche novatrice de confinement des erreurs, d'origines externe et interne, pouvant affecter un micronoyau. La solution proposée s'appuie sur une modélisation du comportement attendu des classes fonctionnelles en absence de faute, à partir de laquelle il est possible de définir un ensemble de prédicats. Nous appliquons cette approche aux classes de synchronisation et d'ordonnancement de tâches. Pour mettre en ¿uvre ces prédicats, nous introduisons un mécanisme d'encapsulation original, basé sur la notion de réflexivité. Ce concept est illustré sur le micronoyau Chorus/ClassiX. Enfin, nous utilisons MAFALDA pour évaluer de façon objective les bénéfices procurés par les mécanismes d'encapsulation.

Abstract

The use of commercial microkernels appears today as an increasingly attractive design opportunity in many application fields, including dependable systems. The objective of the work presented in this dissertation is to provide answers to the questions raised by this new trend. We develop a method for the evaluation and the improvement of the dependability properties of commercial microkernels. First, we justify the suitability of software implemented fault injection for characterizing the failure modes of a microkernel. We present the guidelines that have led to the tool MAFALDA: Microkernel Assessment by Fault Injection Analysis for Design Aid. Then, MAFALDA is applied to a typical commercial microkernel: Chorus/ClassiX. Lessons learnt from these experiments and means to improve dependability properties of this microkernel are discussed. These could benefit both microkernel providers and dependable system developers. Then, we develop a novel approach to contain the effect of both external and internal errors that may affect the microkernel. The proposed solution relies on the modeling of the expected behavior of the functional classes in the absence of fault, which allows for the definition of dynamic predicates. This approach is exemplified on the synchronization and task scheduling classes. To implement such predicates, we introduce an original wrapping approach, based on reflection. This concept is illustrated on Chorus/ClassiX. Finally, we use MAFALDA to objectively evaluate the actual benefits procured by the proposed wrappers.

Mots-Clés / Keywords

Metakernel; Reflection; Wrapping; Error confinement; Fault injection; Microkernel; Commercial Off The Shelf (COTS) software; Métanoyau; Réflexivité; Encapsulation; Confinement d'erreur; Injection de fautes; Micronoyau; Logiciel COTS "Commercial Off The Shelf";

Résumé

La sécurité et la disponibilité sont deux attributs de la sûreté de fonctionnement auxquels l'on doit apporter des solutions viables dans les systèmes de contrôle-commande critiques. Assurer simultanément la disponibilité et la sécurité est parfois difficile. En effet, l'introduction de redondances pour accroître la disponibilité peut être à l'origine de problèmes de sécurité qui n'auraient pas existé dans un système sans redondance. Les travaux présentés dans ce mémoire portent sur la gestion des redondances dans un système critique afin d'accroître sa disponibilité sans compromettre la sécurité. Il s'agit principalement de la gestion des redondances de façon transparente aux modules d'application tout en assurant la conservation des propriétés de sécurité de ces derniers. Après avoir montré que l'incohérence des contextes des éléments répliqués peut être à l'origine de la non conservation des propriétés de sécurité, nous proposons une technique visant à tolérer les incohérences de contexte. Cette technique consiste à détecter les incohérences potentielles afin de mettre le système dans une configuration où il ne compromet pas la sécurité en cas d'incohérence réelle. En nous appuyant sur le modèle asynchrone temporisé, nous proposons deux mécanismes de gestion de redondance mettant en ¿uvre cette technique, respectivement pour les redondances duplex et les redondances n-plex (n ¿ 3). A titre d'illustration, nous appliquons ces deux mécanismes au pilotage de lignes de métro automatisées. En particulier, nous montrons que ces deux mécanismes permettent de décharger les programmeurs du niveau application de la gestion de la répartition et des redondances. De cette façon, ils induisent une réduction substantielle des coûts associés au développement et à la validation des systèmes critiques.

Abstract

Safety and availability are issues of major importance in dependable critical systems. Ensuring simultaneously both attributes is sometimes difficult. Indeed, the introduction of redundancy to increase the overall system availability can lead to safety problems that would not otherwise exist. The work presented in this thesis deals with redundancy management in critical systems in order to increase the system availability without jeopardising its safety. We show that inconsistency of replicated component contexts can lead to safety problems even if each component (taken individually) is safe. We propose a technique to tolerate context inconsistency. This technique consists in detecting potential inconsistencies and switching the system to a configuration that does not compromise safety in case of a real inconsistency. Using the timed asynchronous model, we have designed two mechanisms that implement this technique for redundancy management in critical systems, respectively for duplex and n-plex (n ¿ 3) redundancy. As an illustration, both mechanisms have been applied to a fully automated subway control system. In particular, we provide a design paradigm enabling an implementation of both mechanisms independently from the application layer. This paradigm induces a substantial reduction of the cost of designing and validating critical systems.

Mots-Clés / Keywords

Railway control; Fail-safe systems; Critical systems; Fail-awareness; Timed asynchronous model; Availability; Safety; Redundancy; Fault tolerance; Commande ferroviaire; Systèmes critiques; Service sûr en présence de faute; Modèle asynchrone temporisé; Disponibilité; Sécurité; Gestion des redondances; Tolérance aux fautes;

Résumé

Cette thèse présente une méthode générale de spécification et d'évaluation quantitative de la sécurité des systèmes d'information. Cette méthode offre l'opportunité de surveiller les évolutions d'un système d'information pendant sa vie opérationnelle, ainsi que de comparer l'impact sur la sécurité de modifications éventuelles du fonctionnement. Elle s'appuie sur une spécification formelle de la politique de sécurité, complétée par un modèle des vulnérabilités du système réel en fonctionnement. Une mesure de la sécurité correspond alors à la difficulté pour un attaquant potentiel d'exploiter les vulnérabilités pour mettre en défaut les objectifs définis par la politique de sécurité. La spécification de la politique de sécurité d'un système d'information nécessite la définition d'un cadre rigoureux, expressif, et suffisamment général pour être utilisable dans le contexte d'une organisation. La méthode définie et utilisée dans ce mémoire est basée sur une extension de la logique déontique, complétée par une représentation graphique. Les vulnérabilités du système d'information sont représentées par un modèle appelé un graphe des privilèges. Ces vulnérabilités, qui doivent être recherchées dans le système, peuvent avoir des origines variées, comme la mauvaise utilisation des mécanismes de protection dans un système informatique, ou les délégations de pouvoirs dans une organisation. L'attribution d'un poids à ces vulnérabilités élémentaires permet de définir des mesures quantitatives de la sécurité globales et pertinentes. La démarche est illustrée par deux exemples d'application pratique : l'étude du fonctionnement d'une agence bancaire de taille moyenne ; et l'observation de l'évolution de la sécurité d'un système informatique de grande taille en exploitation.

Abstract

This dissertation presents a general method for the specification and quantitative evaluation of information systems security. This method allows to monitor the evolutions of an information system in operation, as well as to compare the impact on security of possible modifications of the functioning. It relies on a formal specification of the system security policy, augmented by a model of the vulnerabilities observed in the real system in operation. Then, a security measure represents the difficulty for an attacker to exploit the vulnerabilities and defeat the objectives defined in the security policy. Information systems security policy specification necessitates the definition of a rigorous and expressive framework. Furthermore, the language should be general enough to be usable in the context of an organization. The method defined and used in this work is based on an extension of deontic logic, enriched with a graphical representation. Vulnerabilities of the information system are described by a model called a privilege graph. These vulnerabilities, probed in the system, may have various origins, such as incorrect operation of the protection mechanisms of a computer system, or delegation of privileges in an organization. The assessment of a weight to these individual vulnerabilities allows the definition of accurate and global quantitative measures of security. Two practical examples are presented to illustrate the methodology : the study of a medium-size bank agency ; and the observation of the security evolutions of a large computer system in operation.

Mots-Clés / Keywords

Privilege graph; Information system; Quantitative evaluation; Security policy; Security; Dependability; Graphe des privilèges; Système d'information; Evaluation quantitative; Politique de sécurité; Sécurité; Sûreté de fonctionnement;

Résumé

Les travaux présentés dans ce mémoire concernent la vérification expérimentale de la tolérance aux fautes au plus tôt dans le processus de développement de systèmes informatiques critiques. Ce mémoire expose tout d'abord une synthèse des travaux menés sur la validation de la tolérance aux fautes, et porte plus particulièrement son attention sur l'injection de fautes en tant que technique privilégiée de test de la tolérance aux fautes. On justifie ainsi le choix de l'approche de simulation pour la vérification expérimentale de la tolérance aux fautes. Ce mémoire propose ensuite une caractérisation des attributs de l'injection de fautes dans le contexte de l'élimination des fautes de conception dans les mécanismes de tolérance aux fautes. Le profil de test (fautes et activités) est différent du profil opérationnel et vise à favoriser la sensibilisation des différents mécanismes. Les relevés d'expériences sont des prédicats sur les sorties du système, sur les mécanismes de tolérance aux fautes et sur leurs états internes. Ces relevés visent d'abord à décider de l'issue du test, ensuite à fournir des données utiles au diagnostic. La technique de test proposée est construite d'une part à partir d'une modélisation fonctionnelle globale de la tolérance aux fautes et de ses interactions, d'autre part à partir d'une modélisation comportementale de chaque mécanisme individuel de tolérance aux fautes. L'approche proposée privilégie le test statistique pour sa capacité à dépasser les limites des critères de test usuels. Ces travaux s'appuient d'abord sur le développement d'un outil d'injection de fautes dans des modèles de simulation VHDL : MEFISTO. Ils s'appuient ensuite sur une plate-forme expérimentale simulant un système tolérant aux fautes. Elle est développée en VHDL et est utilisée pour illustrer notre méthode de test statistique des mécanismes de tolérance aux fautes.

Abstract

This dissertation addresses the experimental verification of fault tolerance during the early steps of the development process of critical computing systems. First, we present a state-of-the-art of the validation of fault tolerance, with a particular emphasis on fault injection as a privileged technique for fault tolerance testing. The choice of the simulation-based approach is justified for the experimental verification of fault tolerance. We then propose a characterization of the fault injection attributes in the context of removal of fault tolerance deficiency faults. The testing profile (faults and activities) is different from an operational profile and aims at favouring sensitization of the different mechanisms. Experimental readouts are predicates on the outputs of the system, on the fault tolerance mechanisms and on their internal states. These readouts aim first at deciding the outcome of the test, and second at providing useful data for diagnosis. The proposed technique is built up on a functional modelling of the overall fault tolerance and its interactions on one hand, and on a behavioural modelling of each individual fault tolerance mechanism on the other hand. The proposed approach focuses on statistical testing as a means to surpass the limits of prevailing testing criteria. This work involves first the development of a tool for VHDL simulation-based fault injection: MEFISTO. It also involves the development of an experimental platform simulating a fault-tolerant system. This platform, written in VHDL, is used for illustrating our method for statistical testing of fault tolerance mechanisms.

Mots-Clés / Keywords

Statistical testing; Fault tolerance modeling; Fault injection; Dependability; Simulation VHDL; Test statistique; Modélisation de la tolérance aux fautes; Injection de fautes; Verification; Sûreté de fonctionnement; VHDL-based simulation;

Résumé

Les travaux présentés dans ce mémoire concernent la spécification et la construction des modèles de sûreté de fonctionnement des systèmes informatiques tolérant les fautes, impliquant de nombreux composants matériels et logiciels aux interactions multiples et des procédures complexes de tolérance aux fautes et de restauration, afin d'évaluer de mesures définies par rapport à plusieurs niveaux de dégradation du service. Nous avons défini une méthode de construction modulaire et incrémentale qui permet, d'une manière systématique, la construction et la validation progressive du modèle de sûreté de fonctionnement d'un système, par les réseaux de Petri stochastiques généralisés (RdPSG). Cette méthode est basée sur deux idées originales : l'approche incrémentale de construction, qui consiste à construire et en même temps à valider progressivement un modèle, et le système de règles de construction modulaire, conçues de façon à aboutir à une forme optimale du modèle par RdPSG et de faciliter sa validation progressive. Afin de faciliter sa mise en oeuvre, nous avons complété cette méthode par un formalisme de spécification de haut niveau, graphique et textuel, dont l'objectif est de décrire de façon structurée le comportement des composants et de leurs interactions en présence des défaillances. Le formalisme permet de spécifier de manière incrémentale la construction optimale d'un modèle RdPSG, tout en respectant les règles définies au sein de la méthode. Des règles de transformation ont été définies afin de permettre la génération automatique d'un modèle RdPSG par traduction directe des éléments du formalisme. Nous avons appliqué cette approche de spécification et construction à la modélisation du système informatique CAUTRA (Coordonnateur AUtomatisé du TRafic Aérien), en vue d'évaluer des mesures de sûreté de fonctionnement spécifiques, traduisant l'impact des défaillances et des procédures de restauration utilisées sur la sécurité du trafic. L'évaluation a permis d'effectuer des choix d'architecture, de stratégies de tolérance aux fautes et de procédures d'exploitation.

Abstract

This thesis is concerned with the specification and construction of dependability models of fault-tolerant computing systems with a large number of hardware and software components involving multiple interactions and complex fault-tolerance and restoration procedures. The modeling allows to evaluate measures defined with respect to several levels of service degradation. We defined a modular and incremental construction method which allows the systematic and progressive building and validation of a dependability model, using the Generalized Stochastic Petri Nets (GSPN). This method is based on two original ideas : an incremental construction approach which consists in progressively building up and validating the model and a set of modular construction rules, conceived to develop an optimal model while facilitating its validation. In order to ease its application, this method was further completed with a high-level specification formalism. The formalism combines graphics and text in order to describe in a structured manner the components behavior and their interactions in presence of failures. This formalism allows to incrementally specify the construction of a GSPN model and is coherent with the modular construction rules. We defined transformation rules in order to allow the GSPN generation by directly translating the elements of the specification formalism. This approach was applied to the modeling of the CAUTRA French air traffic control computing system, in order to evaluate specific dependability measures reflecting the impact of the system failures and of its restoration procedures on the air traffic safety. The evaluation of these measures led to optimal choices for the system architecture, fault-tolerance strategies and operating procedures.

Mots-Clés / Keywords

Impact sur la sécurité du trafic; Contrôle du trafic aérien; Formalisme de spécification; Interactions; Réseaux de Petri stochastiques généralisés; Sûreté de fonctionnement; Composants matériels et logiciels; Modélisation modulaire et incrémentale; Dependability; Generalized Stochastic Petri Nets; Modular and incremental modelling; Hardware and software components; Specification formalisme; Air traffic control; Impact on air traffic safety;

Résumé

Les notions de langages à objets réflexifs et de protocoles à métaobjets permettent d'intégrer élégamment dans des applications des propriétés indépendantes de leurs fonctionnalités. Ces notions offrent de nouvelles perspectives pour la réalisation de systèmes répartis tolérant les fautes. Les métaobjets peuvent en effet contrôler l'exécution des objets d'une application, par exemple selon une stratégie de réplication, de manière transparente pour l'application. La thèse propose une architecture à métaobjets, Friends, dans laquelle les métaobjets ont été utilisés en conjonction avec un minimum de services systèmes spécialisés pour réaliser des mécanismes de tolérance aux fautes, de communication de groupe et de sécurité des communications. La composition de mécanismes repose sur une approche originale où les métaobjets sont utilisés de manière récursive, ce qui permet en outre de simplifier la conception des mécanismes, chacun pouvant être conçu séparément des autres propriétés. Une méthode de conception par objets a été utilisée pour concevoir les métaobjets et a permis de développer une hiérarchie de classes pour la tolérance aux fautes, incluant des mécanismes de réplication et à base de support stable. Grâce à l'approche présentée, les métaobjets peuvent être facilement composés au cas par cas suivant les propriétés requises par l'application. Deux prototypes ont été réalisés, tout d'abord pour valider l'approche, mais aussi pour en analyser les avantages, les limites et les performances.

Abstract

The notions of reflective languages and metaobject protocols provides an elegant integration to applications of properties that are independent from their functionalities. Such notions provide a promising framework for the implementation of fault tolerant distributed systems. Metaobjects can control the execution of application objects transparently for the application, for example according to a given replication strategy. The thesis proposes a metaobject architecture, Friends, in which metaobjects are used with a minimum number of system services to implement mechanisms for fault tolerance, group-based communications and communication security. The composition of mechanisms relies on an original approach where metaobjects are used in a recursive way, which simplifies the design of the mechanisms, each one being designed separately from the other properties. An object-oriented design method was used for the design of the metaobjects and allowed the development of a class hierarchy for fault-tolerance, providing mechanisms based on replication or the use of a stable storage. Thanks to the approach described here, metaobjects can be composed easily on a case-by-case basis according to the application requirements. Two prototypes were implemented in order to validate the approach and also to analyse its advantages, limits and performances.

Mots-Clés / Keywords

Conception par objets; Techniques à objets; Réflexivité; Protocole à métaobjets; Systèmes répartis; Tolérance aux fautes; Sûreté de fonctionnement informatique; Reuse; Réutilisation; Object-oriented design; Object-oriented technology; Metaobject protocols; Reflection; Distributed systems; Fault tolerance; Dependability;