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.

Ce travail présente l'approche UML/PNO (Unified Modelling Language with Petri Net Objects) pour la spécification de systèmes temps réel. La méthode propose d'enrichir la description semi-formelle UML du système par une modélisation formelle basée sur les réseaux de Petri. Les concepts UML de sous-système et d'interface ont été étendus afin d'améliorer la description de la vue système en termes de tructuration, gestion de projet et organisation de la modélisation. L'objectif est également d'adapter la méthode de modélisation système à une approche " orientée composant " pour le temps réel. Le concept " d'objet composé " permet d'intégrer des spécificités temps réel au sein du composant (protocole de communication, contrainte temporelle, effet observable). Le comportement des objets est spécifié à l'aide des réseaux de Petri à places et transitions stochastiques temporelles afin de permettre la validation et la vérification du système en cours de spécification. L'approche de validation propose des traductions semi-automatiques des diagrammes UML en réseaux de Petri. Les techniques classiques de simulation et d'évaluation de performances peuvent alors être appliquées. Ces traductions présentent l'avantage de rassembler, sur un même modèle à réseau de Petri, tous les aspects dynamiques du composant apparaissant dans différents diagrammes UML et de vérifier ainsi la cohérence de son comportement et de son utilisation. La vérification utilise les techniques d'analyse formelle, basées sur l'utilisation conjointe du graphe de classes et de la logique linéaire. Une approche de vérification quantitative des contraintes temporelles est proposée au niveau de l'analyse des besoins et des exigences du système. Une partie de ce travail a été concrétisée par l'intégration d'un module (ArgoPNO) dans l'atelier de génie logiciel ArgoUML. A ce jour, une première automatisation de la démarche de vérification des contraintes temporelles est opérationnelle sur cet outil.