L'utilisation de la virtualisation dans le domaine des serveurs d'entreprise est aujourd'hui une méthode courante. La virtualisation est une technique qui permet de faire fonctionner sur une seule machine réelle plusieurs systèmes d'exploitation. Cette technique est train d'être adoptée dans le développement des systèmes embarqués suite à la disponibilité de nouveaux processeurs classiquement destiné à ce domaine. Cependant, il y a une différence de contraintes entre les applications d'entreprise et les applications embarquées, celleci doivent respecter des contraintes de temps-réel en réalisant leurs tâches. Dans nos travaux de recherche nous avons étudié l'impact de la virtualisation sur un système d'exploitation temps-réel. Nous avons mesuré le surcoût et la latence des fonctions internes du système d'exploitation déployé sur une machine virtuelle, et nous les avons comparés à celles du système installé sur une machine réelle. Les résultats ont montré que ces métriques sont plus élevées lorsque la virtualisation est utilisée. Notre analyse a révélé que la puce électronique doit inclure des mécanismes matériels qui assistent le logiciel de contrôle des machines virtuelles afin de réduire le surcoût de la virtualisation, mais il est aussi essentiel de choisir une politique d'allocation des ressources efficace afin de garantir le respect des contraintes de temps-réel demandées par les machines virtuelles. Notre second axe de recherche concerne la transformation d'un modèle de simulation d'un système d'exploitation vers des programmes exécutables sur un système-sur-puce. Cette transformation doit également préserver une caractéristique offerte par ce modèle qui est la facilité de configuration des techniques d'allocation de ressources. Pour transformer le modèle de système d'exploitation nous avons utilisé des techniques de l'ingénierie-dirigée par les modèles. Où dans un premier temps le modèle initiale est transformé vers un autre modèle, ensuite ce second modèle est à son tour transformé automatiquement en un code source. Pour assurer la configuration du système d'exploitation finale nous avons utilisé une librairie placée entre le système d'exploitation et l'application afin d'identifier les besoins de celle-ci en termes de ressources et adapter le système à ces besoins. L'évaluation des performances de la librairie a démontré la viabilité de l'approche. / In the domain of server and mainframe systems, virtualizing a computing system's physical resources to achieve improved sharing and utilization has been well established for decades. Full virtualization of all system resources makes it possible to run multiple guest operating systems on a single physical platform. Recently, the availability of full virtualization on physical platforms that target embedded systems creates new use-cases in the domain of real-time embedded systems. In this dissertation we use an existing “virtual machines monitor” to evaluate the performance of a real-time operating system. We observed that the virtual machine monitor affects the internal overheads and latencies of the guest OS. Our analysis revealed that the hardware mechanisms that allow a virtual machine monitor to provide an efficient way to virtualize the processor, the memory management unit, and the input/output devices, are necessary to limit the overhead of the virtualization. More importantly, the scheduling of virtual machines by the VMM is essential to guarantee the temporal constraints of the system and have to be configured carefully. In a second work and starting from a previous project aiming at allowing a system designer to explore a software-hardware codesign of a solution using high-level simulation models, we proposed a methodology that allows the transformation of a simulation model into a binary executable on a physical platform. The idea is to provide the system designer with the necessary tools to rapidly explore the design space and validate it, and then to generate a configuration that could be used directly on top of a physical platform. We used a model-driven engineering approach to perform a model-to-model transformation to convert the simulation model into an executable model. And we used a middleware able to support a variety of the resources allocation techniques in order to implement the configuration previously selected by the system designer at simulation phase. We proposed a prototype that implements our methodology and validate our concepts. The results of the experiments confirmed the viability of this approach.

Les phases de validation et de vérification (V&V) des systèmes réactifs temps réel critique (de plus en plus complexes) sont très importantes en termes de coût et de temps. Dans ce contexte, toute méthode et outil permettant d'aider à la réalisation des activités de V&V est d'une très grande importance au cours du développement. Le test fonctionnel est le moyen le plus utilisé au cours de ces phases de V&V. Or, les méthodes de test présentent des limites : un test exhaustif est quasiment impossible à réaliser en raison de la taille et de la complexité des systèmes considérés. Dans ce contexte, les enjeux de la maîtrise de l'effort de test (complexité et coût) sont majeurs, mais les exigences de qualité pour ces systèmes sont très grandes. L'effort de test caractérise tout autant l'élaboration des jeux de test que le diagnostic. Dans cette optique, nous avons défini deux méthodologies basées sur les concepts d'analyse de testabilité et les stratégies de test. La première méthodologie permet d'aider à la définition de jeux de test pertinents et à l'analyse de couverture des systèmes réactifs spécifiés dans un formalisme flot de données SCADE dans le contexte AIRBUS. La seconde propose des méthodes d'aide à la vérification (identification de tests pertinents et localisation de composants défectueux au cours diagnostic) de systèmes sur la chaîne d'assemblage finale (FAL) d'un avion AIRBUS.

