Ce mémoire présente des travaux concernant la spécification, la modélisation et l'analyse de systèmes de contrôle-commande temps réel répartis sur un réseau de terrain. La problématique de modélisation de tels systèmes, qui doivent satisfaire des contraintes temporelles, réside dans la maîtrise de la taille et de la complexité des modèles. Pour cela, une méthodologie de modélisation est proposée ; elle repose sur les concepts de structuration, de modélisation et de validation modulaires au moyen du modèle formel Réseaux de Petri Temporisés Stochastiques. La structuration consiste en une décomposition hiérarchisée en blocs fonctionnels élémentaires. Une structure est proposée pour des entités de communication d'un réseau local temps réel, ainsi que pour un système temps réel de commande et surveillance réparties. La modélisation repose sur la construction et la composition de modèles de modules élémentaires. Les principes énoncés concernent la définition de règles de composition. Des modèles d'assertions logiques sont également proposés pour faciliter le passage des descriptions de comportements exprimées en langage naturel, à une modélisation en Réseaux de Petri Temporisés Stochastiques. La validation repose sur des étapes de composition partielle qui utilisent la modularité pour effectuer des vérifications ascendantes du comportement. Cette méthodologie est appliquée au réseau de terrain FIP, ainsi qu'au futur système de contrôle-commande de poste de transformation d'énergie électrique d'EDF. L'étude du réseau FIP porte plus particulièrement sur les services et mécanismes périodiques de couche application pour les échanges temps réel. Les analyses (qualitatives et quantitatives) effectuées sur l'application de EDF répartie sur le réseau FIP portent sur la vérification des propriétés fonctionnelles et des contraintes temporelles du système.

Les probabilités sont de plus en plus utilisées dans la conception et l'analyse des systèmes logiciels et matériels informatiques. L'introduction des tirages aléatoires dans les algorithmes concurrents et distribués permet de résoudre certains problèmes insolubles dans le cadre déterministe et de réduire la complexité de nombreux autres. Nous avons été amenés à étudier deux types de propriétés probabilistes. La convergence : cette propriété assure que, quel que soit l'état de départ et quel que soit l'enchainement des actions, le système atteindra toujours (avec probabilité 1) un ensemble donné d'états d'arrivée en un nombre fini d'actions (auto-stabilisation).L'accessibilité : ce type de propriété répond à des questions telles que "quelle est la probabilité p qu'une exécution partant d'un état initial donné atteigne un état final donné ? Quelles sont les bornes maximales et minimales de p ?" En ce qui concerne le premier point, nous avons développé de nouveaux critères permettant d'assurer la convergence et d'en calculer la vitesse (mixing time). Ces crotères utilisent l'analogie avec des modèles de physiquestatistique (champs de Markov) et exploitent des outils d'analyse probabiliste classiques (coupling, chaînes de Markov, processus de décision markoviens). Pour le second point, nous avons obtenu des résultats pratiques sur la vérification de protocoles de communication, comme le protocole Ethernet, en les modélisant à l'aide d'automates temporisés probabilistes et utilisant des outils de model-checking temporisés (HyTech) et probabiliste (PRISM, APMC).

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 nous sommes intéressés au concept de stabilisation instantanée. Ainsi, nous avons tout d'abord proposé deux solutions instantanément stabilisantes au problème de parcours en profondeur pour des réseaux enracinés quelconques. Ces deux protocoles sont écrits dans le modèle à états et fonctionnent sous l'hypothèse d'un démon distribué inéquitable : le démon le plus général du modèle. Le premier est basé sur des listes d'identités. Le second utilise un principe de question/réponse pour remplacer les listes d'identités. Nous proposons ensuite deux applications instantanément stabilisantes obtenues à partir de nos deux protocoles de parcours en profondeur. Ces deux applications évaluent des propriétés globales sur le réseau. La première application permet de marquer les points d'articulation et les isthmes du réseau. La seconde application permet d'évaluer si un ensemble donné est un ensemble séparateur du réseau. Enfin, dans une dernière partie, nous adoptons une approche plus générale en étudiant un protocole efficace permettant de transformer semi-automatiquement des protocoles de service mono-initiateurs en protocoles instantanément stabilisants. Un protocole de parcours en profondeur et un protocole de construction d'arbre en largeur illustrent la facilité avec laquelle nous pouvons rendre instantanément stabilisants ce type protocole grâce à notre transformateur. Le protocole de parcours en profondeur est non seulement trivial à écrire mais les performances obtenues en font un compromis quasi idéal entre les protocoles à listes et à questions présentés précédemment. Enfin, grâce à une propriété de comptage due à notre transformateur, nous montrerons comment utiliser ce protocole de parcours pour résoudre en quelques lignes l'exclusion mutuelle de manière instantanément stabilisante.

