Dans le domaine de l’aéronautique, les systèmes embarqués ont fait leur apparition durant les années 60, lorsque les équipements analogiques ont commencé à être remplacés par leurs équivalents numériques. Dès lors, l’engouement suscité par les progrès de l’informatique fut tel que de plus en plus de fonctionnalités ont été numérisées. L’accroissement permanent de la complexité des systèmes a conduit à la définition d’une architecture appelée Avionique Modulaire Intégrée (IMA pour Integrated Modular Avionics). Cette architecture se distingue des architectures antérieures, car elle est fondée sur des standards (ARINC 653 et ARINC 664 partie 7) permettant le partage des ressources de calcul et de communication entre les différentes fonctions avioniques. Ce type d’architecture est appliqué aussi bien dans le domaine civil avec le Boeing B777 et l’Airbus A380, que dans le domaine militaire avec le Rafale ou encore l’A400M. Pour des raisons de sûreté, le comportement temporel d’un système s’appuyant sur une architecture IMA doit être prévisible. Ce besoin se traduit par un ensemble d’exigences temps réel que doit satisfaire le système. Le problème exploré dans cette thèse concerne la vérification d’exigences temps réel dans les systèmes IMA. Ces exigences s’articulent autour de chaînes fonctionnelles, qui sont des séquences de fonctions. Une exigence spécifie alors une borne acceptable (minimale ou maximale) pour une propriété temporelle d’une ou plusieurs chaînes fonctionnelles. Nous avons identifié trois catégories d’exigences temps réel, que nous considérons pertinentes vis-à-vis des systèmes étudiés. Il s’agit des exigences de latence, de fraîcheur et de cohérence. Nous proposons une modélisation des systèmes IMA, et des exigences qu’ils doivent satisfaire, dans le formalisme du tagged signal model. Nous montrons alors comment, à partir de ce modèle, nous pouvons générer pour chaque exigence un programme linéaire mixte, c’est-à-dire contenant à la fois des variables entières et réelles, dont la solution optimale permet de vérifier la satisfaction de l’exigence / Embedded systems appeared in aeronautics during the 60’s, when the process of replacing analog devices by their digital counterpart started. From that time, the broad thrust of computer science advances make it possible to digitize more and more avionics functionalities. The continual increase of the complexity of these systems led to the definition of a new architecture called Integrated Modular Avionics (IMA). This architecture stands apart from previous architecture because it is based on standards (ARINC 653 and ARINC 664 part 7) which allow the sharing of computation and communication resources among avionics functions. This architecture is implemented in civil aircrafts, with Boeing B777 and Airbus A380, and in military aircrafts, with Rafale or A400M. For safety reason, the temporal behaviour of such a system must be predictable, which is expressed with a set real-time requirements. A real-time requirement specifies an upper or lower bound of a temporal property of one or several functional chains. A functional chain is a sequence of functions. In this thesis, we explore the verification of real-time requirements in IMA systems. We have identified three real-time requirements relevant to our problem : latency, freshness and consistency. We propose a model of IMA systems, and the requirements they must meet, based on the tagged signal model. Then we derive from this model, for each requirement, a mixed integer linear program whose optimal solution allows us to verify the requirement