Cette thèse s'inscrit dans le cadre général de l'utilisation des techniques formelles lors de la phase conceptuelle des systèmes distribués temps-réel, et concerne plus précisément l'extension des pouvoirs d'expression et d'analyse du modèle Réseaux de Petri Temporisés Stochastiques. Ce modèle, qui appartient à la classe des Réseaux de Petri Stochastiques, associe à chaque transition un intervalle de temps, et une distribution de probabilité sur cet intervalle (ceci permet de représenter des caractéristiques temporelles variées et en particulier des contraintes) En ce qui concerne le pouvoir d'expression, nous avons introduit, d'une part, la notion de mémoire temporelle de toutes les sensibilisations (ceci est important pour l'étude des phénomènes de préemption que l'on rencontre dans des algorithmes d'ordonnancement et dans des problèmes de sûreté de fonctionnement) et, d'autre part, plusieurs règles de tir de transitions (en particulier les règles MIN et MAX qui permettent des études des cas pires, aspect important dans les systèmes temps-réels). Les graphes ainsi obtenus ont été également situés par rapport à la référence comportementale que constitue le graphe des classes d'états (obtenu à partir des Réseaux de Petri Temporels). En ce qui concerne le pouvoir d'analyse, nous avons défini le concept d'automate quotient quantifié (concept basé, à la fois, sur la relation d'équivalence de Milner et les règles de réduction de Beizer), qui a deux qualités importantes : il permet, d'une part, d'obtenir des modèles, à la fois qualitatifs et quantitatifs de services de communication ; et, d'autre part, de contrôler les dimensions des modèles à traiter lors de la modélisation d'architectures de communication multicouches. Ce modèle a été appliqué à un exemple industriel, le protocole embarqué temps-réel ARINC 629 CP. L'étude faite a mis en évidence les propriétés temps-réel et de tolérance aux pannes de ce protocole.

Cette thèse se situe dans le domaine des systèmes informatiques temps-réel embarqués, plus particulièrement les logiciels embarqués dans l'automobile pour tous les dispositifs émergents et à venir d'évaluation des systèmes d'aide à la conduite (ADAS) pour les prochaines générations de véhicules. Ce document présente les trois axes principaux des travaux de cette thèse : Le premier axe comprend le développement d'un middleware reconfigurable dynamiquement, SCOOT-R. Le deuxième axe concerne le développement des techniques d'ordonnancement distribuées des opérations SCOOT-R avec un objectif de qualité de service de bout en bout. Finalement, le développement des techniques d'ordonnancement régulé pour l'adaptation du système à des situations de conduite et comportements du conducteur variables. Dans ce cas l'importance des fonctions est adaptée suivant le contexte momentané du système.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique

Les travaux présentés dans cette thèse s’inscrivent dans le cadre du développement logiciel des systèmes temps réel embarqués. Nous définissons dans ce travail une méthodologie nommée DRIM. Cette méthodologie permet de guider le déploiement des applications temps réel sur différents RTOS en suivant la ligne de l’IDM et en assurant le respect des contraintes de temps après le déploiement. L’automatisation de la méthodologie DRIM montre sa capacité à détecter les descriptions non-implémentables de l’application, réalisées au niveau conception, pour un RTOS donné, ce qui présente l’avantage de réduire le temps de mise sur le marché d’une part et de guider l’utilisateur pour un choix approprié de l’RTOS cible d’autre part. / The main purpose of this Phd is to contribute to the software development of real-time embedded systems. We define in this work a methodology named DRIM: Design Refinement toward Implementation Methodology. This methodology aims to guide the deployment of a real-time application on to different RTOS while respecting MDE principals and ensuing that the timing properties are still met after deployment. The automation of DRIM shows its ability to detect non-implementable design models describing the real-time application, on aparticular RTOS, which permits to reduce the time-to-market on the one hand and guide the user to the selection of the appropriate RTOS from the other hand.

Dans cette thèse nous proposons un modèle temporel dans le cadre des machines à états abstraits (ASM). Une extension du langage de spécification ASM est développé qui correspond à ce modéle temporel pour le temps continu. L'extension du langage avec des constructions de temps permet de diminuer la taille de la spécification et donc de réduire la probabilité d'erreurs. La sémantique de l'extension du langage ASM est fournie et prend en compte les définitions des fonctions externes, les valeurs des délais et les choix de résolution des non-déterminismes. Un sous-système de vérification des propriétés exprimées en logique FOTL (FirstOrder Timed Logic) est développé. Un simulateur d'ASMs temporisées est développé et implémenté, il comprend un analyseur syntaxique, un interprète du langage, un sous-système de vérification des propriétés ainsi qu'une interface graphique / In this thesis a temporal model for abstract state machines (ASM) method is pro- posed. An extension of ASM specification language on the base of the proposed temporal model with continuous time is developed. The language extension helps to reduce the size of the specification hence to diminish the probability of an error. The semantics of the extended ASM language is developed which takes into account the definitions of external functions, the values of time delays and the method of non-determinism resolving. A subsystem for verification of user properties in the FOTL language is developed. A simulator prototype for ASMs with time is developed and implemented. It includes the parser of the timed ASM language, the interpreter, the verification subsystem and the graphical user interface

Les systèmes réactifs sont de plus en plus présents dans de nombreux secteurs d´activité tels que l´automobile, les télécommunications et l´aéronautique. Ces systèmes réalisent des tâches complexes qui sont souvent critiques. Au vu des conséquences catastrophiques que pourrait entraîner une défaillance dans ces systèmes, suite à la présence de fautes matérielles (processeurs et média de communication), il est essentiel de prendre en compte la tolérance aux fautes dans leur conception. En outre, plusieurs domaines exigent une évaluation quantitative du comportement de ces systèmes par rapport à l'occurrence et à l'activation des fautes. Afin de concevoir des systèmes sûrs de fonctionnement, j'ai proposé dans cette thèse trois méthodologies de conception basées sur la théorie d'ordonnancement et la redondance active et passive des composants logiciels du système. Ces trois méthodologies permettent de résoudre le problème de la génération automatique de distribution et d'ordonnancements temps réel, fiables et tolérants aux fautes. Ce problème étant NP-difficile, ces trois méthodologies sont basées sur des heuristiques de type ordonnancement de liste. Plus particulièrement, les deux premières méthodologies traitent le problème de la tolérance aux fautes matérielles des processeurs et des media de communication, respectivement pour des architectures à liaisons point-à-point et des architectures à liaison bus. La troisième méthodologie traite le problème de l'évaluation quantitative d'une distribution/ordonnancement en terme de fiabilité à l'aide d'une heuristique bi-critère originale. Ces méthodologies offrent de bonnes performances sur des graphes d'algorithme et d'architecture générés aléatoirement.

Vu le développement important des micro-systèmes, leur utilisation sous forme de nappes dans les systèmes de commande-contrôle critiques est une vraie opportunité. Cela soulève néanmoins des défis, parmi lesquels, la définition d'un système de communication à haut niveau d'intégrité. <br />L'étude que nous avons effectuée sur des réseaux standard montre que les protections classiques à base de codes CRC ne permettent pas d'obtenir le niveau d'intégrité visé. <br />Pour l'atteindre, nous avons proposé une solution originale - fonction de contrôle évolutive - qui tire profit du fait que, pour les systèmes de commande-contrôle envisagés (systèmes à dynamique lente), l'intégrité est à considérer sur un lot de messages et non sur un seul message. La solution proposée a ensuite été validée via des simulations Matlab-Simulink. <br />Le cas d'étude utilisé est celui de systèmes de commande de vol du futur, en vue de pouvoir commander des nappes de milliers de micro-surfaces tels que des micro-spoilers.

Ce travail est consacré à la problématique du suivi des systèmes répartis temps réel. Plus précisément, il se concentre sur les aspects formels de la supervision basée sur des modèles ainsi que sur les problèmes qui lui sont liés. Dans la première partie du travail, nous présentons les propriétés de base de deux modèles formels bien connus utilisés pour la modélisation de systèmes répartis : les réseaux d'automates temporisés et les réseaux de Petri temporels. Nous montrons que le comportement de ces modèles peut être représenté par les procédés dits de branchement. Nous introduisons également les éléments conceptuels clés du système de surveillance. La deuxième partie du travail est consacrée à la question des dépliages avec contraintes qui permettent le suivi des relations causales entre les événements dans un système réparti. Ce type de structure peut reproduire des processus sur la base d'un ensemble totalement non-ordonné d'évènements. Dans notre travail, nous soulevons les problèmes des contraintes de temps et de leurs paramétrages. Les méthodes proposées sont illustrées par des études de cas. La troisième partie du travail traite de la problématique des boucles inobservables qui peuvent résulter de comportements cycliques inobservables des systèmes considérés. Ce type de comportement conduit à un nombre infini d'événements dans les dépliages avec contraintes. La quatrième et dernière partie du travail est consacrée à l'implémentation des méthodes décrites précédemment. / This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.