L'implémenation distribuée des systèmes temps-réel a été toujous une tâche non-triviale. La coordination des composants s'exécutant sur une plate-forme distribuée doit être assurée par des protocoles de communication complexes en tenant compte de leurs contraintes de temps. Dans cette thèse, nous proposons un flot de conception rigoureux à partir d'un modèle de haut niveau d'un logiciel d'application décrit en BIP (Behavior, Interaction, Priority) et conduisant à une implémenation distribuée. Le flot de conception implique l'utilisation de transformations de modèles tout en conservant les propriétés fonctionnelles des modèles originaux de BIP. Un modèle BIP se compose d'un ensemble de composants qui se synchronisent à travers les interactions et les priorités. Notre méthode transforme les modèles BIP en un modéle Send/Receive qui fonctionnent en utilisant le passage de messages asynchrones. Les modèles obtenus sont directement implémenté sur une plate-forme donnée. Nous présentons trois solutions pour obtenir un modéle Send/Receive. Dans la première solution, nous proposons des modéles Send/Receive qui fonctionnent avec un engin centralisé qui implémente les interactions et les priorités. Les composants atomiques des modèles originaux sont transformés en composants Send/Receive qui communiquent avec l'engin centralisé via des interactions Send/Receive. L'engin centralisé exécute les interactions sous certaines conditions définies par les modèles à états partiels. Ces modèles représentent une déscription haut niveau de l'exécution parallèle de modèles BIP. Dans la deuxième solution, nous proposons de décentraliser l'engin. Les modéles Send/Receive obtenus sont structurées en trois couches: (1) les composants Send/Receive (2) un ensemble d'engin, chacun exécutant un sous-ensemble d'interactions, et (3) un ensemble de composants implémentant un protocole de résolution des conflits. Avec les solutions décrites ci-dessus, nous supposons que les latences de communication sont négligeables. Ceci est du au fait que les modéles Send/Receive sont concu de telle sorte qu'il n'y ait pas retard entre la décision d'exécuter une interaction dans un engin et son exécution dans les composants participant. Dans la troisième solution, nous proposons des modéles Send/ Receive qui exécutent correctement même en présence de latences de communication. Cette solution est basée sur le fait que les engin planifient l'exécution des interactions et notifient les composants à l'avance. Afin de planifier correctement les interactions, nous montrons que les engins sont tenus à observer des composants supplémentaires, en plus de ceux qui participent aux interactions. Nous présentons également une méthode pour optimiser le nombre de composants observés, en se basant sur l'utilisation de techniques d'analyse statique. A partir d'un modéle Send/Receive donné, nous générons une application distribuée où les interactions Send/Receive sont implémentées par les sockets TCP. Les résultats expérimentaux sur des exemples non triviaux et des études de cas montrent l'efficacité de notre méthode. / Correct distributed implementation of real-time systems has always been a challenging task. The coordination of components executing on a distributed platform has to be ensured by complex communication protocols taking into account their timing constraints. In this thesis, we propose rigorous design flow starting from a high-level model of an application software in BIP (Behavior, Interaction, Priority) and leading to a distributed implementation. The design flow involves the use of model transformations while preserving the functional properties of the original BIP models. A BIP model consists of a set of components synchronizing through multiparty interactions and priorities. Our method transforms high-level BIP models into Send/Receive models that operate using asynchronous message passing. The obtained models are directly implementable on a given platform. We present three solutions for obtaining Send/Receive BIP models. -In the first solution, we propose Send/Receive models with a centralized scheduler that implements interactions and priorities. Atomic components of the original models are transformed into Send/Receive components that communicate with the centralized scheduler via Send/Receive interactions. The centralized scheduler is required to schedule interactions under some conditions defined by partial state models. Those models represent high-level representation of parallel execution of BIP models. - In the second solution, we propose to decentralize the scheduler. The obtained Send/Receive models are structured in 3 layers: (1) Send/Receive atomic components, (2) a set of schedulers each one handling a subset of interactions, and (3) a set of components implementing a conflict resolution protocol. With the above solutions, we assume that the obtained Send/Receive models are implemented on platforms that provide fast communications (e.g. multi-process platforms) to meet perfect synchronization in components. This is because the obtained schedulers are modeled such that interactions scheduling corresponds exactly to execution in components. - In the third solution, we propose Send/Receive models that execute correctly even if communications are not fast enough. This solution is based on the fact that schedulers plan interactions execution and notify components in advance. In order to plan correctly the interactions, we show that the schedulers are required to observe additional components, in addition to the ones participating in the interactions. We present also a method to optimize the number of observed components, based on the use of static analysis techniques. From a given Send/Receive model, we generate a distributed implementation where Send/Receive interactions are implemented by TCP sockets. The experimental results on non trivial examples and case studies show the efficiency of our design flow.