Les systèmes industriels recouvrent de nombreuses formes. Aujourd'hui, ils sont le plus souvent organisés en réseaux. Les nouvelles technologies de l'information et de la communication apportent un ensemble de moyens supplémentaires pour réaliser des applications ayant un intérêt majeur pour renforcer l'exploitation sûre de ces systèmes et la sécurité des personnes.Parmi ces systèmes industriels, on peut citer les systèmes cyber-physiques (CPS) caractérisés par un grand nombre de variables, des non linéarités et des incertitudes. Leur décomposition en sous-systèmes, permet de les rendre plus facilement gérables et organisés de façon hiérarchique, est fondamentale. Chacun des sous-systèmes est constitué de différents composants remplaçables interconnectés qui réalisent différentes fonctions.Dans cette optique, nous proposons une approche de diagnostic basée sur quatre types de connaissances : fonctionnelle, structurelle, topologique et comportementale.Cette approche qui inclut la détection et la localisation, exploite la représentation des différentes connaissances pour détecter et isoler la source de défaillance. Afin de lever toute ambigüité de localisation, l’adjonction d’un automate temporisé permet, grâce à une analyse temporelle, d’identifier efficacement le ou les composants défectueux. L’approche multimodèle proposée est agencée autour de trois algorithmes.La modélisation et d’analyse des défaillances est illustrée sur un système cyber-physique : le robot de téléprésence "RobAIR". Les différents modèles de connaissances ont été établis avec une démarche d’analyse ainsi que la construction du diagnostiqueur basée sur des signatures préalablement définies.L‘implémentation des algorithmes de détection, d’isolation sous Simulink/ Stateflow de Matlab a permis de construire le diagnostiqueur selon la méthodologie proposée et valider ainsi notre approche par simulation du fonctionnement avec injection de façon aléatoire de différentes défaillances.La méthode d’analyse proposée a été appliquée aux tests de démarrage du robot RobAIR avec une attention particulière sur la partie déplacement. Le test de l’ensemble des fonctionnalités du robot est réalisé par la programmation de la carte Arduino. Pour cette application, les algorithmes de détection et d’isolation ont été complétés par la détection d’obstacle et l’identification du mode défaillance. / Industrial systems cover many forms. Today, they are most often organized in networks. The new information and communication technologies provide a set of additional means to realize applications of major interest to strengthen the safe operation of these systems and the safety of people.Among these industrial systems, we can cite cyber-physical systems (CPS) characterized by a large number of variables, nonlinearities and uncertainties. Their decomposition into subsystems, making them more manageable and hierarchically organized, is fundamental. Each of the subsystems consists of different interconnected replaceable components that perform different functions.With this in mind, we propose a diagnostic approach based on four types of knowledge: functional, structural, topological and behavioral.This approach, which includes detection and localization, exploits the representation of different knowledge to detect and isolate the source of failure. In order to eliminate any ambiguity of location, the addition of a timed automat allows, thanks to a temporal analysis, to efficiently identify the defective component(s). The proposed multimodel approach is organized around three algorithms.Modeling and failure analysis is illustrated on a cyber-physical system: the "RobAIR" telepresence robot. The different knowledge models were established with an analysis approach as well as the construction of the diagnostician based on previously defined signaturesThe implementation of Matlab's Simulink / Stateflow isolation and detection algorithms made it possible to build the diagnoser according to the proposed methodology and thus validate our approach by simulating the operation with random injection of various failures.The proposed analysis method was applied to the RobaIR robot's start-up tests with particular attention to the displacement part. The testing of all the robot's functionalities is done by programming the Arduino board. For this application, the detection and isolation algorithms have been supplemented by obstacle detection and failure mode identification.

