La logique linéaire (LL) permet de prendre naturellement en compte la notion de ressource. Elle est ainsi très expressive : le plus petit fragment propositionnel est déjà NP-complet alors que le plus grand est indécidable car on peut y simuler les modèles de calculs usuels comme les machines à registres. La décidabilité du fragment multiplicatif exponentiel de LL (MELL) est un problème ouvert. Cette thèse établit la complétude de la sémantique des phases semi-linéaire pour le fragment de Horn de MELL. La prouvabilité dans ce dernier est équivalente à l'accessibilité dans les réseaux de Pétri. Ce résultat constitue une première étape vers l'éventuelle décidabilité de MELL (conjecture de Y.Lafont). Le chapitre suivant développe le codage du problème des circuits hamiltoniens où la notion de choix (qui est ici naturellement traduite par les connecteurs additifs) est gérée multiplicativement. Ce procédé pourrait être étendu à l'étude d'autres problèmes de théorie des graphes. On obtient ainsi une nouvelle preuve de la NP-complétude du fragment multiplicatif de la logique linéaire. C'est un travail réalisé en commun avec T.Krantz. Enfin, on donne un critère de correction quadratique pour les réseaux de preuves de la logique non-commutative de P.Ruet (qui contient la logique linéaire et la logique linéaire cyclique). Il permet de plus de traiter les réseaux de preuve avec coupures.

Le travail présenté dans le mémoire traite des problèmes liés au contrôle d'exécution des actions des robots mobiles autonomes. Une première partie présente l'architecture de contrôle globale et la compare à d'autres approches. On décrit les niveaux hiérarchiques qui la constituent et leurs rôles dans le fonctionnement du système. Le niveau inférieur, composé d'un ensemble de modules, rassemble les fonctions de perception, de modélisation et d'action du système. La seconde partie présente le niveau exécutif. L'exécutif doit suivre l'exécution des fonctions, résoudre les conflits entre modules, accomplir certaines actions réflexes et maintenir une information sur l'utilisation des ressources non partageables du robot. Il peut être vu comme un ensemble d'automates, qui interagissent et changent d'état selon les requêtes qui arrivent du niveau supérieur et les répliques qui proviennent des modules. La mise en oeuvre de l'exécutif utilise le système à base de règles KHEOPS. La compilation faite par KHEOPS permet, à partir d'un ensemble de variables d'entrée et de sortie et des règles qui les relient, d'obtenir un arbre de décision équivalent et de profondeur connue, ce qui garantit un temps d'exécution borné pour l'exécutif. La compilation permet aussi de garantir certaines propriétés logiques des automates mis en place. La troisième partie présente les relations entre le niveau fonctionnel (modules et exécutif) et la couche immédiatement supérieure, le niveau tache. Ce niveau est basé sur le système PRS, qui transforme des taches de haut niveau d'abstraction en procédures d'actions reconnues par le niveau fonctionnel et surveille leur exécution. Le mémoire présente une équivalence entre un sous-ensemble de PRS et les réseaux de Pétri colorés, ce qui permet de faire une vérification du niveau tache quand l'équivalence existe. Enfin, on présente quelques rés ultats de la mise en oeuvre expérimentale de ces travaux avec le robot Hilare 2.

Nous étudions la modélisation et la validation hors-ligne des applications temps-réel en environnement monoprocesseur, qui prend explicitement en compte l'échange des messages, le partage des ressources et les instructions conditionnelles entre les tâches. Notre objectif est de mettre en évidence l'impact de ces paramètres sur l'analyse des applications. Classiquement, ces applications sont modélisées de façon linéaire, en encapsulant les blocs conditionnels, et les séquences sont utilisées pour leur validation. Nous proposons une approche de modélisation et de validation arborescente, qui permet de considérer de façon explicite les blocs conditionnels, et qui utilise les arbres d'ordonnancement pour la validation. Nous comparons ensuite ces deux approches, et prouvons que les premières sont parfois trop pessimistes, c'est à dire qu'elles peuvent conduire à déclarer certaines applications comme non ordonnançables, alors qu'en réalité elles le sont. Nous commençons par construire un générateur d'arbres d'ordonnancement valides. La complexité du générateur étant exponentielle en fonction du nombre de tâches, cette approche est di cile à mettre en ÷uvre dans la pratique. Nous proposons donc une approche de modélisation bas ée sur les réseaux de Petri. Ce réseau sera utilisé pour générer les arbres valides, par construction du graphe de marquages, et la complexité pourra être réduite grâce à des heuristiques.

