Ce mémoire a pour vocation de prouver aux membres du jury ma capacité à diriger des recherches. Il est organisé de la manière suivante : La première partie regroupe mon curriculum vitae, et une liste de publications. Le chapitre 2 est une présentation générale d'une partie des travaux que j'ai initié au cours de la dernière décennie. Dans un souci de cohérence d'ensemble je n'ai présenté que les travaux relatifs à la commande de systèmes (max,+) linéaires. Ils constituent le dénominateur commun aux trois thèses que j'ai encadrées. Ce chapitre inclut quelques nouveautés à l'attention du lecteur averti, notamment la synthèse d'un observateur d'état est introduite pour la première fois ici. Il se termine sur la présentation de quelques perspectives de recherche. La troisième partie regroupe quelques publications qui permettront au lecteur de retrouver les preuves des résultats énoncés dans le second chapitre.

Les travaux exposés dans ce mémoire portent sur la conception de l'architecture de conduite des systèmes automatisés de production. Ils ont été développés au sein du Laboratoire Universitaire de Recherche en Production Automatisée (LURPA - EA 1385). Il s'agit de travaux prospectifs dont l'objectif est de construire un cadre méthodologique formel de conception et d'évaluation d'architectures.<br /><br />La première partie est consacrée à l'exposé du cadre méthodologique retenu et comporte quatre chapitres dans lesquels sont successivement abordés :<br /><br /> * la problématique générale de la conception d'architectures de conduite, ainsi qu'une revue des \travaux scientifiques dans le domaine,<br /> * la présentation générale de la méthode proposée avec le point de vue des activités de conception, d'évaluation et de choix d'architecture,<br /> * la présentation détaillée de la construction d'architecture avec cette fois le point de vue des différents modèles produits,<br /> * la présentation détaillée d'évaluation et de choix de l'architecture retenue avec encore une fois le point de vue des modèles d'évaluation. <br /><br />La seconde partie du mémoire est destinée à préciser et à valider par l'exemple la méthode proposée. Pour ce faire, nous l'avons appliquée à la conception de l'architecture de conduite d'un poste de lance ment d'un transfert libre. Le plan de cette étude suit de manière ordonnée la démarche que nous avons présenté dans la première partie.

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).

Construire des modèles qui représentent fidèlement les systèmes temps réels complexes est indispensable pour l'analyse de leurs propriétés fonctionnelles et temporelles. Ce travail présente une méthodologie de modélisation pour les systèmes temps réels dans le contexte de la technologie Java. Le modèle est obtenu par la restriction du modèle fonctionnel du logiciel avec les informations temporelles appropriées. Nous établissons un sous ensemble du langage Java qui réglemente la structure concurrente de l'application, la communication et les pratiques de programmation au niveau des threads, des objets et du flot de contrôle. Le modèle fonctionnel est construit à partir de règles de réécriture basées sur la sémantique du langage. Les modèles non temporisés sont ensuite décorés par les informations relatives à la plate forme d'exécution, la dynamique de l'environnement et les échéances temps réel. La méthodologie de modélisation à été implémentée dans l'outil JediTool.

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 développe une méthodologie pour résoudre les problèmes d'ordonnancement de programmes conditionnels où savoir si une tâche doit être exécutée n'est pas connue à l'avance mais dynamiquement. Le modèle utilisé est à base d'automates temporisés représentant l'espace d'états à explorer. Le problème est donc formulé comme le calcul d'une stratégie gagnante (pire cas optimale) dans un jeu contre l'environnement. Dans un premier temps nous étudions le problème d'ordonnancement sur graphes de tâches déterministe puis nous étendons l'étude au problème d'ordonnancement avec incertitude conditionnelle. Pour les deux problèmes nous étudions différentes classes d'ordonnancements et de stratégies pour réduire l'espace d'états, des décompositions en chaînes pour réduire sa taille, puis nous investiguons plusieurs classes d'algorithmes exactes pour en évaluer l'efficacité et à partir desquels nous dérivons de bonnes heuristiques. Des résultats expérimentaux sur plusieurs exemples de benchmarks sont présentés afin de montrer l'efficacité de chaque algorithme et la précision des heuristiques proposées, puis des bornes théoriques sont déduites pour prouver la garantie de performance pire cas de chaque heuristique.

Cette thèse s'inscrit dans le cadre de la théorie des systèmes linéaires dans les dioïdes. Cette théorie concerne la sous-classe des systèmes à événements discrets modélisables par les Graphes d'Événements Temporisés (GET). La dynamique de ces graphes peut être représentée par des équations récurrentes linéaires sur des structures algébriques particulières telles que l'algèbre (max,+) ou l'algèbre (min,+).Ce mémoire est consacré à l'analyse de performances des systèmes dynamiques qui peuvent être modélisés graphiquement par des Graphes d'Événements Temporisés Généralisés (GETG). Ces derniers, contrairement au GET, n'admettent pas une représentation linéaire dans l'algèbre (min,+). Pour pallier à ce problème de non linéarité, nous avons utilisé une approche de modélisation définie sur un dioïde d'opérateurs muni de deux lois internes : loi additive correspondant à l'opération (min), et loi multiplicative équivalente à la loi de composition usuelle. Le modèle d'état obtenu, est utilisé pour évaluer les performances des GETG. Pour cela, nous avons proposé une nouvelle méthode qui a pour but de linéariser le modèle mathématique régissant l'évolution dynamique du modèle graphique, dans le but d'obtenir un modèle (min,+) linéaire. La deuxième partie de cette thèse est consacrée au problème qui consiste à déterminer les ressources à utiliser dans une ligne de production, en vue d'atteindre des performances souhaitée. Ceci est équivalent à déterminer le marquage initial de la partie commande du GETG.

