Les pièces de formes complexes des domaines aéronautique et automobile sont fabriquées par usinage 5 axes UGV pour accroître leur qualité ou la productivité. Cependant, la gestion combinée du multi-axe et des vitesses élevées posent divers problèmes au couple MO-CN lors de l'exécution des trajectoires.<br />Ces travaux portent sur l'optimisation de l'usinage 5 axes UGV au travers de l'étude des trajectoires et de leur suivi. Après avoir analysé le processus de réalisation des trajectoires et identifié les limites associées, un modèle d'évaluation des performances cinématiques lors du suivi est développé ; il permet de détecter les portions critiques des trajets ainsi que les éléments limitants. Une structure d'optimisation, basée sur un modèle de description surfacique des trajets est ensuite présentée. L'optimisation de l'orientation de l'axe de l'outil, tenant compte des contraintes précédentes y est plus spécifiquement étudiée pour évaluer la faisabilité d'une telle démarche.

Cabri-graphes est un environnement logiciel, destine aux chercheurs, étudiants et enseignants en théorie des graphes. La pratique de cette discipline amené a recourir a des représentations graphiques, afin de visualiser les structures mathématiques mises en œuvre; ceci dans le but de les manipuler, de leur appliquer concrètement certaines transformations, afin de vérifier une propriété, conforter ou infirmer une idée, une conjecture. Cette pratique, menée sur un cahier de brouillon traditionnel, souffre de limitations et les résultats ne sont que faiblement garantis. C'est pourquoi nous avons étudié et réalisé un logiciel, alliant la simplicité d'usage d'un environnement interactif à la puissance de l'ordinateur. Cette thèse présente l'ensemble des concepts mathématiques et de génie logiciel ayant servi a la réalisation de ce projet. Nous donnons en particulier l'implémentation d'un générateur de graphes aléatoires, ainsi que quelques applications motivées et réalisées grâce à cet environnement logiciel

Mes travaux de thèse s'articulaient autour de la validation de modèles et de programmes. En ce sens, les modèles sont validés par animation, de manière à s'assurer qu'ils décrivent le bon comportement du système qu'ils représentent. Il s'agit d'un processus semi-automatique, car l'utilisateur sélectionne les actions du système à exécuter et effectue la comparaison entre les descriptions informelles données dans le cahier des charges et les résultats produits par le modèle. Un modèle validé est ensuite utilisé dans l'objectif de produire des cas de tests fonctionnels destinés à être joués sur une implantation ou un système sous test. Le modèle formel est ainsi utilisé à deux niveaux : d'une part, il permet de calculer de manière automatique les suites de tests, et, d'autre part, il sert d'oracle pour établir le verdict du test.<br />Au cours de ces travaux, nous nous sommes intéressés à la validation de programmes Java par l'intermédiaire de son langage de modélisation associé, nommé JML. Suite aux expériences et aux savoirs-faire accumulés au sein de l'équipe Techniques Formelles et à Contraintes du Laboratoire d'Informatique de Franche-Comté, nous avons choisi d'appliquer une représentation logico-ensembliste des modèles JML, reposant sur des solveurs de contraintes pour gérer les valeurs des variables des modèles objets que nous traitons. A partir de cette représentation symbolique, nous avons exprimé l'animation symbolique d'un modèle objet basé sur la sémantique de Java, utilisant les descriptions formelles contenues dans les pré- et postconditions des spécifications des méthodes.<br />Nous nous sommes ensuite appuyés sur la définition symbolique des états du système objet pour extraire des cibles de tests, liées aux comportements issus des méthodes, définies par un prédicat obtenu par conjonction de la condition d'activation du comportement et de la mise aux limites des attributs des objets du système et des paramètres de la méthode sous test. L'animation symbolique du modèle entre en jeu pour la construction des cas de tests. Un algorithme de parcours de l'espace d'états effectue la recherche d'un chemin d'exécution menant à la cible. Les cas de tests sont ensuite concrétisés pour produire un pilote de test Java. Une étude de cas a été menée sur une modélisation fonctionnelle d'un porte-monnaie électronique.<br />Ces travaux ont été implantés dans un prototype, nommé JML-Testing-Tools, qui permet l'animation symbolique d'un modèle JML et la génération de cas de tests pour l'implantation Java qui lui est associée. Ce prototype est composé d'un compilateur traduisant une spécification JML et des signatures de classes Java dans un format logico-ensembliste. Le modèle décrit dans ce format est ensuite animé par un interpréteur rétablissant la sémantique opérationnelle du Java/JML.