Aujourd'hui, les ordinateurs et l'Internet sont partout dans le monde : dans chaque maison, domaine et plateforme. Dans ce contexte, le standard XML s'est établi comme un moyen insigne pour la représentation et l'échange efficaces des données. Les communications et les échanges d'informations entre utilisateurs, applications et systèmes d'information hétérogènes sont désormais réalisés moyennant XML afin de garantir l'interopérabilité des données. Le codage simple et robuste de XML, à base de données textuelles semi-structurées, a fait que ce standard a rapidement envahi les communications medias. Ces communications sont devenues inter-domaines, partant de l'informatique et s'intégrant dans les domaines médical, commercial, et social, etc. Par conséquent, et au vu du niveau croissant des données XML flottantes entre des utilisateurs non-experts (employés, scientifiques, etc.), que ce soit sur les messageries instantanées, réseaux sociaux, stockage de données ou autres, il devient incontournable de permettre aux utilisateurs non-experts de manipuler et contrôler leurs données (e.g., des parents qui souhaitent appliquer du contrôle parental sur les messageries instantanées de leur maison, un journaliste qui désire regrouper et filtrer des informations provenant de différents flux RSS, etc.). L'objectif principal de cette thèse est l'étude des manipulations des données XML par des utilisateurs non-experts. Quatre principales catégories ont été identifiées dans la littérature : i) les langages visuels orientés XML, ii) les Mashups, iii) les techniques de manipulation des données XML, et iv) les DFVPL (langages de programmation visuel à base de Dataflow), couvrant différentes pistes. Cependant, aucune d'entre elles ne fournit une solution complète. Dans ce travail de recherche, nous avons formellement défini un Framework de manipulation XML, intitulé XA2C (XML-oriented mAnipulAtion Compositions). XA2C représente un environnement de programmation visuel (e.g., Visual-Studio) pour un DFVPL orienté XML, intitulé XCDL (XML-oriented Composition Definition Language) qui constitue la contribution majeure de cette thèse. XCDL, basé sur les réseaux de Pétri colorés, permet aux non-experts de définir, d'arranger et de composer des opérations de manipulation orientées XML. Ces opérations peuvent être des simples sélections/projections de données, ainsi que des opérations plus complexes de modifications de données (insertion, suppression, tatouage, etc.). Le langage proposé traite les données XML à base de documents ou de fragments. En plus de la définition formelle (syntaxique et sémantique) du langage XCDL, XA2C introduit une architecture complète à base d'un compilateur et un environnement d'exécution dédiés. Afin de tester et d'évaluer notre approche théorique, nous avons développé un prototype, intitulé X-Man, avec un Framework d'évaluation pour les langages et outils visuels de programmation orientés XML. Une série d'études de cas et d'expérimentations a été réalisée afin d'évaluer la qualité d'usage de notre langage, et de le comparer aux solutions existantes. Les résultats obtenus soulignent la supériorité de note approche, notamment en termes de qualité d'interaction, de visualisation, et d'utilisation. Plusieurs pistes sont en cours d'exploration, telles que l'intégration des opérations plus complexes (opérateurs de contrôle, boucles, etc.), les compositions automatiques, et l'extension du langage pour gérer la spécificité des formats dérivés du standard XML (flux RSS, RDF, SMIL, etc.)

Considérons les systèmes à évènements discrets qui sont modélisables par des réseaux de Pétri du type "graphes d'évènements temporisés", Ils ont un comportement optimal (fonctionnement au plus tôt) qui peut-être calculé sans simulation par un système dynamique qui est linéaire dans l'algèbre des dïodes (max,+) ou (min,+). Le comportement asymptotique d'un tel système à évènements discrets est cyclique et les caractéristiques de ce cycle (période, délai, motif) sont analysables par un calcul de valeur propre sur la matrice de dynamique. À partir de cette formulation linéaire, une représentation externe (fonction de transfert) peut-être obtenue grâce à un calcul formel sur des séries à coefficients dans les dïodes, la fonction de transfert d'un tel système est rationnelle au sens des dïoides et est factorisable en une expression finie de polynômes.

L'avenir de la communication est perçu comme étant quasiment exclusivement constitué de nœuds mobiles évoluant dans un réseau mobile. Dans ce contexte, différentes approches contribuent continuellement à l'amélioration directe ou indirecte des délais d'acheminement des informations échangées entre les utilisateurs, dont :- l'analyse des traces;- l'évaluation des performances ;- les services de localisation;- le routage. Nous décrivons chacun de ses thèmes et proposons des solutions faisant évoluer l'état de l'art. Celles-ci prennent appui sur des méthodes et outils tels que :- les Réseaux de Petri, pour l'analyse des traces ;- les modèles de mobilité, pour l'évaluation des performances;- l'introduction du social dans les services de localisation;- la mise en place d'une nouvelle métrique pour le routage. Nous montrons comment ces solutions concourent de façon complémentaire les unes avec les autres, à améliorer l'expérience de l'utilisateur.