Le thème global de la thèse est le comportement transitoire de certains systèmes répartis. Les résultats peuvent être divisés en trois groupes : transients de matrices et systèmes max-plus, convergence de systèmes de consensus asymptotique et la modélisation de "glitches" dans des circuits numériques. Pour l'algèbre max-plus, les résultats sont des bornes supérieures sur les transients de matrices et système linéaires max-plus. Elles améliorent strictement les bornes publiées. La thèse inclut une discussion de l'impact des bornes dans des applications. Les preuves utilisent notamment des réductions de chemins. La thèse contient aussi des bornes plus précises pour les transients des indices critiques. Ces bornes sont, en fait, indépendantes des poids spécifiques et ne dépendent que de la structure du graphe de la matrice et son graphe critique. De plus, elles sont des généralisations strictes des bornes booléennes pour des graphes non pondérées; par exemple les bornes de Wielandt ou de Dulmage et Mendelsohn. Quant au consensus asymptotique, la thèse améliore des bornes supérieures sur le taux de convergence et établit de nouveaux résultats sur la convergence dans le cas où les agents n'ont pas nécessairement de confiance en soi, c'est-à-dire qu'ils peuvent ignorer leurs propres valeurs. Ces résultats sont notamment pour des réseaux complètement dynamiques. Elle contient aussi un exemple d'un réseau complètement statique dont le taux de convergence est dans le même ordre que celui d'une grande classe de réseaux dynamiques. La dernière partie de la thèse est sur la propagation de "glitches" (signaux transitoires très courts) dans des circuits numériques. Plus spécifiquement, elle traite des modèles à valeur discrète et temps continu pour des circuits numériques. Ces modèles sont utilisés dans des outils pour la conception de circuits car ils sont beaucoup plus vites que la résolution des équations différentielles. Cependant, comme c'est prouvé dans la thèse, les modèles existants ne prédisent pas correctement l'occurrence de glitches dans le signal sortant d'un circuit. De plus, la thèse contient une proposition d'un nouveau modèle qui ne partage pas les caractéristiques avec les modèles existants qui leur interdisent de prédire correctement l'occurrence de glitches.

