|
|<
<< Page précédente
1
2
Page suivante >>
>|
|
documents par page
|
Tri :
Date
Editeur
Auteur
Titre
|
|
Université de Franche-Comté
/ 06-04-2006
Couchot Jean-François
Voir le résumé
Voir le résumé
Le prouveur de théorèmes haRVey implante une procédure de décision pour les formules équationnelles non quantifiées dans des théories des tableaux. Ce travail étudie son applicabilité à la vérification, par construction d'invariants, de propriétés de sûreté exprimées sur des systèmes paramétrés. La correction du programme paramétré doit être assurée pour toutes les valeurs des paramètres, interdisant le model-checking. Elle peut s'entreprendre par un calcul de point fixe dont les conditions d'évolution sont déchargées dans un prouveur supportant les formules quantifiées. Graf et Saïdi ont ouvert cette voie en exploitant le prouveur PVS. D'autres ont suivi en exprimant leur système à l'aide de contraintes arithmétiques linéaires obtenues par une abstraction de comptage. Nous proposons un cadre plus basique mais unificateur où les paramètres sont des ensembles finis. Nous montrons que ce cadre convient pour des exemples industriels et des systèmes uniformes distribués. Les spécifications sont écrites dans le langage des machines abstraites B et nous exploitons les calculs de plus faible précondition déjà définis pour cette méthode. Nous introduisons ensuite un calcul de point fixe, obtenu par raffinement d'un calcul de point fixe trivial. Nous proposons ensuite diverses traductions en logique équationnelle des conditions d'évolution, dans l'objectif de faire converger le plus rapidement le prouveur haRVey qui les décharge. Nos expérimentations sur un exemple industriel montrent que la démarche supplante celle du prouveur de l'Atelier B. Théoriquement, nous montrons la décidabilité de certaines obligations de preuve dans le cadre de systèmes uniformes distribués.
|
|
Université de Franche-Comté, UFC, UTBM
/ 26-02-2008
Monticolo Davy
Voir le résumé
Voir le résumé
Ce travail est fondé sur une approche organisationnelle pour la gestion des connaissances lors des projets de conception mécanique. Lors de ces travaux, nous avons pris en compte les aspects sociaux et coopératifs du processus de conception où les acteurs métier travaillent ensemble, créent, utilisent et partagent leurs connaissances pour atteindre le même objectif : le développement d un nouveau système mécanique. Quatre aspects ont été développés dans ce travail : l élaboration d un modèle organisationnel du processus de conception où sont représentés les rôles des acteurs métier, leurs compétences, leurs interactions ainsi que les connaissances qu ils utilisent et partagent tout au long des activités de conception. Ce modèle est un guide pour la capitalisation et la réutilisation des connaissances lors des projets de conception ; la définition d un modèle de mémoire organisationnelle, MemoDesign, fournissant un cadre pour la structuration et l indexation des connaissances à archiver lors des projets de conception ; la construction d une ontologie appelée OntoDesign permettant de manipuler les connaissances du domaine ; la conception et l implantation du système multi-agents "KATRAS" prenant en compte les aspects sociaux et coopératifs du processus de conception et chargé de la construction de mémoires de projet au fil de l eau des projets de conception mécaniques.
|
|
Université de Franche-Comté, UFC, UTBM
/ 08-12-2008
Meignan David
Voir le résumé
Voir le résumé
Un objectif de cette thèse est de fournir des outils d analyse, de conception et d implantation des approches métaheuristiques pour l optimisation combinatoire en les formulant dans le cadre des systèmes multi-agents. L accent est mis sur la potentialité de mise en oeuvre distribuée des approches et sur l utilisation de techniques d apprentissage permettant d adapter dynamiquement des méthodes de recherche. Dans le cadre de cette thèse nous proposons tout d abord, un framework organisationnel et multi-agent pour la modélisation de l implantation de métaheuristiques. Ce framework nommée AMF (Agent Metaheuristic Framework), introduit un modèle organisationnel de métaheuristiques qui donne un cadre d analyse de comparaison et de conception de différentes métaheuristiques. Ensuite, nous présentons une métaheuristique fondée sur la métaphore de la coalition, CMB (Coalition Based Metaheuristic), mettant en avant l intérêt d utiliser les systèmes multi-agents pour la conception de métaheuristiques. Dans cette métaheuristique, la recherche de solution est effectuée par un ensemble d agents regroupés dans une coalition. La structure de coalition permet d intégrer naturellement au système de résolution des aspects de distribution et de décentralisation du contrôle, de même que des procédés d apprentissage individuels et collectifs. L efficacité de notre approche est évaluée expérimentalement en traitant deux problèmes d optimisation combinatoire : un problème de tournées de véhicules et un problème de positionnement.
|
|
Université de Franche-Comté
/ 14-02-2006
Kuroda Kyoko
Voir le résumé
Voir le résumé
Des phrases obtenues à l’issue de traduction montrent des divergences variées et importantes surtout quand il s’agit de langues éloignées comme le japonais et le français. Le but du présent travail est de mettre en évidence la divergence de traduction de ces langues et d’appliquer ce qui en sera dégagé à un système de transfert. Pour ce faire nous nous intéressons particulièrement à leur disparité qui s’observe au niveau de la structure prédicat-arguments. Nous y avons entre autres recensé des changements de catégorie prédicative, changement de voix, une diversification de la distribution actancielle et différentes formes du prédicat actualisé. Ces disparités sont souvent, d’après nous, corrélées et ont des souches communes. Elles peuvent s’expliquer par ce que Pottier appelle statuts événementiels du prédicat, c’est-à-dire que selon que le procès à exprimer est au statif ou à l’évolutif, la façon de le représenter devient différente. Cette différenciation dépend largement du lexique dont chaque langue dispose et des contraintes syntactico-sémantiques que chaque langue impose à son lexique. Nous avons ainsi essayé de dégager des facteurs qui sont à la fois corrélés entre les faits divergents et communs à nos deux langues. Nous les avons par la suite inscrits dans la description de chaque item lexical, en considérant qu’ils permettent au système de transfert de déclencher des opérations qui neutralisent la disparité. Après avoir présenté la formalisation de ces descriptions lexicales qui sont basées sur la grammaire de l’unification, nous montrons le processus de transfert que le système mène à l’aide des indications des facteurs communs
|
|
Université de Franche-Comté, UFC, UTBM
/ 09-12-2008
Oughdi Mustapha
Voir le résumé
Voir le résumé
Le contrôle de la congestion dans les réseaux mobiles dépend de la répartition spatiale et temporelle du trafic. Lorsque la congestion est localisée dans le temps, la tarification est un moyen incitatif efficace pour la redistribution temporelle de la demande. L’objectif est de proposer un modèle de tarification planifiée pour l’optimisation de l’utilisation des ressources du réseau. Le calcul des nouvelles grilles tarifaires se base sur un modèle de comportement des clients. En plus de la modélisation du comportement, l’étude prend en compte la diversité des propriétés de la demande et au dimensionnement non homogène des cellules. Un enjeu de cette étude est alors de montrer dans quelle mesure une grille peut s appliquer à tout ou une partie du réseau et l influence de ce choix sur la décongestion des ressources. Les travaux fondamentaux effectués s appuient d abord sur des probabilités pour modéliser le comportement du client, puis sur des méthodes statistiques, d’analyse de données et de classification automatique pour identifier les propriétés pertinentes des cellules du réseau, et enfin sur des méthodes de partitionnement de graphe pour formaliser le problème de découpage spatial du réseau. Un travail sur les méthodes d’optimisation approchée basées sur la recherche locale et les algorithmes génétiques est réalisé pour l optimisation de l’utilisation des ressources et pour le découpage spatial du réseau. Une étude a été menée sur l’optimisation robuste où l’incertitude sur les données d’entrée du problème est appréhendée par l’examen de la stabilité du modèle vis-à-vis de perturbations sur les données.
|
|
Université de Franche-Comté
/ 28-06-2007
Abbas Amine
Voir le résumé
Voir le résumé
Au cours de ces dernières années a émergé un nouveau type de réseaux sans fil , à savoir les réseaux de capteurs. Une problématique majeure dans ce type de réseaux est la maîtrise de l’énergie consommée par chaque nœud capteur, puisque chaque nœud est alimenté par une batterie. Des mécanismes doivent donc être développés afin d’utiliser à bon escient l’énergie et maintenir le réseau en activité aussi longtemps que possible. Dans cette thèse, nous proposons un algorithme itératif décentralisé pour augmenter la durée de vie d’un réseau de capteurs. L’approche proposée consiste à faire participer chaque nœud proportionnellement à son énergie. Pour cela, à chaque nœud est associé un ratio d’énergies, ratio qu’il s’agira d’équilibrer à travers le réseau en faisant migrer des tâches entre nœuds voisins. L’algorithme a été validé par des simulations en OMNet++, qui mettent en évidence la pertinence de l’approche proposée.
|
|
Université de Franche-Comté, UFC, UTBM
/ 08-12-2008
Gondran Alexandre
Voir le résumé
Voir le résumé
Le problème de planification de réseaux WLAN consiste d'une part à positionner et à paramétrer des antennes dans un bâtiment et d'autre part à leur affecter une fréquence afin d'offrir aux clients un accès sans fil au réseau local. Le réseau ainsi construit doit répondre à des critères de couverture et de qualité de service, tout en minimisant le coût financier. Notre modélisation est basée sur le calcul du débit réel offert en chaque point de demande de service du réseau. Nous montrons que ce critère de débit réel permet une modélisation complète de la qualité de service car il unifie les critères habituels de couverture, de gestion des interférences et de capacité. Notre optimisation traite simultanément le problème de placement des points d'accès et le problème d'affectation de fréquences par un algorithme Voisinages Variables Aléatoires VVA : à chaque itération de cette recherche locale le type de voisinage est tiré au hasard. Cet algorithme est très modulaire et permet facilement de combiner les deux sous problèmes (placement et affection). Ces travaux ont donné lieu à des collaborations et partenariats industriels : logiciel de planification globale des WLAN avec Orange Labs et solutions de planification séquentielle avec la start-up Trinaps. Enfin nous approfondissons la modélisation du problème en explicitant les liens entre le calcul du débit réel et les SINR. Dans une première étape, nous montrons que les contraintes de seuil sur les SINR induisent un problème de T-coloration de graphe (condition nécessaire). Pour obtenir une équivalence rendant compte des interférences multiples, une généralisation du problème de T-coloration pour les hypergraphes est introduite. Dans une seconde étape, nous définissons un algorithme déduisant les seuils de SINR à partir des contraintes sur les débits réels. Cette nouvelle modélisation est la base de nos développements futurs.
|
|
Université de Franche-Comté
/ 30-08-2010
HAJ RACHID Mais
Voir le résumé
Voir le résumé
Le problème de tournées de véhicules est l un des problèmes d optimisation combinatoire les plus étudiés car il a de multiples applications en planification industrielle. La littérature associée est très riche, en variantes de problèmes et en approches de résolution. Face à un problème réel, il est difficile d identifier la classe de problème à laquelle il appartient, de recenser les travaux correspondants, et de déterminer le type de méthode de résolution le plus approprié. Cette thèse étudie la faisabilité d un projet destinée à faciliter ces démarches, en s intéressant plus particulièrement aux approches de résolution évolutionnaires. Il repose sur trois éléments : une notation des variantes de VRP, un recensement d opérateurs évolutionnaires de la littérature, et la construction d une base de règles liant les variantes de problèmes à l efficacité des opérateurs évolutionnaires. L objectif est de guider la conception d un algorithme en fonction des caractéristiques du problème, en proposant les opérateurs qui ont la plus grande probabilité d être efficaces. Appliquer la notation proposée à plusieurs articles montre qu elle permet à chacun de classifier les travaux de manière précise, et d identifier ainsi plus facilement les approches et résultats comparables aux siens. La méthode expérimentale proposée est illustrée en considérant 3 types de croisement et 3 types de mutation. Cette étude montre qu il est possible d estimer quels éléments de l algorithme ont un impact détectable sur les performances, et d établir des relations entre les choix de conception de l algorithme ou entre l instance de problème et l efficacité des opérateurs.
|
|
Université de Franche-Comté
/ 25-06-2009
Alustwani Husam
Voir le résumé
Voir le résumé
Deux problématiques principales ont guidé les travaux de cette thèse:
(a) comment supporter efficacement les interactions (navigation) dans les présentations multimédias streamées et
(b) comment améliorer la disponibilité des données dans un système de streaming P2P ? Afin de permettre une navigation rapide au sein d une présentation multimédia, diffusée en continu, nous avons proposé une approche exploitant les informations disponibles sur son contenu (les objets la constituant). Ces informations permettent, entre autres, de préserver la cohérence sémantique de la présentation lors des interactions utilisateurs. Dans un deuxième temps, nous avons étudié les performances de notre approche en proposant une stratégie de pré-chargement, nommé CPS (Content-Based Prefetching Strategy), qui a permis de réduire considérablement les temps de latence des interactions utilisateurs. La disponibilité des données dans les systèmes de streaming P2P diffère fondamentalement de celle observée dans les systèmes PSP classiques, dans le sens où les données consommées sont dépendantes du temps. Ainsi, cette problématique se pose en terme de possibilité au pair destinataire (consommateur) de pouvoir terminer le visionnage du contenu vidéo dans sa totalité i.e., durant toute la durée de la vidéo. Or, les systèmes P2P spontanés sont essentiellement caractérisés par leur volatilité fréquente, ce qui pose le problème de la disponibilité des pairs sources pendant le streaming. Nous avons étudié cette problématique en mettant en oeuvre, dans un premier temps, un mécanisme de cache centralisé permettant de réduire les effets de la volatilité des pairs et en préservant uniquement les suffixes des vidéos en cours d accès. Dans un deuxième temps, nous avons étendu notre approche vers un cache virtuel distribué. Les résultats des simulations ont montré la pertinence des approches proposées. Enfin, nous avons décrit la conception et la mis en œuvre d un prototype qui démontre la faisabilité d un système de streaming P2P spontané.
|
|
Université de Franche-Comté, UFC, UTBM
/ 30-11-2007
Devarenne Isabelle
Voir le résumé
Voir le résumé
Toutes les méthodes d'optimisation ont des paramètres internes qui prennent une part prépondérante dans leurs performances. La difficulté pour les utilisateurs est de trouver un bon réglage pour chaque problème. Depuis quelques années une part importante de la recherche en optimisation combinatoire porte sur la conception de méthodes adaptives. L'objectif de cette démarche est de définir les procédés qui tentent d'adapter dynamiquement le paramétrage des méthodes en fonction du problème. Dans ce contexte, cette thèse porte sur les mécanismes de mémoire et d'adaptation dans le but de mettre au point une méthode de Recherche Locale Adapative (RLA) combinant des mécanismes d'extension et de restriction du voisinage. L'extension du voisinage est définie par une procédure de détection de blocage de la recherche en étudiant l'historique des choix effectués par la méthode afin d'intervenir sur son comportement. Le mécanisme de restriction quant à lui est basé sur l'utilisation d'une liste Tabou à paramétrage adaptatif pour gérer l'accès aux variables. La méthode ainsi obtenue a été appliquée à deux problèmes : un problème académique, la k-coloration de graphes, et un problème réel, l'affectation de fréquences en réseaux de radiocommunications. Plusieurs variantes de RLA ont élé développées et comparées à des résultats publics sur les deux problèmes.
|
|
|<
<< Page précédente
1
2
Page suivante >>
>|
|
documents par page
|