Thèse de doctorat : Sciences et ingénierie matériaux, modélisation, environnement : Paris 12 : 2004. / Version électronique uniquement consultable au sein de l'Université Paris 12 (Intranet). Titre provenant de l'écran-titre. Bibliogr. : 116 réf.

Reproduction de : Thèse de doctorat : microélectronique : Grenoble, INPG : 1988. / Titre provenant de l'écran-titre. Bibliogr. p. 151-160.

Reproduction de : Thèse de doctorat : Informatique : Toulouse 3 : 2007. / Titre provenant de l'écran-titre. Bibliogr. p. 251-265.

Thèse en accès restreint. Reproduction de : Thèse de doctorat : Informatique : Toulouse 3 : 2007. / Titre provenant de l'écran-titre. Bibliogr. p. 143-154.

Thèse de doctorat : Informatique : Paris 12 : 2007. / Titre provenant de l'écran-titre. Bibliogr. : 79 réf. Index.

Thèse doctorat : Informatique : Rennes 1 : 2008. / Titre provenant de la page du titre du document électronique. Bibliogr. p. 257-264.

Thèse de doctorat : Informatique : Evry-Val d'Essonne : 2008. / Titre provenant de l'écran-titre.

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.

Thèse (de maîtrise)--Université Laval, 2009. / Titre de l'écran-titre (visionné le 16 juin 2009). Bibliogr.

Thèse (Ph. D.)--Université Laval, 2005. / Titre de l'écran-titre (visionné le 15 décembre 2005). Bibliogr.