Les langages formels sont des séquences sur un ensemble discret de symboles appelé alphabet. On les spécifie souvent par des formules dans une certaine logique, par des expressions rationnelles ou bien par des automates discrets de types variés. La théorie actuelle est principalement qualitative, dans le sens où ses objets sont des séquence sur un temps discret, non-métrique, dans le sens où l'acceptation d'une séquence sur un automate dépend du fait que l'on visite ou non un état accepteur, et enfin dans le sens où la comparaison de langages est plus souvent considérée en termes d'inclusion, plutôt qu'en termes de mesures quantitatives. Cette thèse contribue à l'étude de ces aspects souvent négligés en présentant des résultats fondamentaux dans trois nouvelles classes de problèmes quantitatifs sur les langages formels. Dans la première partie, nous étudions une classe de problèmes d'ordonnancement qui combine les aspects structurels associés aux dépendances entre tâches avec les aspects dynamiques liés au fait qu'un flux de requêtes arrive en continu pendant l'exécution. Nous montrons que, dans cette classe de problèmes, certains flux, pourtant admissibles dans le sens que les requêtes ne représentent pas plus de travail que ce que les machines peuvent traiter, ne peuvent pas être ordonnancé avec une latence bornée. Cependant nous développons une politique d'ordonnancement que peut garantir une accumulation de retard bornée pour tout flux de requêtes admissible, même sans le connaître à l'avance. Nous montrons que si les flux sont sous-critiques, alors cette même politique peut garantir une latence bornée. En vérification quantitative, les états et transitions d'un système peuvent être associés à des coûts, et ceux-ci utilisés pour associer des coûts moyens aux comportements infinis. Dans cette seconde partie, nous proposons de définir des omega-langages par des requêtes booléennes sur les coûts moyens. Des spécifications concernant des moyennes, tels que " le taux de perte moyen de messages est inférieur à un certain seuil " ne sont pas omega-régulières, mais exprimables dans notre modèle. Ainsi, nous étudions l'expressivité et la complexité de Borel de telles spécifications. Nous montrons que pour la clôture par intersection, il est nécessaire de considérer des coûts multi-dimensionnels. Nous mettons en évidence que dans le cas général, les conditions d'acceptation portent sur l'ensemble des points d'accumulation de la séquence des coûts moyens des préfixes d'une exécution, et nous donnons une caractérisation précise de tels ensembles. Nous proposons une classe de langages de coût moyen à seuils multiples, comparant les coordonnées minimales et minimales des points de cet ensemble à des constantes. Nous montrons enfin que cette classe est close par opérations booléennes et analysable. Enfin, dans le dernier volet, nous définissons deux mesures pour un langage temporisé : le volume de ses sous-langages de mots à nombre d'événements fixe et l'entropie (vitesse de croissance), mesure asymptotique pour un nombre non borné d'événements. Ces mesures peuvent être utilisées pour la comparaison quantitative de langages, et l'entropie peut être vue comme la quantité d'information par événement dans un mot typique du langage temporisé. Pour les langages acceptés par des automates temporisés déterministes, nous donnons une formule exacte pour le volume. Ensuite, nous caractérisons l'entropie, en utilisant des méthodes d'analyse fonctionnelle, en tant que logarithme du rayon spectral d'un opérateur intégral positif. Nous établissons plusieurs méthodes pour calculer l'entropie : une symbolique pour les automates que nos appelons " à une horloge et demie ", et deux numériques : une utilisant les techniques d'analyse fonctionnelle, l'autre basée sur la discrétisation. Nous donnons une interprétation de l'entropie en théorie de l'information en termes de complexité de Kolmogorov.

