Méthodes formelles pour les systèmes distribués temps-réel

Nowadays, real-time systems are ubiquitous in several application domains.Such an emergence led to an increasing need of performance (resources,availability, concurrency, etc.) and initiated a shift from theuse of single processor based hardware platforms, to large setsof interconnected and distributed computing nodes. This trend introduced the birthof a new family of systems that are intrinsically distributed, namelyemph{Networked Embedded Systems}.Such an evolution stems from the growing complexity of real-time softwareembedded on such platforms (e.g. electronic control in avionicsand automotive domains), and the need to integrate formerly isolated systems so thatthey can cooperate, as well as share resources improving thus functionalitiesand reducing costs.Undoubtedly, the design, implementation and verification of such systems areacknowledged to be very hard tasks since theyare prone to different kinds of factors, such as communication delays, CPU(s)speed or even hardware imprecisions, which increases considerably the complexity ofcoordinating parallel activities.In this thesis, we propose a rigorous design flow intended forbuilding distributed real-time applications.We investigate timed automata based models, with formally defined semantics, in orderto study the behavior of a given system with some imposed timing constraints when deployedin a distributed environment. Particularly, we study emph{(i)} the impact of the communicationdelays by introducing a minimum latency between actions executions and the effectivedate at which actions executions have been decided,and emph{(ii)} the effect of hardware imperfections, more precisely clocks imprecisions,on systems execution by breaking the perfect clocks hypothesis, often adopted duringthe modeling phase. Nevertheless, timed automata formalism is intended to describe a highlevel abstraction of the behavior of a given application.Therefore, we use an intermediate representation ofthe initial application that, besides having say{equivalent} behavior, explicitly expressesimplementation mechanisms, and thus reduces the gap between the modeling and the concreteimplementation. Additionally, we contribute in building such systems by emph{(iii)}proposing a knowledge based optimization method that aims to eliminate unnecessarycomputation time or exchange of messages during the execution.We compare the behavior of each proposed model to the initial high level model and study therelationships between both. Then, we identify and formally characterize the potential problemsresulting from these additional constraints. Furthermore, we propose execution strategies thatallow to preserve some desired properties and reach a say{similar} execution scenario,faithful to the original specifications.Aujourd'hui, les systèmes temps réel sont omniprésents dans plusieurs domaines.Une telle expansion donne lieu à un besoin croissant en terme de performance (ressources,disponibilité, parallélisme, etc.) et a initié par la même occasion une transition del'utilisation de plateformes matérielles à processeur unique, à de grands ensemblesde nœuds de calcul inter-connectés et distribués. Cette tendance a donné la naissanceà une nouvelle famille de systèmes connue sous le nom de emph{Networked Embedded Systems},qui sont intrinsèquement distribués.Une telle évolution provient de la complexité croissante des logiciels temps réelembarqués sur de telles plateformes (par exemple les système de contrôle en avioniqueet dans domaines de l'automobile), ainsi que la nécessité d'intégrer des systèmes autrefoisisolés afin d'accomplir les fonctionnalités requises, améliorant ainsi les performanceset réduisant les coûts.Sans surprise, la conception, l'implémentation et la vérification de ces systèmes sontdes tâches très difficiles car ils sont sujets à différents types de facteurs, tels que lesdélais de communication, la fréquence du CPU ou même les imprécisions matérielles,ce qui augmente considérablement la complexité lorsqu'il s'agit de coordonner les activités parallèles.Dans cette thèse, nous proposons une démarche rigoureuse destinée à la construction d'applicationsdistribuées temps réel.Pour ce faire, nous étudions des modèles basés sur les automates temporisés, dont la sémantiqueest formellement définie, afin d'étudier le comportement d'un système donné avec des contraintes de tempsimposées lorsqu'il est déployé dans un environnement distribué. En particulier, nous étudionsemph{(i)} l'impact des délais de communication en introduisant une latence minimale entreles exécutions d'actions et la date à laquelle elles ont été décidées,et emph{(ii)} l'effet des imperfections matérielles, plus précisément les imprécisionsd'horloges, sur l'exécution des systèmes.Le paradigme des automates temporisés reste néanmoins destiné à décrire une abstractiondu comportement d'une application donnée.Par conséquent, nous utilisons une représentation intermédiaire del'application initiale, qui en plus d'avoir un comportement say{équivalent}, exprimeexplicitement les mécanismes mis en œuvre durant l'implémentation, et donc réduit ainsil'écart entre la modélisation et l'implémentation réelle.De plus, nous contribuons à la construction de tels systèmes en emph{(iii)}proposant une optimisation basée sur la emph{connaissance}, qui a pour but d'éliminer lestemps de calcul inutiles et de réduire les échanges de messages pendant l'exécution. Nous comparons le comportement de chaque modèle proposé au modèle initial et étudionsles relations entre les deux. Ensuite, nous identifions et caractérisons formellement lesproblèmes potentiels résultants de ces contraintes supplémentaires. Aussi, nous proposonsdes stratégies d'exécution qui permettent de préserver certaines propriétés souhaitéeset d'obtenir des scénarios d'exécution say{similaires}, et fidèles aux spécificationsde départs