Ce travail montre comment un formalisme logique, la logique de configuration, est intégré au sein d'un outil de gestion de configuration de réseaux, ValidMaker. Le principal objectif de ce travail est de démontrer que la logique de configuration est particulièrement bien adaptée à la vérification automatique de configuration de réseaux. À cette fin, nous développons un exemple réel de configuration de réseaux et nous trouvons des règles qui doivent être vérifiées pour qu'une telle configuration soit fonctionnelle. Ensuite, nous expliquons comment nous avons implanté la logique de configuration dans ValidMaker et nous illustrons le fonctionnement de notre algorithme de vérification.

La responsabilité des routeurs s'engage lorsque les machines hôtes envoient leurs paquets dans le réseau. Les routeurs auront donc la fonction de transmettre ces paquets sur les liens pour les acheminer vers la destination déterminée. Cependant, comme le routeur traite les paquets séparément, la performance du routeur dépend donc du temps de traitement pour chaque paquet. Avec une charge de trafic, il est possible d'optimiser efficacement le traitement des paquets dans le routeur. Notre attention sera portée sur l'évaluation du délai de bout-en-bout dans le réseau End-to-End. Ce mémoire propose donc un modèle qui consiste à évaluer et vérifier les délais des paquets dans les routeurs par la méthode de vérification de modèles (Model-Checking). ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : vérification de modèles, Model-Checking, réseaux, routeur, délai.

Depuis quelques années, de nombreux champs de l'informatique ont été transformés par l'introduction d'une nouvelle vision de la conception et de l'utilisation d'un système, appelée approche déclarative. Contrairement à l'approche dite impérative, qui consiste à décrire au moyen d'un langage formelles opérations à effectuer pour obtenir un résultat, l'approche déclarative suggère plutôt de décrire le résultat désiré, sans spécifier comment ce «but» doit être atteint. L'approche déclarative peut être vue comme le prolongement d'une tendance ayant cours depuis les débuts de l'informatique et visant à résoudre des problèmes en manipulant des concepts d'un niveau d'abstraction toujours plus élevé. Le passage à un paradigme déclaratif pose cependant certains problèmes: les outils actuels sont peu appropriés à une utilisation déclarative. On identifie trois questions fondamentales qui doivent être résolues pour souscrire à ce nouveau paradigme: l'expression de contraintes dans un langage formel, la validation de ces contraintes sur une structure, et enfin la construction d'une structure satisfaisant une contrainte donnée. Cette thèse étudie ces trois problèmes selon l'angle de la logique mathématique. On verra qu'en utilisant une logique comme fondement formel d'un langage de « buts », les questions de validation et de construction d'une structure se transposent en deux questions mathématiques, le model checking et la satisfiabilité, qui sont fondamentales et largement étudiées. En utilisant comme motivation deux contextes concrets, la gestion de réseaux et les architectures orientées services, le travail montrera qu'il est possible d'utiliser la logique mathématique pour décrire, vérifier et construire des configurations de réseaux ou des compositions de services web. L'aboutissement de la recherche consiste en le développement de la logique CTLFO+, permettant d'exprimer des contraintes sur les données, sur la séquences des opérations d'un système, ainsi que des contraintes dites «hybrides». Une réduction de CTL-FO+ à la logique temporelle CTL permet de réutiliser de manière efficace des outils de vérification existants. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Méthodes formelles, Services web, Réseaux.

Cette thèse traduit un premier aboutissement de 3 armées d'études et de réalisations dans le domaine de la télé-informatique en général et du réseau d'ordinateurs CYCLADES en particulier. Nous avons abordé les différentes étapes de ce projet en complète et étroite collaboration. En particulier la conception général du frontal réalisé a été le fruit d'échanges constants d'idées et de critiques entre nous. Par suite il aurait été irréaliste de séparer artificiellement le travail effectué en deux parties distinctes, même si la réalisation, par souci d'efficacité, a été ponctuellement partagée, selon les goûts momentanés de chacun. C'est pourquoi, il en a résulté un document unique qui reflète mieux l'homogénéité de la recherche. Ce document se veut non seulement une présentation du travail effectué, mais également une réflexion cri tique sur les domaines abordés. Sa rédaction a été partagée selon l'intérêt marqué par chacun pour présenter chacune des parties étudiées. Ainsi, tandis que Jean-François CHAMBON rédigeait les chapitres IV, VI, VII et les annexes, Bernard LE BIHAN se consacrait aux chapitres I, II, III, V et VIII.

Le but de ce travail est de construire un système transportable flexible à cout minimum pouvant aider a la réalisation d'un compilateur pour le langage de commande réseau, qui sera utilise par le réseau CYCLADES