.

Étude de méthodes de spécification et vérification des protocoles de communication. La méthode de vérification mise en œuvre consiste a évaluer les spécifications du protocole sur un modèle fini qui le représente. Le langage de spécification est basé sur un mu calcul permettant l'expression aussi bien de comportements que de propriétés

Ces dernières années ont vu une croissance phénoménale dans la production et la diffusion des données spatiales de sources aussi variées qu'hétérogènes. Cela a généré des besoins d'intégration dans des entrepôts de données et des perspectives d'analyse exploratoire et de fouille de données spatiales et spatiotemporelles. Nos travaux se placent dans ce contexte visant l'analyse et l'extraction des connaissances depuis les bases de données spatiotemporelles. Ils traitent différents aspects allant de la modélisation avancée des données spatiales, à la fouille de ces données en passant par leur intégration dans un entrepôt, l'optimisation des requêtes et l'analyse en ligne. Ainsi, nous décrivons nos approches pour la modélisation 3D, puis pour la modélisation spatiotemporelle d'objets mobiles. Ensuite, l'intégration de données spatiales est traitées selon deux aspects : l'intégration de formats et l'intégration de données par l'appariement géométrique. Une architecture d'entrepôt de données spatiales basée sur les standards XML et GML est proposée, puis dotée d'une technique d'optimisation de requêtes spatiales basée sur un cache sémantique. L'exploration des données spatiotemporelles a donné lieu à des solutions originales extension de l'OLAP. Enfin, différentes approches sont proposées pour la fouille de données spatiales. Nous avons ouvert le spectre de nos recherches à la fouille d'autres données complexes, telles que les données séquentielles et textuelles. Ces travaux ainsi que les développements futurs sont exposés dans ce mémoire.

Cette thèse se place dans le cadre de la vérification automatique des systèmes distribués. Elle aborde le problème de la spécification pour de tels systèmes, qui consiste à définir un formalisme logique pour décrire des propriétés des comportements de systèmes. On en attend qu'il soit facile d'exprimer les propriétés courantes (accessibilité, sûreté, exclusion mutuelle, vivacité, etc.). On souhaite par ailleurs que la vérification de ces propriétés soient aisée. Il s'agit donc de trouver un compromis entre pouvoir d'expression et simplicité d'utilisation.<br /><br />On s'intéresse ensuite à la modélisation des systèmes concurrents, en recherchant à nouveau un compromis entre réalisme des modèles et facilité de vérification. Les modèles étudiés dans ce travail sont les automates asynchrones, qui modélisent des processus concurrents communiquant par mémoire partagée.<br /><br />La thèse s'intéresse enfin au problème de la synthèse de contrôleur. Étant donné un système spécifié de façon incomplète, donc non-déterministe, en interaction avec un environnement, il s'agit de calculer de manière automatique comment restreindre son comportement afin qu'il vérifie une spécification donnée (quelles que soient les actions de l'environnement). Ce problème se formule en<br />termes de jeux. Dans le cas distribué, les jeux ont naturellement plusieurs joueurs. Dans ce cadre, la plupart des résultats sont négatifs : il est indécidable de savoir si on peut ou non contrôler un tel système. Cette thèse prouve que certaines propriétés de l'architecture de communication garantissent décidabilité pour toute spécification régulière.

Cette thèse porte sur la réalisation d'une maquette du système CESAR, système d'aide à l'analyse d'applications réparties. L'outil réalisé permet de comparer une application décrite par un programme parallèle avec ses spécifications données par un ensemble de formules d'une logique temporelle.

L'étude des données hydrologiques et biogéochimiques (fCO2, CT, nutriments et chlorophylle-a) récoltées entre Hobart et Dumont D'Urville d'octobre à mars (4 trajets en 1996/97 et 8 en 2002/03) montre que :<br />La région subantarctique (43-53°S) est un puits intense de CO2 au printemps comme en été et la variabilité interannuelle n'y semble pas significative.<br />La région située au sud de 62°S présente une forte variabilité spatio-temporelle due en grande partie à l'influence des glaces.<br />La zone ouverte de l'océan Austral (POOZ) présente la variabilité estivale interannuelle la plus importante: En février elle est presque à l'équilibre en 1997 (–0.3 mmol.m-2.j-1) et présente un puits intense en 2003 (–20.6 mmol.m-2.j-1). Une augmentation de la biomasse phytoplanctonique est à l'origine de ce puits. L'exploitation de différents paramètres révèle que l'augmentation de biomasse n'a pas pu être favorisée par une augmentation de SST, ni par un régime mélange/lumière ou par un contenu intégré d'ozone stratosphérique différents. Par contre, les processus à l'origine de cet accroissement semblent être liés à la présence d'un évènement ENSO en 2002/03 et à des apports de fer épisodiques provenant d'Australie.