De nos jours, les services Web sont très utilisés notamment par les entreprises pour rendre accessibles leurs métiers, leurs données et leurs savoir-faire via le Web. L'émergence des services Web a permis aux applications d'être présentées comme un ensemble de services métiers bien structurés et correctement décrits, plutôt que comme un ensemble d'objets et de méthodes. La composition automatique de services est une tâche complexe mais qui rend les services interopérables, ainsi leur interaction permet d'offrir une valeur ajoutée dans le traitement des requêtes des utilisateurs en prenant en compte des critères fonctionnels et non fonctionnels de la qualité de service. Dans ce travail de thèse, nous nous intéressons plus précisément aux services à base de localisation (LBS) qui permettent d'intégrer des informations géographiques, et de fournir des informations accessibles depuis des appareils mobiles via, les réseaux mobiles en faisant usage des positions géographiques de ces appareils. L'objectif de ce travail est de proposer une approche orientée modèles pour spécifier, valider et mettre en œuvre des processus de composition automatique de services à des fins de sécurité routière dans les transports. Cette approche est basée sur deux outils formels à savoir les Réseaux de Petri (RdP) et l'algèbre (max,+). Pour cela, nous préconisons l'utilisation des workflow patterns dans la composition, où chaque pattern est traduit par un modèle RdP et ensuite par une équation mathématique dans l'algèbre (max,+). Les modèles formels développés ont conduits, d'une part, à la description graphique et analytique des processus considérés, et d'autre part, à l'évaluation et la vérification quantitatives et qualitatives de ces processus. Une plateforme, appelée TransportML, pour la collaboration et l'interopérabilité de services à base de positionnement a été implémentée. Les résultats obtenus par la simulation des modèles formels sont comparés à ceux issus des simulations du fonctionnement de la plateforme et des expérimentations sur le terrain.Cette thèse est effectuée dans le cadre des projets Européens FP7 ASSET (2008-2011) et TeleFOT (2008-2012).

Les rapports d'activité de l'Établissement Français du Sang (EFS) font état d'une demande croissante de produits sanguins labiles (PSL) tels les concentrés globules rouges (CGR), les plaquettes, et le plasma. Afin d'assurer la demande vitale en PSL, il est primordial d'optimiser la logistique liée aux activités de collecte du sang et de ses composants. Pour faire face à cette situation, l'EFS Auvergne-Loire mène une réflexion dans le but d'utiliser de manière plus efficiente les dispositifs de collecte en sites fixes et mobiles pour améliorer (i) la qualité de service rendue au donneur, et (ii) l'efficience de l'utilisation des ressources humaines. Dans ce contexte nous avons développé dans cette thèse des outils opérationnels pour (i) la modélisation des dispositifs de collecte, (ii) la régulation des flux de donneurs, et (iii) la planification de collectes mobiles.La méthode d'analyse des dispositifs de collecte est basée sur des techniques de simulation à événements discrets. Une modélisation préalable des flux de donneurs dans les systèmes de collecte en sites fixes et mobiles à l'aide de réseaux de Petri a été proposée. Pour la régulation de flux de donneurs, notamment pour la planification optimale des rendez-vous des donneurs et la planification de la capacité dans les systèmes de collecte au site fixe, deux approches ont été abordées: (a) Construction d'un algorithme basée sur techniques d'optimisation stochastique via simulation ; (b) Programmation mathématique: Modèle de programmation en nombres entiers non-linéaire (MINLP) basée sur réseaux de files d'attente et représentation et évaluation des systèmes à événements discrets à travers de programmation mathématique. Pour la planification de collectes mobiles. Deux types de modèles ont été développés : (a) Au niveau tactique : Modèles de programmation en nombres entiers linéaire (MIP) pour planifier les semaines de collectes pour chaque ensemble disponible sur un horizon de temps pour garantir l'autosuffisance à niveau régional des CGR. (b) Au niveau opérationnel : Modèle de programmation en nombres entiers linéaire (MIP) pour l'organisation du travail des équipes en charge de la collecte.

