La vérification formelle de systèmes concurrents temps réels se heurte au problème de l'explosion du nombre d'états à explorer. Ce problème connu sous le nom ``d'explosion combinatoire'' à plusieurs causes. Cette thèse s'intéresse à deux d'entre-elles. · Pour lutter contre l'explosion due à la représentation du parallélisme par l'entrelacement d'actions, cette thèse propose des techniques basées sur l'approche des ordres-partiels pour construire un graphe réduit. Pour exploiter les ordres-partiels, les techniques proposées utilisent la construction de « pas de transitions » afin de limiter le nombre d'états explorés. Différentes constructions des « pas de transitions » sont proposées en fonction de la classe de propriétés que l'on souhaite préserver (Blocages, Équivalence de traces, LTL). · Pour lutter contre l'explosion due aux contraintes temporelles, cette thèse propose une approche par sur-approximation du comportement. L'objectif est d'avoir un graphe abstrait du comportement de la sur-approximation plus petit que celui du système. Comme classiquement, les techniques d'abstractions permettent d'obtenir une procédure de décision semi-effective. Lorsque l'analyse de la sur-approximation ne permet pas de conclure, la thèse propose une méthode effective permettant de conclure pour les formules de LTL: le système est analysé, guidé par les résultats obtenus sur la sur-approximation. Cette thèse présente les algorithmes de ces différentes techniques de réduction et l'outil tina (http://www.laas.fr/tina) dans lequel ils ont été implémentés.

Le mémoire constitue un panorama sur l'évolution des variables d'action pour les systèmes presque intégrables. C'est le problème de la diffusion d'Arnold. J'aborde la construction d'Arnold, ainsi que les méthodes variationnelles issues des travaux plus récents de John Mather. J'explique ce qu'est le large gap problem, et j'introduis la relation d'équivalence sur les variables d'action qui m'a permis d'obtenir une solution à ce problème.

Dans le cadre de la télécommunication, les entreprises développent des protocoles gérant le transfert de données entre machines. Ces protocoles fonctionnent sur le principe d'envoi de messages entre deux parties par l'intermédiaire de canaux non fiables. Pour s'assurer que tous les messages ont bien été reçus, les techniques employées consistent à réémettre les messages perdus et/ou à attendre un laps de temps déterminé avant de conclure à l'échec de la transmission. De plus, les systèmes sont souvent modélisés en fonction de paramètres. Nous avons travaillé sur un modèle mathématique permettant la vérification de spécifications (comportements attendus des systèmes) pour des protocoles manipulant à la fois des compteurs, des files d'attente ou des horloges, ainsi que des paramètres. Le but de l'analyse est de calculer l'ensemble des comportements possibles du système puis de vérifier qu'aucun d'eux ne viole une spécification attendue. Le problème ici est que cet ensemble est infini. En effet, un comportement est fonction des valeurs prises par les variables du système au cours de l'exécution et certaines sont définies sur un domaine infini. Il faut alors pouvoir représenter ces comportements de façon finie et aussi trouver des méthodes pour calculer en un temps fini un ensemble infini. Plus formellement, nous nous sommes placés dans le cadre de l'analyse automatique des systèmes (model-checking). La représentation choisie pour les modèles à compteurs et horloges paramétrés est une extension des matrices de bornes pour laquelle nous avons une méthode exacte d'accélération (calcul en un temps fini d'ensembles de comportements infinis). Du côté pratique, nous avons implanté ces méthodes dans un outil TReX qui est, à notre connaissance, le seul pouvant manipuler de manière exacte des compteurs, des horloges et des files d'attente. Nous avons pu vérifier des exemples conséquents tels que le protocole de retransmission bornée.

L'importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d'application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s'intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d'outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l'influence du flot d'informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l'applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l'angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d'un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d'établir un formalisme permettant la preuve du délai de bout-en-bout lors d'une démarche de développement incrémentale.

Ces dernières années plusieurs maladies infectieuses sont apparues ou ré-apparues. Ce phénomène n'est pas nouveaux et de nombreux facteurs, tels que les changements climatiques, l'intensification des échanges et des voyages, favorisent l'extension, le maintien ou l'émergence de nombreuses maladies infectieuses. L'étude de ces maladies dites (ré-)émergentes est relativement récente (années 1990, concept introduit par S. Morse). Dans cette thèse nous nous intéressons au cas d'une maladie tropical : le Chikungunya. Cette maladie due à un arbovirus (\textit{arthropod-borne virus}) est une maladie vectorielle transmise par les moustiques du genre \textit{Aedes}. Depuis une cinquantaine d'années, plusieurs épidémies ont été recensées, notamment en Afrique et en Asie et plus récemment sur l'île de la Réunion (2005-2006) et en Italie (2007). À l'heure actuelle, il n'est malheureusement pas possible de prédire l'émergence de nouveaux évènements, ceux-ci pouvant être plus ou moins localisés géographiquement, sporadiques ou épidémiques. La modélisation mathématique de ces maladies se révèle donc un atout considérable dans la tentative de compréhension de leur évolution. Ces modèles aident ainsi la prise de décisions et orientent les différentes actions. Dans ce travail nous présentons dans un premiers temps, les caractéristiques biologiques du vecteur et le mode transmission de la maladie à la population humaine. Nous formulons et étudions plusieurs modèles (EDO, Contrôle, EDR) décrivant la dynamique de croissance des différents stades d'évolution du vecteur (œuf/larve/nymphe/adulte) en utilisant des modèles structurés par classes. Cette dynamique est alors couplée à un modèle de transmission de la maladie, décrit par des modèles de type SI-SIR. Différentes stratégies de contrôle, intégrant les techniques de luttes contre la maladie et la prolifération de la population de moustique sont également étudiées. La formulation d'un modèle de type métapopulationnel, décrivant les déplacements humains et vecteurs ainsi qu'une modélisation de l'environnement de l'Île de la Réunion, nous permettent de valider nos modèles grâce à une comparaison aux données de seroprévalence enregistrées et estimées par l'INVS (Institut de Veille Sanitaire).

Les systèmes à commutation constituent un cas particulier des systèmes dynamiques hybrides. Ils sont composés d'une famille de systèmes et d'une loi de commutation qui détermine quel mode est activé à chaque instant. Ces systèmes représentent une large gamme de systèmes concrets. L'étude de la stabilité de ceux-ci a déjà été longuement abordée. Les travaux de cette thèse portent sur l'analyse de performance des systèmes à commutation linéaires en temps discret et sur la synthèse de différentes lois de commande pour ces systèmes en tenant compte de contraintes de performances. L'analyse de stabilité de ces systèmes a été étendue pour tenir compte de l'aspect performance qui a été modélisée par un critère quadratique. La valeur du critère dépendant des commutations, l'analyse porte sur le coût garanti des performances. Grâce à la résolution d'un problème d'optimisation sous des contraintes sous la forme d'inégalités matricielles linéaires, un majorant du coût garanti est déterminé. Une approche est proposée pour évaluer la qualité du majorant trouvé. Un deuxième point abordé est la conception de contrôleurs qui tient compte de l'aspect performance. Des méthodes de synthèse de différents contrôleurs (retour d'état, retour d'état reconstruit par observateur et retour de sortie dynamique) sont proposées dans ce cadre. Enfin, nos résultats ont été appliqués au cas des systèmes contrôlés en réseau.

L'univers actuel de l'entreprise moderne se caractérise par la globalisation des échanges commerciaux et la diversification des acteurs qui le composent. pour survivre dans un tel environnement, l'entreprise doit s'adosser à un ensemble d'entreprises partenaires solides et donc s'intégrer à une structure externe qui lui permette non seulement de subsister dans son environnement concurrentiel, la difficulté de prise de décision réside dans le fait que l'entreprise ne maîtrise pas l'ensemble de ces spécificités. Cela implique le besoin de trouver des moyens de coordinatio capables de limiter les effets " néfastes", c'est-à-dire les incohérences issues de la prise de décision. Ce mémoire aborde le problème de prise de décision pour la satisfaction de commandes imprévues. Il est majeur car la satisfaction de commandes est le but essentiel de toute entreprise en réseau. dans le contexte, la prise de décision est opérationnelle car les délais impartis pour répondre à la commande sont courts. En outre, nous nous plaçons volontairement dans la situation pour laquelle les demandes ne correspondent pas aux prévisions préalablement élaborées. Enfin, les entreprises qui forment le réseau considéré sont de nature autonome dans leurs prises de décisions et dans leur système d'information. Il s'agit alors d'une architecture distribuée. L'objectif de ce travail est d'élaborer des processus et des outils d'aide à la décision pour permettre la satisfaction d'une commande imprévue dans le contexte chaîne logistique distribuée

Les systèmes de production manufacturiers sont une classe des systèmes à événements discrets. Leur taille nécessite de distribuer le logiciel de contrôle sur une architecture industrielle de plusieurs ordinateurs reliés en réseau. Dans ce contexte, il devient essentiel d'être capable d'évaluer l'impact d'une architecture réseau spécifique sur les services des systèmes manufacturiers en termes de la performance et la qualité. Les performances du réseau sous-jacent peuvent notamment nuire à la productivité du système. Dans la méthodologie traditionnelle proposée dans la littérature, cet aspect n'est pas pris en compte au niveau conception. Cependant, la modélisation de tels systèmes est importante pour vérifier certaines propriétés. Dans cette thèse, nous proposons une approche de modélisation par composants à l'aide des réseaux de Petri haut niveau pour la modélisation de certains protocoles de réseaux afin d'évaluer les systèmes manufacturiers comme étant des systèmes distribués. La sélection des réseaux de Petri est justifiée par leur pouvoir d'expression en ce qui concerne la modélisation des systèmes distribués et concurrents. L'approche par composants permet de diminuer la complexité de la modélisation et encourage la généricité, la modularité et la réutilisabilité des composants prêt-à-utiliser. Cela permet de construire facilement de nouveaux modèles et de réduire les coûts de développement de systèmes. En outre, cela peut aider à une meilleure gestion des services et des protocoles et à changer facilement/modifier un élément du système. Notre modélisation permet enfin d'évaluer ces systèmes par le biais de simulations centralisées

Cette thèse a pour but de proposer un algorithme de partitionnement matériel/logiciel optimisé. On travaille sur l'hypothèse de que quelques caractéristiques spécifiques à certains algorithmes déjà publiés puissent être combinées de façon avantageuse, menant à l'amélioration d'un algorithme de partitionnement de base et, par conséquence, des systèmes hétérogènes générés par cet algorithme. L'ensemble d'optimisations proposées pour être réalisées dans ce nouvel algorithme consiste en : généralisation des architecturescible candidates avec l'ajout de FPGA's pour le partitionnement, considération précise des coûts et puissances des fonctions allouées en matériel, ordonnancement de systèmes au matériel dynamiquement reconfigurable, et prise en compte de plusieurs alternatives d'implémentation d'un noeud d'application dans un même processeur. Ces optimisations sont implémentées en versions successives de l'algorithme de partitionnement proposé, lesquelles sont testées avec deux applications de traitement du signal. Les résultats du partitionnement démontrent l'effet de chaque optimisation sur la qualité du système hétérogène obtenu.

La production de systèmes temps-réel répartis embarqués (TR2E) est une opération lourde en temps et en coût de développement. De plus, les applications temps-réel doivent satisfaire des contraintes dures pour assurer leur bon fonctionnement (respect des échéances temporelles...). L'utilisation des langages de description d'architecture vise à réduire le coût de développement de ces applications. AADL (Architecture Analysis & Design Language) fait partie de cette famille de langages. Il propose la notion de ``composant'' (matériel ou logiciel) dont la sémantique bien définie permet de décrire plusieurs aspects d'un système TR2E. Les différentes contraintes qui doivent être satisfaites sont intégrées dans le modèle AADL sous forme de propriétés. Ce travail de thèse exploite les fonctionnalités offertes par AADL pour spécifier les besoins exacts d'une application AADL afin de la produire automatiquement. En effet, le processus de production que nous proposons (1) génère automatiquement le code pour intégrer les composants applicatifs à la plate-forme d'exécution, (2) génère automatiquement une importante partie des composants intergiciels taillés sur mesure pour l'application et (3) déploie automatiquement les composants applicatifs et intergiciels afin d'obtenir un système fortement dédié à l'application. Notamment, la plate-forme d'exécution supportant les composants AADL est elle même configurée statiquement en fonction des propriétés spécifiées. L'approche adoptée réduit le temps de développement et permet d'obtenir un code personnalisé et analysable. La configuration et le déploiement (souvent séparés du processus de développement) sont désormais automatiques et intégrés à la chaîne de production.