La vérification en ligne de spécifications formelles permet de créer des détecteurs d'erreur dont le pouvoir de détection dépend en grande partie du formalisme vérifié à l'exécution. Plus le formalisme est puissant plus la séparation entre les exécutions correctes et erronées peut être précise. Cependant, l'utilisation des vérifieurs en-ligne dans le but de détecter des erreurs est entravée par deux problèmes récurrents : le coût à l'exécution de ces vérifications, et le flou entourant les propriétés sémantiques exactes des signaux d'erreur ainsi générés. L'objectif de cette thèse est de clarifier les conditions d'utilisation de tels détecteurs dans le cadre d'applications " temps réel " critiques. Dans ce but, nous avons donné l'interprétation formelle de la notion d'erreur comportementale " temps réel". Nous définissions la propriété de détection " au plus tôt " qui permet de d'identifier la classe des détecteurs qui optimisent la latence de détection. Pour illustrer cette classe de détecteurs, nous proposons un prototype qui vérifie un comportement décrit par un automate temporisé. La propriété de détection au plus tôt est atteinte en raisonnant sur l'abstraction temporelle de l'automate et non sur l'automate lui-même. Nos contributions se déclinent dans trois domaines, la formalisation de la détection au plus tôt, sa traduction pour la synthèse de détecteurs d'erreur à partir d'automate temporisés, puis le déploiement concret de ces détecteurs sur une plate-forme de développement temps réel, Xenomai.

Les systèmes dynamiques présentent des comportements temporels qui peuvent être exprimés sous diverses formes séquentielles telles que des signaux, des ondes, des séries chronologiques et des suites d'événements. Détecter des motifs sur de tels comportements temporels est une tâche fondamentale pour comprendre et évaluer ces systèmes. Étant donné que de nombreux comportements du système impliquent certaines caractéristiques temporelles, le besoin de spécifier et de détecter des motifs de comportements qui implique des exigences de synchronisation, appelées motifs temporisés, est évidente.Cependant, il s'agit d'une tâche non triviale due à un certain nombre de raisons, notamment la concomitance des sous-systèmes et la densité de temps.La contribution principale de cette thèse est l'introduction et le développement du filtrage par motif temporisé, c'est-à-dire l'identification des segments d'un comportement donné qui satisfont un motif temporisé. Nous proposons des expressions rationnelles temporisées (TRE) et la logique de la boussole métrique (MCL) comme langages de spécification pour motifs temporisés. Nous développons d'abord un nouveau cadre qui abstraite le calcul des aspects liés au temps appelé l'algèbre des relations temporisées. Ensuite, nous fournissons des algorithmes du filtrage hors ligne pour TRE et MCL sur des comportements à temps dense à valeurs discrètes en utilisant ce cadre et étudions quelques extensions pratiques.Il est nécessaire pour certains domaines d'application tels que le contrôle réactif que le filtrage par motif doit être effectué pendant l'exécution réelle du système. Pour cela, nous fournissons un algorithme du filtrage en ligne pour TREs basé sur la technique classique des dérivées d'expressions rationnelles. Nous croyons que la technique sous-jacente qui combine les dérivées et les relations temporisées constitue une autre contribution conceptuelle majeure pour la recherche sur les systèmes temporisés.Nous présentons un logiciel libre Montre qui implémente nos idées et algorithmes. Nous explorons diverses applications du filtrage par motif temporisé par l'intermédiaire de plusieurs études de cas. Enfin, nous discutons des orientations futures et plusieurs questions ouvertes qui ont émergé à la suite de cette thèse. / Dynamical systems exhibit temporal behaviors that can be expressed in various sequential forms such as signals, waveforms, time series, and event sequences. Detecting patterns over such temporal behaviors is a fundamental task for understanding and assessing these systems. Since many system behaviors involve certain timing characteristics, the need to specify and detect patterns of behaviors that involves timing requirements, called timed patterns, is evident. However, this is a non-trivial task due to a number of reasons including the concurrency of subsystems and density of time.The key contribution of this thesis is in introducing and developing emph{timed pattern matching}, that is, the act of identifying segments of a given behavior that satisfy a timed pattern. We propose timed regular expressions (TREs) and metric compass logic (MCL) as timed pattern specification languages. We first develop a novel framework that abstracts the computation of time-related aspects called the algebra of timed relations. Then we provide offline matching algorithms for TRE and MCL over discrete-valued dense-time behaviors using this framework and study some practical extensions.It is necessary for some application areas such as reactive control that pattern matching needs to be performed during the actual execution of the system. For that, we provide an online matching algorithm for TREs based on the classical technique of derivatives of regular expressions. We believe the underlying technique that combines derivatives and timed relations constitutes another major conceptual contribution for timed systems research.Furthermore, we present an open-source tool Montre that implements our ideas and algorithms. We explore diverse applications of timed pattern matching over several case studies using Montre. Finally we discuss future directions and several open questions emerged as a result of this thesis.