L'objectif de ce travail est de fournir des modèles et outils pour simplifier la construction des systèmes distribués à base de composants sécurisés, ainsi que la gestion des propriétés de sécurité, en utilisant des outils de haut niveau d'abstraction pour la configuration et la reconfiguration dynamique. En plus des propriétés d'accessibilité et de communications sécurisées classiques, nous focalisons notre travail sur une propriété des systèmes répartis plus générale : la non-interférence. Cette propriété atteste qu'il ne doit pas y avoir de flux d'information entre des parties publiques et privées du système. Ce qui implique le suivi de l'acheminement de l'information entre les différentes composantes du système distribué. Notre objectif principal est donc de proposer un modèle, accompagné d'un ensemble d'outils, garantissant la propriété de la non-interférence à la construction du système, et ce à une plus grosse granularité : celle des composants. Ces outils permettent de (1) configurer les paramètres de sécurité des composants et des liaisons entre eux, (2) vérifier la propriété de non-interférence dans le code d'un composant et entre les différents composants du système et (3) générer automatiquement le code nécessaire pour appliquer ces propriétés de sécurité. D'autre part, nous proposons une architecture permettant de vérifier dynamiquement la propriété de non-interférence dans un système réparti.

Modern organisations rely intensively on information and communication technology infrastruc- tures. Such infrastructures offer a range of services from simple mail transport agents or blogs to complex e-commerce platforms, banking systems or service hosting, and all of these depend on distributed systems. The security of these systems, with their increasing complexity, is a chal- lenge. Cloud services are replacing traditional infrastructures by providing lower cost alternatives for storage and computational power, but at the risk of relying on third party companies. This risk becomes particularly critical when such services are used to host privileged company information and applications, or customers' private information. Even in the case where companies host their own information and applications, the advent of BYOD (Bring Your Own Device) leads to new security related issues. In response, our research investigated the characterization and detection of malicious activities at the operating system level and in distributed systems composed of multiple hosts and services. We have shown that intrusions in an operating system spawn abnormal information flows, and we developed a model of dynamic information flow tracking, based on taint marking techniques, in order to detect such abnormal behavior. We track information flows between objects of the operating system (such as files, sockets, shared memory, processes, etc.) and network packets flowing between hosts. This approach follows the anomaly detection paradigm. We specify the legal behavior of the system with respect to an information flow policy, by stating how users and programs from groups of hosts are allowed to access or alter each other's information. Illegal information flows are considered as intrusion symptoms. We have implemented this model in the Linux kernel4 , as a Linux Security Module (LSM), and we used it as the basis for practical demonstrations. The experimental results validated the feasibility of our new intrusion detection principles. This research is part of a joint research project between Supélec (École supérieure d'éléctricité) and QUT (Queensland University of Technology).

Un Système Multi-Agents (SMA) ouvert est un système extensible et évolutif. Son extension se traduit par la possibilité d'ajouter de nouveaux agents mais aussi de gérer leurs retraits. De plus, un SMA ouvert doit permettre l'évolution de ses agents. Nous nous sommes intéressés à la conception de SMA ouverts du point de vue de la représentation des autres maintenue par chaque agent du système. L'ouverture peut conduire la représentation qu'un agent a des autres, à devenir fausse ou incomplète. Dans les travaux existants, l'ouverture d'un SMA est gérée de manière centrale par une entité regroupant une représentation de chaque agent du système. Cette entité, qui selon les cas est un " broker ", un faciliteur ou des pages jaunes, fournit sur demande la connaissance nécessaire à un agent pour raisonner sur les autres agents de son système. Outre le coût de l'accès à ces informations, cette approche présente l'inconvénient de dépendre du bon fonctionnement de cette entité critique et indispensable à l'ouverture et à la coopération. La première étape de ce travail a été d'analyser dans quelle mesure on peut distribuer la tâche consistant à intégrer de nouveaux agents. Cette analyse nous a conduit à définir un modèle social partiel d'agent que nous appelons sa facette accueillante. Un agent accueillant est un agent ayant la faculté d'aider un nouvel agent à intégrer le système auquel il appartient. Une société composée d'agents accueillants est un SMA ouvert où l'intégration de nouveaux agents est assurée par une activité collective et coopérative faisant intervenir plusieurs agents accueillants. Le développement d'une approche distribuée de la conception de SMA ouverts nous a ensuite amené à généraliser le problème de l'ouverture. Nous avons repris notre définition des tâches associées à la gestion de l'ouverture d'un SMA pour proposer un modèle général de conception de SMA ouvert autorisant le choix d'une approche centralisée ou distribuée.