Cette thèse propose une nouvelle technique de vérification par model-checking de propriétés dynamiques PLTL, exprimées au cours d'un processus de spécification de systèmes réactifs par raffinement. La vérification par model-checking a l'avantage d'être entièrement automatisable, mais elle se heurte au problème de l'explosion combinatoire de l'espace d'états à vérifier. Afin de faire face à ce problème, nous proposons de découper par partition l'espace d'états en un ensemble de modules, et de mener la vérification successivement sur chacun des modules, afin de pouvoir conclure sur le modèle dans son ensemble. Nous prouvons que cette méthode de vérification (appelée vérification modulaire) est valide pour tout une classe de propriétés PLTL, que nous caractérisons par des automates de Büchi. Nous présentons les systèmes d'événements B comme cadre d'application de cette technique. Nous proposons une méthode de découpage en modules guidée par le processus de raffinement B.

À l'heure actuelle, les dispositifs embarqués regroupent une grande variété d'applications, ayant des fonctionnalités complexes et demandant une puissance de calcul de plus en plus importante. Ils évoluent actuellement de systèmes multiprocesseur sur puce vers des architectures many-core et posent de nouveaux défis au développement de logiciel embarqué. En effet, Il a classiquement été guidé par les performances et donc par les besoins spécifiques des plates-formes. Or, cette approche s'avère trop couteuse avec les nouvelles architectures matérielles et leurs évolutions rapprochées. Actuellement, il n'y a pas un consensus sur les environnements à utiliser pour programmer les nouvelles architectures embarquées. Afin de permettre une programmation plus rapide du logiciel embarqué, la chaîne de développement a besoin d'outils pour la mise au point des applications. Cette mise au point s'appuie sur des techniques d'observation, qui consistent à recueillir des informations sur le comportement du système embarqué pendant l'exécution. Les techniques d'observation actuelles ne supportent qu'un nombre limité de processeurs et sont fortement dépendantes des caractéristiques matérielles. Dans cette thèse, nous proposons EMBera~: une approche à base de composants pour l'observation de systèmes multiprocesseurs sur puce. EMBera vise la généricité, la portabilité, l'observation d'un grand nombre d'éléments, ainsi que le contrôle de l'intrusion. La généricité est obtenue par l'encapsulation de fonctionnalités spécifiques et l'exportation d'interfaces génériques d'observation. La portabilité est possible grâce à des composants qui, d'une part, ciblent des traitements communs aux MPSoCs, et d'autre part, permettent d'être adaptés aux spécificités des plates-formes. Le passage à l'échelle est réussi en permettant une observation partielle d'un système en se concentrant uniquement sur les éléments d'intérêt~: les modules applicatifs, les composants matériels ou les différents niveaux de la pile logicielle. Le contrôle de l'intrusion est facilité par la possibilité de configurer le type et le niveau de détail des mécanismes de collecte de données. L'approche est validée par le biais de différentes études de cas qui utilisent plusieurs configurations matérielles et logicielles. Nous montrons que cette approche offre une vraie valeur ajoutée dans le support du développement de logiciels embarqués.