DORIS (Détermination d'Orbite et Radio positionnement Intégré sur Satellite) est un des systèmes permanents d'observation de la Terre avec le Global Positioning System (GPS) et la télémétrie laser sur satellite (SLR). La richesse des mesures collectées par ces systèmes permet de représenter le déplacement des stations au sol sous forme de séries temporelles de coordonnées. Au delà de la modélisation déterministe habituelle des phénomènes géophysiques, un nouveau domaine de recherche en géodésie s'est ouvert il y a quelques années, visant à la validation et à l'interprétation de ces séries temporelles.Dans la première partie du mémoire on décrit l'intégration de la fonction de mesure DORIS dans le logiciel de traitement GPS de l'Université de Berne.La partie principale des recherches effectuées concerne l'étude et la mise en oeuvre d'une méthode d'analyse de séries géodésiques 3D allant au delà des approches classiques que sont la répétitivité ou la recherche de périodicités et de ruptures. La méthode fait appel à des outils empruntés à d'autres disciplines : l'Analyse en Composantes Principales aux statistiques des sondages, et la variance d'Allan à la métrologie du temps et des fréquences. Elle est testée sur un certain nombre de jeux de séries temporelles de coordonnées de stations DORIS et GPS. On obtient une batterie de diagnostics qualifiant le spectre des mouvements de station et celui des erreurs de mesure. Ces diagnostics permettent la description déterministe et statistique du mouvement des stations obtenu par les analyses de géodésie spatiale. Ils conduisent aussi à une différenciation des systèmes de positionnement DORIS et GPS par leur signature spectrale.

Ce travail s'inscrit dans la continuité de l'étude du langage de description de systèmes AltaRica. Ce langage, développé au Labri, permet de modéliser des systèmes réels de manière hiérarchique. L'objectif de la thèse est d'introduire le temps quantitatif dans le but de concevoir des systèmes temps réel, c'est à dire des systèmes assujettis à des contraintes temporelles.<br />Deux extensions du langage sont proposées : une version temporisée et une hybride. Ces extensions respectent les caractéristiques du langage initial et conservent les aspects de hiérarchie, de synchronisation, de partage de variables et de priorité statique. En outre, afin d'améliorer les descriptions temps réel, de nouveaux opérateurs de modélisation, comme l'urgence et les priorités temporelles, ont été ajoutés. Nous obtenons ainsi un langage hiérarchique de haut niveau de modélisation de systèmes temps réel. <br />Une étude formelle complète a été menée sur la sémantique du langage, le pouvoir d'expression des langages AltaRica temps réel et des moyens de traductions automatiques vers des modèles classiques existants. Ces algorithmes reposent sur la notion de mise à plat de modèle, i.e. réécrire le modèle sans sous composant.<br />Enfin, le langage temporisé est implanté dans un prototype qui étant donné un modèle le met à plat puis le traduit en automate temporisé. Ainsi, certains systèmes réels ont pu être modélisés puis des propriétés ont été vérifiées à l'aide du model checker UPPAAL.

Les données temporelles sont fréquemment manipulées dans plusieurs domaines d'application (bancaire, clinique, géographique, etc.). Malgré la diversité des techniques proposées pour visualiser ce type de données, nous constatons un manque d'approches et de méthodes de conception. Dans cette thèse, nous proposons une approche de conception de techniques de visualisation et plus généralement d'interaction avec des espaces de données temporelles. Pour garantir l'utilisabilité de ces techniques, nous proposons de prendre en compte les caractéristiques des données manipulées et les tâches utilisateur, nous situant ainsi à la jonction de deux domaines de l'informatique : les Bases de Données et les Interfaces Homme-Machine. Ce travail contribue donc à la conception de systèmes interactifs pour l'analyse visuelle de données temporelles. Dans ce contexte, nous proposons une taxonomie qui organise les travaux existants de visualisation de données temporelles selon leur processus de visualisation. Cette taxonomie est construite à partir du processus de visualisation proposé par Chi. En collaboration avec des utilisateurs géographes, nous avons identifié une liste de tâches utilisateur pertinentes pour la manipulation de données temporelles. A partir de cette liste, nous avons conçu et implémenté cinq techniques d'interaction adaptées aux tâches identifiées. Nous avons intégré ces techniques pour développer INVEST (Interactive Visualization and Explorative System of Temporal data) qui est une plate-forme multi-techniques pour l'analyse visuelle de données temporelles. Chaque technique de visualisation est une vue du même espace de données. INVEST inclut un moteur de sélection de techniques de visualisation en fonction des tâches utilisateur spécifiées.

Les travaux de cette thèse ont pour cadre l'édition de documents électroniques multimédia en considérant en tout premier lieu leur dimension temporelle (enchaînement des objets dans le temps). L'objectif concerne à la fois l'intégration de cette nouvelle dimension dans la structure globale d'un document (logique, spatiale et hypertexte) et l'intégration d'objets de base qui ont eux-mêmes une dimension temporelle (vidéo, audio, interactions de l'utilisateur ..). Les documents visés sont donc multimédia, temporisés et interactifs. Notre étude a porté tout d'abord sur la définition d'un langage temporel multimédia. Celui-ci permet de spécifier, de façon déclarative, le scénario temporel d'un document en s'appuyant sur des résultats obtenus dans le domaine de la satisfaction de contraintes temporelles et de la planification. Nous avons ensuite conçu des mécanismes d'analyse qui permettent la vérification de la cohérence d'une spécification tout en prenant en compte trois aspects essentiels aux systèmes multimédia : l'incrémentalité, l'efficacité, et la gestion de l'indéterminisme. Nous proposons des mécanismes de synthèse qui permettent alors le calcul d'une solution qui sera exploitée par le système de présentation. Celui-ci permet, à partir d'un automate d'états finis extrait du graphe temporel de contraintes, d'exécuter la présentation multimédia et de contrôler dynamiquement son déroulement. Enfin, nous présentons l'ensemble des résultats à travers leur application concrète au sein d'un outil d'édition et de présentation appelé Madeus.