Notre objectif est de proposer une méthodologie pour le développement d'un intergiciel embarqué dans l'automobile offrant des services de communication aux applications. Le cadre d'utilisation de nos travaux est la conception de systèmes embarqués dans les véhicules. Ces applications requièrent un intergiciel capable de fournir des services standards de communication, qui cachent la localisation des participants aux échanges, qui masquent l'hétérogénéité des plates-formes de communication, et qui garantissent le respect des contraintes temporelles imposées sur l'échanges et sur l'exécution des participants. La méthodologie proposée vise la conception d'un intergiciel optimisé et pour cela aborde deux aspects : la spécification d'une architecture d'implémentation, et la construction d'une configuration faisable. L'architecture d'implémentation est optimisée dans le sens où l'intergiciel est adapté à l'environnement d'exécution (le système d'exploitation OSEK/VDX OS), et minimise son utilisation des ressources disponibles. Elle apporte une réponse, d'une part, au niveau de la spécification d'une architecture logicielle (construite à l'aide de design patterns ), et, d'autre part, à la manière dont cette architecture est déployée sur une plate-forme concrète (sous la forme d'un ensemble de tâches). La procédure proposée pour la construction de la configuration de l'intergiciel calcule les caractéristiques temporelles faisables de l'intergiciel et des trames émises par les stations d'un réseau CAN. Elle prévoit aussi une étape pour le calcul d'une allocation de priorités faisable pour les tâches de l'application sur chaque station. L'optimalité de la configuration est atteinte en assurant le respect de toutes les contraintes temporelles imposées sur les échanges et sur l'exécution des tâches de l'application et de l'intergiciel. / Our objective is to propose a methodology for the development of an automotive embedded middleware that provides communication services to the applicative level software. This work is focused on the design of automotive functions, where the nowadays context demands a middleware capable of offering standard communication services, hiding the localization of the participants in the exchanges, masking the heterogeneity of communication platforms, and ensuring that the timing constraints imposed on the exchanges and on the execution of the participants are met. The proposed methodology is aimed for the design of an optimised middleware. For this purpose, it deals with two topics: the specification of an implementation architecture, and the construction of a feasible configuration. The implementation architecture is optimised because the middleware is well adapted to its execution environment (operating system OSEK/VDX OS), and minimizes the utilization of the available resources. It contributes, on the one hand, to a specification of a software architecture (built using design patterns), and, on the other hand, to mechanisms allowing to deploy this software architecture onto a concrete platform (under the form of a set of tasks). The algorithm proposed for the construction of a configuration determines feasible timing characteristics for the middleware and for the frames exchanged over a CAN bus. It covers also the calculation of a feasible set of priorities for the applicative tasks executing on each station of the bus. The correctness of the configuration is achieved by ensuring that the timing constraints imposed on the exchanges and on the execution of the applicative and middleware tasks are met.

Durant la dernière décennie, la miniaturisation des technologies de semi-conducteurs et de l’intégration à grande échelle a donné lieu à la conception de systèmes complexes, notamment l’intégration de plusieurs milliards de transistors sur un même die. Cette tendance pose de nombreux défis de fabrication et de fiabilité tels que la dissipation de puissance, la variabilité technologique et la polyvalence des applications. Les problèmes de fiabilité, représentées par la présence de points chauds thermiques peuvent accélérer la dégradation des transistors, et par conséquent réduire la durée de vie des puces, également appelée "vieillissement". Afin de relever ces défis, de nouvelles solutions sont nécessaires, basées notamment sur des systèmes auto-adaptatifs. Ces systèmes sont principalement composées d’une boucle de contrôle avec trois processus : (i) la surveillance, qui est chargée d’observer l’état du système, (ii) la prise de décision, qui analyse les informations collectées et prend des décisions pour optimiser le comportement du système et (iii) l’action qui ajuste les paramètres du système en conséquence. Cependant, une adaptation dépendre de façon critique sur le processus de suivi qui devrait fournir une estimation précise sur l’état du système de façon rentable. Dans cette thèse, nous étudions d’abord le suivi de la consommation d’énergie. Nous développons une méthode basée sur plusieurs algorithmes de fouille de données "data mining", pour surveiller l’activité de commutation sur quelques signaux pertinents sélectionnés au niveau RTL. La méthode proposée se compose d’un flot générique qui peut être utilisé pour modéliser la consommation d’énergie pour n’importe quel circuit RTL sur n’importe quelle technologie. Deuxièmement, nous améliorons le flot proposé pour estimer le comportement thermique globale de puce et de développer une nouvelle technique de placement des capteurs thermique sur puce. Les algorithmes proposés choisissent systématiquement le meilleur compromis entre la précision de l’observation et le coût représenté par le nombre de capteurs intégrés sur puce. La surface de la puce est décomposée en plusieurs zones thermiquement homogènes.Outre la partie conception, les systèmes embarqués modernes intègrent des capteurs matériels (analogiques ou numériques) qui peuvent être utilisés pour surveiller l’état du système. Ces méthodes industrielles sont généralement très coûteuses et nécessitent un grand nombre d’unités pour produire des informations précises avec une résolution à grain fin. Une solution alternative pour fournir une estimation précise de l’état du système est réalisée avec un ensemble de compteurs de performance qui peut être configuré pour effectuer le suivi des événements logiques à différents niveaux. Dans ce cas, nous proposons un nouvel algorithme pour la sélection des événements performance pertinents à partir des ressources locales, partagées et système. Nous proposons ensuite une implémentation d'un algorithme d'estimation basé sur un réseau neuronal. La méthode proposée est robuste contre les variations de température extérieure. En outre, estimation thermique est aussi peut être réalisé en utilisant les événements logiques actuelles et historiques, et la précision est évaluée sur la base de la profondeur dans le passé.Enfin, une fois la méthode de suivi et la cible définies et le système est configuré, la méthode de surveillance doit être utilisée au moment de "Run-time". Nous avons mis en place une boucle d’adaptation complète, avec un suivi dynamique de l’état du système afin atteindre une meilleure efficacité énergétique. / Over the last decade, the miniaturization of semiconductor technologies and the large-scale integration has given rise to complex system design, including the integration of several billions of transistors on a single die. This trend poses many manufacturing and reliability challenges such as power dissipation, technological variability and application versatility. The reliability issues represented by the presence of thermal hotspots can accelerate the degradation of the transistors, and consequently reduce the chip lifetime, also referred to as “aging”. In order to address these challenges, new solutions are required, based in particular on self-adaptive systems. Such systems are mainly composed of a control loop with three processes: (i) the monitoring, which is responsible for observing the state of the system, (ii) the diagnosis, which analyzes the information collected and makes decisions to optimize the behavior of the system, and (iii) the action that adjusts the system parameters accordingly. However, effective adaptations depend critically on the monitoring process that should provide an accurate estimation about the system state in a cost-effective manner. In this thesis, we firstly investigate the monitoring of the power consumption. We develop a method, based on several data mining algorithm, to monitor the toggling activity on a few relevant signals selected at the RTL level. The proposed method consists of a generic flow that can be used to model the power consumption for any RTL circuit on any technology. Secondly, we improve the proposed flow by estimating the overall chip thermal behavior and developing a new technique of on-die thermal sensor placement. The proposed algorithms systematically choose the best trade-off between accuracy and overhead. The surface of the chip is decomposed into several thermally homogeneous regions.Besides the design part, modern embedded systems integrates hardware sensors (analog or digital) that can be used to monitor the system’s state. These industrial methods are usually very expensive, and require a large number of units to produce precise information at a fine-grained resolution. An alternative solution to provide an accurate estimation of system’s state is achieved with a set of performance counters that can be configured to track logical events at different levels. To this end, we propose a novel algorithm for the selection of the relevant performance events from the local, shared and system resources. We propose then an implementation of a neural network based estimation algorithm. The proposed method is robust against the external temperature variations. Furthermore, thermal estimation is also can be achieved using the current and historic logical events, and the accuracy is evaluated on the basis of the depth in the past.Finally, once the tracking method and target are defined and the system is configured, the monitoring method should be used at “Run-time”. We implemented a complete adaptation loop, with a dynamic monitoring of the system’s state in order to achieve better energy efficiency.

Les calculateurs embarqués dans les automobiles, ou ECU (Electronic Control Unit) sont responsables d’un nombre croissant de fonctionnalités au sein du véhicule. Pour pouvoir coordonner leurs actions, ces calculateurs s’échangent des données via des bus de communication et forment ainsi un véritable réseau embarqué. Si historiquement ce réseau pouvait être considéré comme un système fermé, l’apparition de nombreux moyens de communication dans les automobiles a ouvert ce réseau au monde extérieur et fait émerger de nombreuses problématiques de sécurité dans ce domaine.Nos travaux s’inscrivent dans une démarche de mise en place de moyens de sécurité-immunité dans les réseaux automobiles. La thématique de la sécurité-immunité dans l’automobile étant un sujet relativement récent, un effort particulier a été apporté à la définition du contexte. Ainsi, dans ce manuscrit, nous décrivons les menaces qui peuvent cibler ces systèmes embarqués, proposons une classification des scénarios d’attaques puis présentons les différents mécanismes de sécurité pouvant être appliqués aux systèmes embarqués d’une automobile.Ensuite, afin de compléter les mesures de sécurité préventives mises en place pour empêcher un attaquant de pénétrer au coeur du réseau embarqué, nous proposons dans cette thèse un système de détection d’intrusion pour les réseaux automobiles embarqués. Celui-ci, conçu à partir des spécifications du ou des systèmes à surveiller, intègre notamment des mécanismes permettant d’effectuer une corrélation des messages observés sur le réseau afin d’identifier des séquences de messages suspectes. Après avoir décrit formellement le fonctionnement de notre système de détection, nous présentons de premières expérimentations visant à valider notre méthode et à évaluer ses performances. / In today’s automobiles, embedded computers, or ECUs (Electronic Control Units) are responsible for an increasing number of features in a vehicle. In order to coordinate their actions, these computers are able to exchange data over communication buses, effectively constituting an embedded network. While this network could previously be considered a closed system, the addition of means of communication in automobiles has opened this network to the outside world, thus raising many security issues.Our research work focuses on these issues and aims at proposing efficient architectural security mechanisms for protecting embedded automotive networks. The security of embedded automotive systems being a relatively recent topic, we first put a strong focus on defining the context. For that purpose, we describe the threats that can target a car’s embedded systems, provide a classification of the possible attack scenarios and present a survey of protection mechanisms in embedded automotive networks.Then, in order to complement the preventive security means that aim at stopping an attacker from entering the embedded network, we introduce an Intrusion Detection System (IDS) fit for vehicular networks. Leveraging the high predictability of embedded automotive systems, we use language theory to elaborate a set of attack signatures derived from behavioral models of the automotive calculators in order to detect a malicious sequence of messages transiting through the internal network. After a formal description of our IDS, we present a first batch of experiments aimed at validating our approach and assessing its performances.

Le développement rapide des systèmes embarqués et les exigences croissantes auxquelles ils sont soumis créent un besoin de techniques innovantes en terme de conception, de vérification et de validation. Les méthodes formelles fournissent des approches intéressantes à la conception de ces systèmes, notamment pour des études de sûreté de fonctionnement (SdF). Le formalisme choisi est basé sur les Réseaux de Petri Colorés (RdPC). L'avantage de ces modèles, en plus d'être très expressifs et formels, est qu'ils permettent d'exprimer le double caractère des systèmes étudiés : statique et dynamique. Le défi relevé par cette thèse est d'utiliser des modèles établis, décrivant l'architecture et/ou le comportement de systèmes, pour en extraire des informations de SdF en général et de diagnostic de défaillances en particulier. L'approche proposée est une analyse structurelle par accessibilité arrière de RdPC. Elle peut être décomposée en deux parties. La première consiste en la proposition d'un outil pour réaliser cette analyse : le RdPC inverse. Il est obtenu grâce à l'application de transformations structurelles sur le RdPC original. La seconde partie est la mise en \oe uvre de l'analyse. Cette partie requiert des mécanismes complémentaires dont le plus important est l'enrichissement du marquage. L'approche proposée est étudiée de deux points de vue complémentaires : algorithmique et théorique. Le point de vue algorithmique consiste à proposer des modèles de transformations pour l'inversion des RdPC et la mise en \oe uvre de l'analyse. L'aspect théorique vise à offrir une base formelle à l'approche en appliquant deux méthodes (l'algèbre linéaire et la logique linéaire) pour prouver notre approche.

Ce manuscrit présente une méthode de contrôle de qualité de service à grain fin d'applications multimédia. Celle-ci permet le contrôle d'applications dont les actions sont paramétrées par des niveaux de qualité et dont les durées d'exécution ne sont pas connues. Le contrôle consiste en la construction d'un ordonnancement et le choix des niveaux de qualité respectant des propriétés de sûreté et d'optimalité. C'est-à-dire que l'on cherche à maximiser l'utilisation du budget de temps sans pour autant le dépasser tout en ayant un choix de qualité régulier. Le contrôleur utilise une politique de gestion de qualité permettant de choisir pour chaque action l'ordonnancement et le niveau de qualité respectant les contraintes de qualité de service. Nous étendons et améliorons les résultats précédents dans deux directions. La première propose une approche symbolique de la politique de gestion de qualité. Celle-ci utilise un diagramme de vitesses qui est une représentation graphique du comportement de l'application contrôlée. À partir de cette représentation, nous avons proposé une technique de contrôle permettant de relâcher le nombre d'appels au contrôleur tout en respectant les propriétés de sûreté et d'optimalité. Nous avons ensuite proposé une approche stochastique du problème basée sur des fonctions de distribution de probabilités pour les durées d'exécution des actions. Notre méthode donne la possibilité à l'utilisateur de fixer la criticité des contraintes temps-réel. Elle permet aussi de calculer à priori le taux attendu de dépassement des échéances. Ces résultats théoriques ont été appuyés par des expériences réalisées sur un encodeur vidéo s'exécutant sur machine nue.

L'évolution actuelle de l'informatique conduit à un environnement composé d'un grand nombre de petits dispositifs spécialisés, servant les individus. Mark Weiser, le pionnier de l'informatique ubiquitaire, dépeint cette vision du monde informatique au début des années 90 [Wei91], qu'il définit ainsi, à l'inverse de la réalité virtuelle : “la réalité virtuelle mets les gens au coeur d'un monde généré par l'ordinateur, alors que l'informatique ubiquitaire force l'ordinateur à vivre dans le monde réel des gens.” Dans cette vision, les individus sont entourés d'une pléiade d'objets intelligents. Ces dispositifs communicants sont conscients des individus, à l'écoute de leurs besoins, et ajustent leurs actions en fonction.<br />Le concept d'objet intelligent apparaît dans les années 90, au carrefour de la miniaturisation des composants, des technologies de traitement de l'information et des communications sans fil. Dans cette thèse, nous voyons les objets intelligents comme des dispositifs dotés de capacités d'acquisition de données, de stockage, de traitement et de communication. Les cartes à puce (cartes Java multi-applications, cartes bancaires, cartes SIM, carte d'indenté électronique, etc.), les capteurs surveillant leur environnement (collectant des informations météorologiques, de composition de l'air, de trafic routier, etc.) et les dispositifs embarqués dans des appareils domestiques [BID+99, KOA+99, Wei96] (puce embarquée dans un décodeur de télévision) sont des exemples représentatifs des objets intelligents. Les chercheurs en médecine (projet Smartdust [KKP]) comptent aussi sur les puces pour être inhalées ou ingérées (pour remplacer les radiographies, automatiser la régulation du taux de sucre chez les diabétiques, etc.).<br />Dès lors que les objets intelligents acquièrent et traitent des données, des composants base de données embarqués peuvent être nécessaires. Par exemple, dans [BGS01], des réseaux de capteurs collectant des données environnementales sont comparés à des bases de données distribuées, chaque capteur agissant comme un micro-serveur de données répondant à des requêtes. [MaF02] souligne le besoin d'effectuer des traitements locaux sur les données accumulées, telles que des calculs d'agrégats, pour réduire la quantité de données à émettre et ainsi économiser de l'énergie. De plus, la protection de données contextuelles ou de dossiers portables (comme un dossier médical, un carnet d'adresse, ou un agenda) stockés dans des objets intelligents conduit à embarquer des moteurs d'exécution de requêtes sophistiqués pour éviter de divulguer des informations sensibles [PBV+01]. Ces exemples sont représentatifs du besoin grandissant de composants base de données embarqués.<br />Cette thèse adresse particulièrement l'impact des contraintes relatives aux objets intelligents sur les techniques base de données à embarquer dans les calculateurs. L'introduction est organisée comme suit. La première section de l'introduction met en évidence ces contraintes et motive le besoin de composants base de données embarqués. La section suivante expose les trois contributions majeures de la thèse et la dernière section présente l'organisation de ce résumé.

Ce document est rédigé en vue de l'obtention d'un diplôme d'habilitation à diriger des recherches de l'Université Joseph Fourier de Grenoble. Il présente une synthèse de nos travaux de recherche concernant essentiellement le test hors ligne et la surveillance en fonctionnement des systèmes embarqués. Ces travaux sont conduits au sein du laboratoire TIMA de Grenoble successivement dans les équipes ‘'RIS'' (Reliable Integrated Systems) jusqu'en 2002 et ‘'RMS'' (Reliable Mixed Signal Systems) de 2002 à ce jour.<br />Dans le chapitre introductif, nous définissons les systèmes embarqués et nous présentons les défis scientifiques et techniques qu'induisent leur émergence et leur prolifération rapides. Ensuite, nous posons le problème du test hors ligne et de la surveillance en ligne de ces systèmes. La fin du chapitre situe nos activités dans la discipline du test des systèmes intégrés et présente nos principaux axes de recherche. <br />Dans le chapitre 2, nous présentons nos travaux concernant le test intégré de modules analogiques et mixtes incorporés dans un environnement numérique. La première partie du chapitre est consacrée au développement d'outils de conception assistée par ordinateur pour le test des systèmes analogiques et mixtes alors que la deuxième décrit les techniques d'intégration de test à bas coût que nous avons développées pour les systèmes analogiques et mixtes. <br />Le chapitre 3 concerne les techniques de surveillance en ligne intégrée. Une description rapide du flot de synthèse automatique de systèmes intégrés nous permet de situer nos travaux par rapport aux processus modernes de conception de circuits. Les méthodes de test en ligne non-concurrent, semi-concurrent et concurrent sont ensuite exposées. Nous expliquons les liens que partagent les techniques proposées avec d'autres disciplines de recherche, notamment les travaux sur la détection et l'identification de fautes dans les systèmes automatisés. <br />Le chapitre 4 conclut le mémoire. Nous indiquons aussi quelques perspectives possibles pour nos prochaines activités de recherche. Les pistes qui se dégagent concernent aussi bien la poursuite des travaux déjà engagés que des travaux sur de nouvelles problématiques.

L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l'applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l'angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d'un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d'établir un formalisme permettant la preuve du délai de bout-en-bout lors d'une démarche de développement incrémentale.