La modélisation par points de vue constitue la thématique générale de notre travail de thèse. C'est une approche de modélisation orientée objet, visant l'analyse et la conception des systèmes complexes avec une démarche centrée autour des acteurs interagissant avec le système. Notre équipe a ainsi développé un profil UML appelé VUML (View based UML), qui permet l'élaboration d'un modèle unique partageable à partir de vues associées aux points de vue des acteurs. Cependant, les travaux réalisés sur le profil VUML [Nassar, 05 ; Anwar, 09] ne couvrent pas les aspects comportementaux de la modélisation. En effet, – en proposant la notion de classe multivue – VUML traite les aspects structuraux liés à la composition des vues et au partage des données statiques sans prendre en compte la manière dont ces vues vont réagir, ni comment les synchroniser afin de représenter le comportement des objets multivue (instances d'une classe multivue). Les travaux effectués dans le cadre de cette thèse cherchent à combler ce manque en dotant le profil VUML de nouveaux mécanismes permettant d'exprimer le comportement d'un système. Nous nous sommes concentrés pour cela sur le comportement des objets multivue décrit par des machines à états qui nécessitent des adaptations des concepts de modélisation UML. Pour réaliser cet objectif nous avons introduit la notion de sonde d'événements, qui permet de spécifier des communications implicites entre les vues par observation d'événements. Ceci permet de découpler des spécifications qui sont a priori fortement interconnectées, de les concevoir séparément par points de vue, selon les préconisations de la méthode VUML, puis de les intégrer sans avoir à les modifier. Nous avons tout d'abord défini le concept de sonde d'événements, identifié les différents types de sondes avec les paramètres associés, puis défini un ensemble de concepts permettant d'enrichir et de manipuler les sondes. Nous avons ensuite proposé une représentation compatible avec VUML des concepts introduits sous forme d'un profil nommé VxUML (extension de VUML). En plus de la définition des éléments du profil (stéréotypes, valeurs marquées, classes de librairie prédéfinies), nous avons développé en OCL des règles de bonne formation (sémantique statique). Pour illustrer l'intérêt des concepts introduits, nous avons développé une étude de cas en proposant une modélisation par points de vue complète traitant à la fois les aspects structurel et comportemental. Pour valider concrètement notre approche, nous avons développé, selon une approche IDM, un générateur de code qui prend en entrée une spécification de système en VxUML. Ce générateur utilise les techniques de transformation de modèles liées à la génération de code, et notamment les transformations de modèles indépendants de plate-forme (PIM) vers des modèles spécifiques à une plate-forme (PSM), et des modèles PSM vers le code ; il a été développé dans un premier temps avec le langage cible Java. Sur le plan méthodologique, nous avons défini une démarche associée à VxUML, qui complète celle de VUML, en permettant d'utiliser d'une manière méthodique les mécanismes dédiés au traitement du comportement. Désormais, le processus de développement VxUML permet une modélisation par points de vue complète, traitant à la fois les aspects structurel et comportemental. Mots clés : Conception par points de vue, profil VUML, profil VxUML, sonde d'événements, machine à états multivue, composition du comportement.

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.

Les travaux réalisés dans cette thèse traitent de la gestion des données dans les réseaux inter-véhiculaires (VANETs). Ces derniers sont constitués d'un ensemble d'objets mobiles qui communiquent entre eux à l'aide de réseaux sans fil de type IEEE 802.11, Bluetooth, ou Ultra Wide Band (UWB). Avec de tels mécanismes de communication, un véhicule peut recevoir des informations de ses voisins proches ou d'autres plus distants, grâce aux techniques de multi-sauts qui exploitent dans ce cas des objets intermédiaires comme relais. De nombreuses informations peuvent être échangées dans le contexte des "VANETs", notamment pour alerter les conducteurs lorsqu'un événement survient (accident, freinage d'urgence, véhicule quittant une place de stationnement et souhaitant en informer les autres, etc.). Au fur et à mesure de leurs déplacements, les véhicules sont ensuite " contaminés " par les informations transmises par d'autres. Dans ce travail, nous voulons exploiter les données de manière sensiblement différente par rapport aux travaux existants. Ces derniers visent en effet à utiliser les données échangées pour produire des alertes aux conducteurs. Une fois ces données utilisées, elles deviennent obsolètes et sont détruites. Dans ce travail, nous cherchons à générer dynamiquement à partir des données collectées par les véhicules au cours de leur trajet, un résumé (ou agrégat) qui fourni des informations aux conducteurs, y compris lorsqu'aucun véhicule communicant ne se trouve pas à proximité. Pour ce faire, nous proposons tout d'abord une structure d'agrégation spatio-temporelle permettant à un véhicule de résumer l'ensemble des événements observés. Ensuite, nous définissons un protocole d'échange des résumés entre véhicules sans l'intermédiaire d'une infrastructure, permettant à un véhicule d'améliorer sa base de connaissances locale par échange avec ses voisins. Enfin, nous définissons nos stratégies d'exploitation de résumé afin d'aider le conducteur dans la prise de décision. Nous avons validé l'ensemble de nos propositions en utilisant le simulateur " VESPA " en l'étendant pour prendre en compte la notion de résumés. Les résultats de simulation montrent que notre approche permet effectivement d'aider les conducteurs à prendre de bonnes décisions, sans avoir besoin de recourir à une infrastructure centralisatrice

Mémoire numérisé par la Division de la gestion de documents et des archives de l'Université de Montréal

Dans cet ouvrage nous allons résumer nos activités de recherche depuis l'obtention du titre de docteur à l'Université du Québec à Montréal. Ces recherches ont eu lieu auprès de et ont été possibles grâce à de nombreuses institutions que nous remercions : le BRICS à l'Université de Aarhus, le PIMS et le Département d'Informatique de l'Université de Calgary, le LaBRI de Bordeaux et, enfin, le Laboratoire d'Informatiqu Fondamentale de Marseille et l'Université de Provence. Nous souhaitons illustrer comment la notion de structure, algébrique et d'ordre, peut être un guide fructueux dans l'étude de sujets importants de l'informatique tels que les processus concurrents et les logiques modales et temporales pour la vérification des systèmes informatiques.

Le problème abordé ici concerne l'indexation de données multimédia par la recherche d'extraits pertinents. Nos travaux se focalisent sur l'analyse de séquences vidéo afin d'y détecter des événements prédéfinis. La recherche de ces événements étant contextuelle, nous proposons une architecture et des outils génériques et rapides pour la mise en oeuvre de systèmes d'indexation spécifiques. Nous insistons notamment sur les problèmes suivants : la segmentation temporelle des données, la séparation du fond et des objets, la structuration du fond, le suivi des objets (rigides ou non, avec ou sans apprentissage) et l'analyse des données audio. Afin de résoudre ces différents problèmes, les outils génériques que nous proposons sont basés sur des analyses semi-locales, des approches multirésolution, des modèles de Markov cachées et la méthode des contours actifs. L'architecture et les outils introduits ici ont été validés au travers de plusieurs applications.