De nos jours, les services Web sont très utilisés notamment par les entreprises pour rendre accessibles leurs métiers, leurs données et leurs savoir-faire via le Web. L'émergence des services Web a permis aux applications d'être présentées comme un ensemble de services métiers bien structurés et correctement décrits, plutôt que comme un ensemble d'objets et de méthodes. La composition automatique de services est une tâche complexe mais qui rend les services interopérables, ainsi leur interaction permet d’offrir une valeur ajoutée dans le traitement des requêtes des utilisateurs en prenant en compte des critères fonctionnels et non fonctionnels de la qualité de service. Dans ce travail de thèse, nous nous intéressons plus précisément aux services à base de localisation (LBS) qui permettent d'intégrer des informations géographiques, et de fournir des informations accessibles depuis des appareils mobiles via, les réseaux mobiles en faisant usage des positions géographiques de ces appareils. L'objectif de ce travail est de proposer une approche orientée modèles pour spécifier, valider et mettre en œuvre des processus de composition automatique de services à des fins de sécurité routière dans les transports. Cette approche est basée sur deux outils formels à savoir les Réseaux de Petri (RdP) et l'algèbre (max,+). Pour cela, nous préconisons l'utilisation des workflow patterns dans la composition, où chaque pattern est traduit par un modèle RdP et ensuite par une équation mathématique dans l'algèbre (max,+). Les modèles formels développés ont conduits, d'une part, à la description graphique et analytique des processus considérés, et d'autre part, à l'évaluation et la vérification quantitatives et qualitatives de ces processus. Une plateforme, appelée TransportML, pour la collaboration et l'interopérabilité de services à base de positionnement a été implémentée. Les résultats obtenus par la simulation des modèles formels sont comparés à ceux issus des simulations du fonctionnement de la plateforme et des expérimentations sur le terrain.Cette thèse est effectuée dans le cadre des projets Européens FP7 ASSET (2008-2011) et TeleFOT (2008-2012). / Web services are widely used by organizations to share their knowledge over the network and facilitate business-to-business collaboration. The emergence of Web services enabled applications to be presented as a set of business services well structured and correctly described. However, combining Web services and making them interoperable, to satisfy user requests taking into account functional and non-functional quality criteria, is a complex process. In this work, we focus specifically on location-based services (LBS) that integrate geographic information and provide information reachable from mobile devices, through wireless network by making use of the geographical positions of the devices. The aim of this work is to develop a model driven approach to specify, validate and implement service composition process in an automatic fashion for road security. This approach is based on two formal tools namely Petri nets (PN) and (max, +) algebra used to model, to verify and to evaluate the performance of service composition process. Workflow patterns are used to represent service composition processes. The behavior of each pattern is modeled by a PN model and then by a (max,+) state equation. The developed formal models allow the graphical and analytical description of the considered processes. Also, these models enable to evaluate some quantitative and qualitative properties of the considered processes. A platform, called TransportML, has been developed for collaboration and interoperability of different LBS. The obtained simulation results from the formal models are compared, on one hand, to those obtained from trials of the platform, and on the other hand, to those obtained from the real experimentations on the field.This work is a part of the FP7 European projects ASSET (2008-2011) and TeleFOT (2008-2012).

L'avenir de la communication est perçu comme étant quasiment exclusivement constitué de nœuds mobiles évoluant dans un réseau mobile. Dans ce contexte, différentes approches contribuent continuellement à l'amélioration directe ou indirecte des délais d'acheminement des informations échangées entre les utilisateurs, dont :- l'analyse des traces;- l'évaluation des performances ;- les services de localisation;- le routage. Nous décrivons chacun de ses thèmes et proposons des solutions faisant évoluer l'état de l'art. Celles-ci prennent appui sur des méthodes et outils tels que :- les Réseaux de Petri, pour l'analyse des traces ;- les modèles de mobilité, pour l'évaluation des performances;- l'introduction du social dans les services de localisation;- la mise en place d'une nouvelle métrique pour le routage. Nous montrons comment ces solutions concourent de façon complémentaire les unes avec les autres, à améliorer l'expérience de l'utilisateur. / Future of communication is perceived as being almost exclusively composed of mobile nodes operating in a mobile network. In this context, different approaches contribute to continually improve directly or indirectly, delivery times of information exchanged between users, including:- Trace analysis,- Performance evaluation,- Location services,- Routing.We describe each of these topics and propose solutions by changing the state of the art.These are supported by tools and methods such as:- Petri Nets for Trace analysis,- Mobility Models for Performance evaluation,- Social addings in Location services,- The establishment of metrics for Routing.We show how these solutions work together in a complementary manner with each other, to improve the user experience.