Les systèmes de médiation sont aujourd'hui largement développés et connus. Cependant, leur mise en œuvre pose un certain nombre de problèmes, en particulier la définition de requêtes de médiation en présence d'un grand nombre de sources de données, et d'un volume important de méta-données les décrivant. Ce problème est d'autant plus complexe que les sources sont hétérogènes.<br />Face a cette problématique, nous proposons dans cette thèse pour le contexte relationnel, une approche de génération automatique de requêtes de médiation. A partir de la description d'un ensemble de sources de données distribuées et hétérogènes et de méta-données, notre algorithme produit un ensemble de requêtes de médiation possibles. Nous avons développé un outil qui permet de générer automatiquement des requêtes de médiation dans un environnement hétérogène. Notre objectif principal étant de fournir à l'utilisateur un outil adapté aux petits et grands systèmes, nous avons réalisé une série de tests d'évaluation des performances pour mesurer son passage à l'échelle. Ces tests montrent la faisabilité de notre approche.

Cette thèse propose une nouvelle approche pour le test statistique de<br />logiciel à partir d'une description graphique des comportements du<br />système à tester (graphe de contrôle, statecharts). Son originalité<br />repose sur la combinaison de résultats et d'outils de combinatoire<br />(génération aléatoire de structures combinatoires) et d'un solveur de<br />contraintes, pour obtenir une méthode de test complètement automatisée.<br />Contrairement aux approches classiques qui tirent des entrées, la <br />génération aléatoire uniforme est utilisée pour tirer des chemins parmi<br />un ensemble de chemins d'exécution ou de traces du système à tester. <br />Puis, une étape de résolution de contraintes est utilisée pour <br />déterminer les entrées qui permettront d'exécuter ces chemins.<br />De plus, nous montrons comment les techniques de programmation <br />linéaire peuvent améliorer la qualité d'un ensemble de tests.<br /><br />Une première application a été effectuée pour le test statistique<br />structurel défini par Thévenod-Fosse et Waeselynck (LAAS) et un <br />prototype a été développé.<br />Des expériences (plus de 10000 réalisées sur quatre fonctions issues <br />d'un logiciel industriel) ont été effectuées pour évaluer notre approche <br />et sa stabilité.<br /><br />Ces expériences montrent que notre approche est comparable à celle <br />du LAAS, est stable et a l'avantage d'être complètement automatisée. <br />Ces premières expériences nous permettent également d'envisager un <br />passage à l'échelle de notre approche. Plus généralement, ces travaux <br />pourraient servir de base pour une nouvelle classe d'outils dans le <br />domaine du test de logiciel, combinant génération aléatoire de <br />structures combinatoires, techniques de programmation linéaire et <br />résolution de contraintes.

La première partie de ce mémoire est consacrée à l'énumération de diverses familles de structures arborescentes, en général selon le nombre de sommets. Les trois premiers chapitres sont consacrés à l'étude des arborescences de Cayley telles que la racine est inférieure à ses fils et des arborescences alternantes. La plupart de nos résultats sont prouvés bijectivement. Nous nous intéressons ensuite aux arborescences coloriées, et plus particulièrement à la formule d'inversion de séries formelles multivariées de Good-Lagrange. Nous donnons une nouvelle preuve bijective d'une variante de cette formule et utilisons cette preuve pour prouver combinatoirement diverses formules d'énumération de structures arborescentes et en déduire des algorithmes de génération aléatoire pour ces structures (notamment les cactus planaires). Nous concluons cette première partie par un chapitre consacré aux constellations : en combinant notre preuve de la formule de Good-Lagrange et la conjugaison d'arborescences (due à Bousquet-Mélou et Schaeffer), nous prouvons bijectivement une formule (nouvelle) pour l'énumération de constellations selon le nombre de sommets et de faces. Dans la seconde partie, nous étudions le problème de la recherche de motifs dans une arborescence, en utilisant une structure de données classique pour les mots : l'arborescence des suffixes. Nous proposons notamment un algorithme de recherche de motifs dans une arborescence, basé sur un codage d'une arborescence par des mots et sur l'utilisation de l'arborescence des suffixes d'un de ces mots, qui semble avoir de bonnes propriétés expérimentales. Nous concluons en étendant la notion d'arborescence des suffixes des mots aux arborescences et en décrivant un algorithme de construction pour cette structure.

Ce travail aborde le problème de la validation de spécifications de services téléphoniques et notamment la recherche d'interactions entre services. Une interaction correspond à la modification du comportement d'un ou plusieurs services, du fait de la coexistence des services. L'interaction est un obstacle majeur au développement de l'offre de services de télécommunications. La validation de spécifications requiert une modélisation des services et du réseau sous-jacent. Nous proposons une méthode de spécification formelle et de validation de services. Celle-ci est basée sur l'utilisation d'un formalisme synchrone pour la modélisation et la spécification, et sur la mise en oeuvre de méthodes de test pour la validation. Nous avons à cette fin proposé une méthode de test adaptée au problème. Cette méthode a été intégrée à Lutess, un environnement de test fonctionnel de systèmes réactifs synchrones, reposant sur un principe de génération de données dynamique et aléatoire. Elle est basée sur la notion de "guidage par schémas". Un schéma représente une classe de comportements de l'environnement du système sous test, comportements que l'on souhaite tester principalement, soit parce qu'ils sont réalistes, soit parce qu'ils conduisent à une situation estimée critique. Cette méthode a été formalisée, puis validée expérimentalement dans plusieurs études de cas conséquentes, en particulier lors du premier concours de détection d'interaction proposé en marge de la conférence "Feature Interaction Workshop", qui a consacré Lutess "Meilleur outil pour la détection d'interactions".

Les réseaux de télécommunications évoluent vers des modèles qui consistent en un certain nombre de routeurs IP interconnectés par un réseau optique intelligent. Cette nouvelle infrastructure multicouche nécessite un haut niveau de fiabilité, de telle manière que les services du réseau puissent être rétablis en cas de panne. Dans cette thèse, nous considérons différents problèmes de sécurisation et de dimensionnement liés à cette infrastructure multicouche. Nous donnons des formulations en terme de programmes linéaires mixtes , et nous discutons des polytopes associés. Nous décrivons plusieurs classes d'inégalités valides et étudions les conditions pour qu'elles définissent des facettes. Nous discutons de procédures de séparation pour ces inégalités et induisons des opérations de réduction. Nous développons des algorithmes de coupes et branchements et de coupes génération de colonnes et branchements et présentons une étude expérimentales sur des instances aléatoires et réelles.

Ce travail est consacré à l'étude de la marche d'un robot bipède non actionné au niveau des chevilles. Les mouvements du robot sont réduits au plan sagittal. La spécificité de l'étude actuelle est la prise en compte d'une phase de double support sur actionnée, en plus de la phase de simple support sous-actionnée. Ce travail traite de trois points distincts. Il traite d'abord de l'étude de l'impact du pied libre avec le sol, dans les cas avec et sans pieds. Nous avons trouvé qu'avec le modèle d'impact utilisé le seul moyen d'obtenir un double support était d'éviter l'impact. Cette étude nous a également amené à remettre en cause les hypothèses généralement faites qui conduisent au modèle d'impact que nous avons utilisé, dans le cas où des contacts ont déjà lieu au moment de l'impact. Il traite ensuite de la génération de mouvements de marche que nous avons posée rigoureusement sous la forme d'un problème d'optimisation avec une hiérarchie de contraintes. Cette hiérarchie de contraintes consiste en une suite de contraintes où une contrainte doit être vérifiées pour que les contraintes suivantes soient définies. Une adaptation de programmes d'optimisation existants a été développée afin de tenir compte des spécificités du problème de la génération de mouvements qui a été posé. Le calcul du gradient de manière analytique a également été développé afin d'améliorer le déroulement du processus d'optimisation. Enfin est étudiée la stabilité des dynamiques non commandées en simple support, sachant que la marche inclut la phase de double support sur-actionnée. Des conditions de stabilité sont déterminées ainsi que le domaine d'attraction pour les dynamiques non commandées en simple support. Il est aussi prouvé tout l'intérêt de la phase sur actionnée pour améliorer la stabilité de la marche.

Les avancées récentes en matière d'animation ont permis le déploiement de personnages virtuels à des fins diverses et variées. Les signeurs virtuels sont des personnages en trois dimension s'exprimant en langue des signes et permettant la diffusion de messages aux personnes sourdes et malentendantes signantes de manière anonyme et modulaire. Cependant, la génération d'animations pour ces personnages dépend de la description lexicale des signes, modèle linguistique dépendant du système de génération. Les signes décrits par ces modèles sont généralement des réalisations parfaites et géométriques menant à des mouvements robotiques et peu naturels de la part du signeur. Cette thèse s'intéresse à l'addition d'informations anatomiques au squelette de contrôle du personnage virtuel de manière à le faire signer de manière plus humaine et réaliste. Ces informations supplémentaires sont regroupées sous l'appellation de "modèle anatomique" et sont divisées en cinq contributions principales : une nouvelle représentation informatique du squelette, une étude anthropométrique sur la main, l'unification de dépendances articulatoires, un nouveau modèle de complexe carpo-métacarpien permettant l'opposition aisée du pouce et enfin un modèle calculant le confort d'une posture. Ces apports sont intégrés à une plateforme de génération au moyen de techniques adaptées aux contraintes imposées par les modèles linguistiques. Les travaux sont conclus par une évaluation du système ainsi qu'une réflexion sur les travaux futurs pouvant être élaborés à partir de cette thèse.