L'objectif de ce travail est d'étudier l'exploitation des réseaux haute performance des grappes dans le cadre du stockage distribué. Les applications parallèles s'exécutant sur les grappes nécessitent à la fois des communications performantes entre les différents noeuds et des accès efficaces au système de stockage. Les travaux menés sur les technologies réseau ont abouti à la conception d'architectures dédiées aux grappes qui permettent des communications très rapides entre les noeuds. Les travaux visant à obtenir un stockage distribué efficace dans les grappes se sont pour leur part principalement focalisés sur des mécanismes de parallélisation pour augmenter la charge de travail supportée par le (ou les) serveur. Nous proposons dans ce travail d'améliorer les performances du stockage distribué dans les grappes en utilisant au mieux le réseau haute performance sous-jacent pour accéder au stockage distant. La question générale que nous soulevons est : est-ce que les réseaux rapides des grappes sont adaptés à un accès transparent, efficace et performant au stockage distant ? Nous montrons que les besoins du stockage sont très différents de ceux du calcul parallèle. Les réseaux des grappes ont été conçus pour optimiser les communications entre les différents noeuds d'une application parallèle. Nous étudions leur utilisation dans le cadre, très différent, du stockage dans les grappes, qui s'appuie généralement sur un modèle client/serveur d'accès aux fichiers distants (par exemple NFS, PVFS ou Lustre). Une étude expérimentale reposant sur l'utilisation de GM, l'interface de programmation du réseau rapide Myrinet, dans le contexte du stockage distribué révèle différents freins. Tout d'abord, l'utilisation mémoire particulière dans les couches système d'accès au stockage s'intègre difficilement dans l'habituelle gestion mémoire des réseaux rapides. Ensuite, les modèles client-serveur utilisés dans le stockage distribué présentent des besoins spécifiques pour la gestion des messages et des événements réseau, besoins non couverts par les interfaces actuelles. Nous proposons différentes solutions pour résoudre, au niveau du système de fichiers les problèmes liés au contrôle du réseau mais montrons qu'il est nécessaire de modifier l'interface de programmation réseau et le système d'explotation pour venir à bout des difficultés liées au transfert de données. Nous détaillons des propositions à mettre en oeuvre dans les interfaces de programmation du réseau pour faciliter leur utilisation dans le cadre du stockage. L'intégration dans une nouvelle interface de programmation, Myrinet/MX, d'une gestion souple des transferts de données est présentée. Les premiers résultats montrent que son utilisation dans le cadre du stockage distribué, mais aussi dans d'autres applications, se révèle aisée et efficace.

Les systèmes de commande en réseau (SCR) sont de plus en plus répandus dans le milieu industriel. Ils procurent en effet de nombreux avantages en termes de coût, de flexibilité, de maintenance, etc. Cependant,l'introduction d'un réseau, qui par nature est composé de ressources partagées, impacte considérablement les performances temporelles des systèmes de commande. Un signal de commande par exemple n'arrive à destination qu'après un certain délai. Pour s'assurer que ce délai soit inférieur à un certain seuil de sécurité ou du respect d'autres contraintes temps réels de ces systèmes, une évaluation au préalable, avant la mise en service d'un SCR, s'avère donc nécessaire. Dans nos travaux de recherche, nous nous intéressons à la réactivité des SCR client/serveur et évaluons leur temps de réponse.Notre contribution dans ces travaux est d'adopter une approche analytique à base de l'algèbre (Max,+) et remédier aux problèmes des méthodes existantes comme l'explosion combinatoire de la vérification formelle ou de la non exhaustivité des approches par simulation. Après modélisation des SCR client/serveur à l'aide de Graphe d'Evénements Temporisés puis représentation de leurs dynamiques à l'aides d'équations (Max,+) linéaires, nous obtenons des formules de calcul direct du temps de réponse. Plus précisément, nous adoptons une analyse déterministe pour calculer les bornes, minimale et maximale, du temps de réponse puis une analyse stochastique pour calculer la fonction de sa distribution. De plus, nous prenons en compte dans nos travaux tous les délais élémentaires qui composent le temps de réponse, y compris les délais de bout-en-bout, dus à la traversée du seul réseau de communication. Ce dernier étant naturellement composé de ressources partagées, rendant l'utilisation des modèles (Max,+) classiques impossibles, nous introduisons une nouvelle approche de modélisation à base du formalisme (Max,+) mais prenant en compte le concept de conflit ou ressource partagée.L'exemple d'un réseau de type Ethernet est considéré pour évaluer ces délais de bout-en-bout. Par ailleurs, cette nouvelle méthode (Max,+) est assez générique et reste applicable à de nombreux systèmes impliquant des ressources partagées, au delà des seuls réseaux de communication. Enfin, pour vérifier la validité des résultats obtenus dans nos travaux, notamment la formule de la borne maximale du temps de réponse, une compagne de mesures expérimentales sont menées sur une plateforme dédiée. Différentes configurations et conditions de trafic dans un réseau Ethernet sont considérées.