L'analyse d'une chaîne de production manufacturière complète, composée de plusieurs systèmes bouclés temporisés, en utilisant des modèles détaillés est presque impossible à cause des problèmes liés aux tailles des modèles. Une solution pour contourner ces difficultés consiste à utiliser des techniques d'analyse multi-échelles utilisant à la fois des modèles détaillés des système bouclés, lorsque nécessaire, mais aussi des modèles abstraits de certains systèmes bouclés dès que possible. Afin de garantir les résultats lors d'analyses multi-échelles, il convient de garantir que les modèles détaillés des systèmes bouclés ne permettent pas d'évolutions indésirables ne représentant pas un comportement réaliste des système bouclés, et que les modèles abstraits des système bouclés utilisés pendant l'analyse ont un comportement identique aux modèles détaillés de ces mêmes systèmes bouclés. La première contribution de ces travaux est une méthodologie de conception de modèles détaillés, utilisant des automates temporisés, de systèmes bouclés temporisés permettant de supprimer les évolutions irréalistes. Les solutions proposées pour y parvenir se basent sur une conception modulaire, des mécanismes d'urgence et des variables partagées. La seconde contribution de ces travaux est axée sur la vérification de l'équivalence entre les modèles détaillé et abstrait d'un même système bouclé. Pour ce faire, une équivalence conforme aux exigences d'une analyse multi-échelles est retenue, puis une méthode basée sur un automate observateur-séquenceur couplé à un model-checker est décrite. Enfin, la prise en compte d'une équivalence avec tolérances (en valeur et/ou temporelle) est détaillée.