Nous considérons une sous classe d'automates temporisés probabilistes où les contraintes temporelles au niveau des gardes et des invariants sont exprimées par des paramètres. Cette sous classe est appelée la classe des automates Temporisés Probabilistes Paramétrés Semi Déterminés (ATPP Semi Déterminés). Cette classe d'automates se définit en particulier par l'attribution d'une unique distribution à chaque état et par des gardes de la forme x<=a où a est un paramètre ou un entier naturel. Nous imposons de plus deux propriétés sur ces automates qui sont celles de non blocage et fortement non zenon. Notre travail vise à calculer le temps moyen maximal de convergence vers un état dit absorbant q_end dans ce type d'automates. L'unique méthode traitant déjà ce type de problème fait appel à la discrétisation du temps et à l'application de techniques de programmation linéaire. Elle est cependant exponentielle car elle dépend du nombre d'horloges et de la plus grande constante à laquelle sont comparées les horloges, lors de la discrétisation. Le graphe résultant peut être de taille exponentielle. Pour tout ATPP Semi Déterminé, on définit un automate totalement déterministe, appelé ATPP Déterminé, en remplaçant toute garde de la forme x<=a par une garde de la forme x=a. Le temps d'attente en chaque état est ainsi fixé par la valuation de l'état initial qui remet toutes les horloges à zéro. Nous démontrons que le temps moyen de convergence vers q_end dans l'ATPP Déterminé est égal au temps moyen maximal de convergence dans l'ATPP Semi Déterminé dont il découle. Pour calculer le temps moyen de convergence vers q_end nous construisons à partir de l'ATPP Déterminé un graphe appelé "graphe des macro-steps" qui contient de façon concise l'information nécessaire au calcul du coût moyen de convergence vers q_end. Ce graphe est de taille polynomiale et se construit en temps polynomial. Le calcul du temps moyen de convergence dans le graphe des macro-steps est solution d'un système linéaire, comme dans le cas des chaînes de Markov avec coûts. On résout ce système linéaire en temps polynomial, ce qui permet d'obtenir finalement le temps moyen maximal de convergence vers q_end dans l'ATPP Semi Déterminé. Nous appliquons enfin cette méthode à certains protocoles de communication, notamment BRP (Bounded Retransmission Protocol) et CSMA/CD (Carrier Sense Multiple Access with Collision Detection).

Ce travail propose une méthode pour l'analyse de systèmes temps-reél. <br />Cette méthode est basée sur la compilation des spécifications<br />vers des graphes temporisés, à partir desquels il est possible<br />de vérifier des propriétés et de générer du code exécutable.<br /><br />Les graphes temporisés sont des automates étendus avec des<br />variables, appelées horloges, qui permettent de décrire les<br />contraintes temporelles. <br /><br />Un algorithme de compilation est développé pour l'algèbre<br />de processus temporisés ATP, qui est une extension des <br />algèbres de processus avec des opérateurs temporels comme <br />le ``timeout'' et le ``watchdog''. L'intérêt de l'algorithme est <br />que la taille du graphe obtenu est indépendante des valeurs <br />des paramètres des opérateurs temporels.<br /><br />Les propriétés temps-reél sur les graphes temporisés sont <br />décrites par des formules de la logique TCTL. <br />Il est montré que les opérateurs temporels<br />de TCTL s'expriment en termes de points fixes à l'aide d'un <br />opérateur ``d'état suivant'' défini de façon appropriée.<br />De plus, ce travail propose un algorithme de vérification qui<br />consiste à évaluer symboliquement l'ensemble caractéristique<br />d'une formule comme une disjonction de contraintes linéaires<br />sur les horloges.<br /><br />Les algorithmes de compilation et de vérification développés <br />ont été implémentés dans l'outil KRONOS, <br />utilisé pour analyser des applications temps-reél <br />significatives. Les résultats obtenus confirment l'intérêt<br />pratique de l'approche proposé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.

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.

Notre travail de recherche concerne l'étude du diagnostic à base de modèles pour les systèmes temporisés et pour une sous-classe de systèmes dynamiques hybrides. Nous avons d'abord développé une méthode de diagnostic basée sur la compilation hors-ligne d'un diagnostiqueur à partir du modèle automate temporisé du système à diagnostiquer. Une méthode systématique permettant la vérification de la diagnosticabilité du modèle utilisé est ensuite donnée. Nous avons ensuite proposé une méthode de diagnostic pour une sous-classe de systèmes dynamiques hybrides modélisés par des automates hybrides rectangulaires. Cette méthode repose sur l'utilisation d'une procédure de diagnostic en-ligne qui estime l'état courant du système ainsi que les occurrences des défauts non-observables. Enfin, nous avons proposé une méthode de vérification de la diagnosticabilité du langage temporisé accepté par un automate hybride rectangulaire vérifiant les hypothèses considérées dans notre travail.

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.