Cette thèse porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes temps-réel. La thèse est constituée de trois parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (sur-approximation, sous-approximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes temps-réel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure non-déterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles forçant la convergence d'horloges. Finalement, nous étudions le problème de l'accessibilité des états acceptants dans des réseaux d'automates temporisés qui communiquent via des files FIFO. Nous considérons tout d'abord des automates temporisés à temps discret, et caractérisons les topologies de réseaux pour lesquelles l'accessibilité est décidable. Cette caractérisation est ensuite étendue aux automates temporisés à temps continu.

Dans cette thèse nous proposons un cadre formel complet pour l'analyse des systèmes temporisés, avec l'accent mis sur la valeur pratique de l'approche. Nous décrivons des systèmes comme des automates temporisés et nous exprimons les propriétés en logiques temps-réel. Nous considérons deux types d'analyse. Vérification : étant donnés un système et une propriété, vérifier que le système satisfait la propriété. Synthèse de contrôleurs : étant donnés un système et une propriété, restreindre le système pour qu'il satisfasse la propriété. Pour rendre l'approche possible malgré la difficulté théorique des problèmes, nous proposons : Des abstractions pour réduire l'espace d'états concret en un espace abstrait beaucoup plus petit qui, pourtant, préserve toutes les propriétés qui nous intéressent. Des techniques efficaces pour calculer et explorer l'espace d'états abstrait. Nous définissons des bisimulations et simulations faisant abstraction du temps et nous étudions les propriétés qu'elles préservent. Pour les bisimulations, l'analyse consiste à générer d'abord l'espace abstrait, et ensuite l'utiliser pour vérifier des propriétés sur l'espace concret. Pour les simulations, la génération et la vérification se font en même temps (à-la-volée). Un algorithme à-la-volée est aussi développé pour la synthèse de contrôleurs. Pour aider l'utilisateur à sa compréhension du système, nous produisons des séquences diagnostiques concrètes. Nous avons implanté nos méthodes dans Kronos, l'outil d'analyse temps-réel de Verimag, et nous avons traité un nombre d'études de cas réalistes parmi lesquelles le protocole FRP-DT de réservation rapide de débit pour les réseaux ATM (dans le cadre d'une coopération scientifique avec le CNET), le protocole de détection de collisions dans un réseaux à accès multiple de Band&Olufsen, l'ordonnancement de tâches temps-réel périodiques, la cohérence et l'ordonnancement des documents multimédia, ainsi qu'un nombre d'études de cas benchmarks, telles que le protocole d'exclusion mutuelle de Fischer, les protocoles de communication CSMA/CD et FDDI.

Les services web gagnent de l'importance en tant que cadre facilitant l'intégration d'applications au sein et en dehors des frontières des entreprises. Il est accepté que la description d'un service ne devrait pas seulement inclure l'interface, mais aussi le protocole métier supporté par le service. Dans le cadre de ce travail, nous avons formalisé la catégorie des protocoles incluant des contraintes de temps (appelés protocoles temporisés) et étudié l'impact du temps sur l'analyse de compatibilité et de remplaçabilité. Nous avons formalisé les contraintes suivantes : les contraintes Clnvoke définissent des fenêtres de disponibilités tandis que les contraintes Mlnvoke définissent des délais d'expiration. Nous avons étendu les techniques pour l'analyse de compatibilité et de remplaçabilité entre protocoles temporisés à l'aide d'un mapping préservant la sémantique entre les protocoles temporisés et les automates temporisés, ce qui a défini la classe des automates temporisés de protocoles (PTA). Les PTA possèdent des transitions silencieuses qui ne peuvent pas être supprimées en général, et pourtant ils sont fermés par calcul du complément, ce qui rend décidable les différents types d'analyse de compatibilité et de remplaçabilité. Enfin, nous avons mis en oeuvre notre approche dans le cadre du projet ServiceMosaic, une plate-forme pour la gestion du cycle de vie des services web.

La plupart des scénarios multimédia interactifs sont basés sur des spécifications informelles, il n'est donc pas possible de vérifier formellement des propriétés de ces systèmes. Nous préconisons la nécessité d'un modèle général et formel. Partitions interactives est un formalisme pour décrire des scénarios multimédia interactifs. Nous proposons une nouvelle sémantique pour les partitions interactives basée sur les structures d'événements temporisés. Avec une telle sémantique, nous pouvons spécifier des propriétés pour le système, en particulier, des propriétés sur les traces, qui sont difficiles à préciser avec la programmation par contraintes. Nous présentons également une sémantique opérationnelle des partitions interactives basée sur le calcul non-déterministe, temporisé, concurrent, par contraintes (ntcc) et nous rapportons la sémantique operationelle à la semantique en structures d'événements temporisés. Avec la sémantique opérationnelle, nous pouvons décrire formellement le comportement d'un scenario dont les durées des objets temporels peuvent être des intervalles d'entiers arbitraires. La sémantique opérationnelle est obtenue à partir de la sémantique en structures d'événements temporisés de la partition interactive. Pour fournir une telle traduction, nous avons d'abord défini la forme normale d'une structure d'événements temporisés, dans laquel les événements liés avec une durée zéro sont regroupés en un seul. Nous avons également défini la notion de structures d'événements temporisés répartissables, de telle sorte que son graphe de contraintes peut être expédié en se fondant uniquementsur la propagation locale. Nous croyons que la sémantique opérationnelle basée sur ntcc offre certains avantages par rapport à la sémantique des partitions interactives basée sur des réseaux de Petri; par exemple, les durées des objets temporels peuvent être des intervalles d'entiers arbitraires, tandis que dans la plupart des modèles de partitions interactives, les intervalles ne peut être utilisés que pour représenterles relations telles que l'égalité et les inégalités. Nos modèles ntcc de partitions interactives sont exécutés en utilisant Ntccrt, un interprète temps réel pour ntcc. Nos modèles peuvent également être vérifiés automatiquement en utilisant ntccMC, un vérificateur pour ntcc, de temps borné, basée sur les automates finis, que nous introduisons dans cette thèse. En utilisant ntccMC, nous pouvons vérifier des propriétés de logique de temps linéaire avec des contrantes (CLTL). Dans cette thèse, nous introduisons deux extensions du formalisme de partitions interactives:(1) l'une pour gérer le traitement audio en utilisant le langage de programmation français Faustet (2) l'autre pour traiter des condition et des branchements, permettant de spécifier des choix et des boucles. Pour la première extension, nous présentons une sémantique basée sur les structures d'événements temporisés et des idées sur la façon de définir une sémantique opérationnelle. Pour la deuxième extension, nous présentons une mise en oeuvre et la comparaison des résultats du jitter relative moyenne d'une implémentation d'un arpège base sur l'algorithme de Karplus-Strong par rapport aux implémentations existants écrits dans Pure Data. Nous définissons aussi un format de sauvegarde XML pour les partitions interactives et pour la extension avec branchement conditionnel. Un format de sauvegarde est crucial pour assurer la persistance des partitions. / Technology has shaped the way on which we compose and produce music. Notably, the invention of microphones and computers pushed the development of new music styles in the 20th century. In fact, several artistic domains have been benefiting from such technology developments ; for instance, Experimental music, non-linear multimedia, Electroacoustic music, and interactive multimedia. In this dissertation, we focus on interactive multimedia.Interactive multimedia deals with the design of scenarios where multimedia content and interactive events are handled by computer programs. Examples of such scenarios are multimedia art installations, interactive museum exhibitions, some Electroacoustic music pieces, and some Experimental music pieces. Unfortunately, most interactive multimedia scenarios are based on informal specifications, thus it is not possible to formally verify properties of such systems. We advocate the need of a general and formal model. Interactive scores is a formalism to describe interactive multimedia scenarios. We propose new semantics for interactive scores based on timed eventstructures. With such a semantics, we can specify properties for the system, in particular, properties about traces, which are difficult to specify as constraints. In fact, constraints are an important part of the semantic model of interactive scores because the formalism is based on temporal constraints among the objects of the scenario. We also present an operational semantics of interactive scores based on the non-deterministic timed concurrent constraint (ntcc) calculus and we relate such a semantics to the timed event structures semantics. With the operational semantics, we formally describe the behavior of a score whose temporal object durations can be arbitrary integer intervals. The operational semantics is obtained from the timed event structures semantics of the score. To provide such a translation, we first define the normal form of a timed event structure in which events related with zero-duration delays are collapsed into a single one. We also define the notion of dispatchable timed event structures. Event structures such that its constraint graph can be dispatched by relying only on local propagation.We believe that operational semantics in ntcc offers some advantages over existing Petri nets semantics for interactive scores; for instance, the duration of the temporal objects can be arbitrary integer intervals, whereas inprevious models of interactive scores, such durations can only be intervals to represent equalities and inequalities. In this dissertation, we also introduce two extensions of the formalism of interactive scores : (1) one to handle audio processing using the Fast AUdio Stream (Faust) languageand (2) another one to handle conditional branching, allowing designers to specify choices and loops. For the first extension, we present a timed event structures semantics and ideas on how to define operational semantics. For the second extension, we present an implementation and results comparing the average relative jitter of an implementation ofan arpeggio based on Karplus-Strong with respect to existing implementations of Karplus written in Pure Data. We also define a XML file format for interactive scores and for the conditional branching extension. A file format is crucial to assure the persistence of the scores. Ntcc models of interactive scores are executed using Ntccrt, a real-time capable interpreter for ntcc. They can also be verified automatically using ntccMC, a bounded-time automata based model checker for ntcc which we introduce in this dissertation. Using ntccMC, we can verify properties expressed on constraint linear-time logic. Ntcc has been used in the past, not only for multimedia interaction models, but alsofor system biology, security protocols and robots.

Nous présentons dans ce travail de thèse des approches pour la spécification et la vérificationdes systèmes temporisés. La première partie concerne une méthode de spécification enutilisant les diagrammes états-transitions pour modéliser un système donné en partant d’unedescription textuelle. Cette méthode guide l’utilisateur pour le développement de la modélisation.Elle comporte plusieurs étapes et utilise des observateurs d’états et des événements afind’engendrer le diagramme états-transitions. Un outil qui implémente les différentes étapes de laméthode de spécification pour une application semi-automatique est présenté. La seconde partieconcerne une traduction des diagrammes états-transitions vers les réseaux de Petri colorés, cequi permet d’utiliser les méthodes de vérification. Nous prenons en considération dans cette traductionun ensemble important des éléments syntaxiques des diagrammes états-transitions, telsque la concurrence, la hiérarchie, etc. Un outil qui implémente la traduction pour un passageautomatique des diagrammes états-transitions vers les réseaux de Petri colorés est en cours de développement.La dernière partie concerne l’intégration des contraintes temporelles dans les deuxapproches précédentes. Nous définissons des annotations pour les diagrammes états-transitionsdont nous fournissons la syntaxe et la sémantique. Ces annotations seront ensuite utilisées dansla méthode de spécification et la traduction. Le but est de proposer des annotations faciles àcomprendre et à utiliser avec une syntaxe qui prend en compte des contraintes parmi les plusutilisées. / In order to specify and verify timed systems, we present in this thesis approaches using UMLstate machines and coloured Petri nets. Our first approach is a specification method that takesinto account a textual description of the system and generates the corresponding state machinediagram. This method helps a non-expert user to model a system in a structural way. We presenta tool that implements the specification method. Our second approach is the translation of UMLstate machine diagrams to coloured Petri nets diagrams. In this approach we take into account animportant set of UML state machine elements that allows the modelling of concurrent systems,etc. A tool that implements the approach and allows us to automate the translation is beingdeveloped. Finally, the last approach is the integration of time constraints in our specificationmethod and in our translation. We propose a set of annotations to model time in state machinediagrams, and we define the corresponding syntax and semantics.

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.

La composition des systèmes temporisés est source de nombreux problèmes, notamment de blocage. Nous proposons un cadre de description compositionnelle des systèmes temporisés qui préserve la réactivité temprorelle, à savoir que si le système ne peut réagir, alors le temps peut avancer. Nous effectuons d'abord une étude préliminaire sur la spécification des évolutions temporelles dans les systèmes, débouchant sur la définition de mécanismes de description adéquats. Ceci nous permet de définir une classe de modèles temporisés temporellement réactifs, par construction. Nous définissons sur cette classe des opérateurs de choix et de composition parallèle qui préservent cette propriété. En outre, les opérateurs sont définis de sorte à préserver l'activité dans le sens où si à partir d'un état une action est possible dans un composant, alors une action est possible dans la composition. L'opérateur de composition parallèle respecte également la propriété de progrès maximal grâce à l'utilisation d'opérateurs de choix avec priorités qui favorise les synchronisations. Un cadre général est donné pour exprimer différents modes de synchronisation, parmi lesquels on retiendra AND (synchronisation classique), MAX (synchronisation avec attente) et MIN (interruption). Pour terminer, nous développons une approche algébrique pour une sous-classe des modèles considérés.

Les performances temporelles d'une architecture de contrôle-commande conditionnent fortement celles du système automatisé de production commandé. Pour maîtriser ces performances temporelles, l'architecte automaticien doit pouvoir les évaluer à chaque phase du cycle de développement : de l'étude d'avant-projet à la conception détaillée ainsi que lors de la mise au point. Il n'a cependant pas les mêmes attentes concernant les performances estimées. Des résultats approximatifs, obtenus rapidement à partir de données encore imprécises, lui suffisent en début de cycle de développement, alors que des prévisions fiables, même si elles sont plus difficiles à obtenir, lui sont nécessaires en conception détaillée. L'approche que nous présentons prend en compte ces différents besoins et contraintes. Elle consiste en une méthode d'évaluation des performances temporelles d'architectures de commande complexes distribuées en réseaux, destinée à accompagner l'architecte tout au long du cycle de développement. Cette méthode est basée sur une modélisation modulaire du comportement temporel de la commande par réseaux de Petri Colorés Temporisés. Pour ce faire, trois temps sont nécessaires dans la modélisation. La modélisation de l'architecture fonctionnelle consiste à représenter les fonctions de commande, et leurs interactions. La modélisation de l'architecture matérielle permet de traduire la topologie et les connexions entre équipements de commandes (automates programmables, réseaux de communication, ...). L'affectation des fonctions de commande aux équipements ainsi que la prise en compte des communications entre ces fonctions via des réseaux de communication constitue le modèle de l'architecture opérationnelle. Une fois le modèle de comportement de l'ensemble de l'architecture opérationnelle constitué, l'évaluation des performances temporelles est réalisée par simulation du réseau de Petri obtenu. Pour valider notre approche, nous traitons un exemple significatif à l'aide de la plate forme logicielle Design CPN. Cette étude de cas nous permet de présenter une série d'études portant sur la convergence de nos modèles, sur la sensibilité des résultats de simulation aux erreurs de paramétrages et sur la précision des performances obtenues par simulation en les confrontant à celles mesurées sur le système réel.

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.