Cette thèse présente les fondements théoriques et pratiques d'un système pour l'analyse statique de langages manipulant des documents et données XML. Le système s'appuie sur une logique temporelle de point fixe avec programmes inverses, dérivée du mu-calcul modal, dans laquelle les modèles sont des arbres finis. Cette logique est suffisamment expressive pour prendre en compte les langages réguliers d'arbres ainsi que la navigation multidirectionnelle dans les arbres, tout en ayant une complexité simplement exponentielle. Plus précisément, la décidabilité de cette logique est prouvée en temps 2^O(n) où n est la taille de la formule dont le statut de vérité est déterminé.<br /><br />Les principaux concepts de XML sont traduits linéairement dans cette logique. Ces concepts incluent la navigation et la sémantique de sélection de noeuds du langage de requêtes XPath, ainsi que les langages de schémas (incluant DTD et XML Schema). Grâce à ces traductions, les problèmes d'importance majeure dans les applications XML sont réduits à la satisfaisabilité de la logique. Ces problèmes incluent notamment l'inclusion, la satisfaisabilité, l'équivalence, l'intersection, le recouvrement des requêtes, en présence ou en l'absence de contraintes régulières d'arbres, et le typage statique d'une requête annotée.<br /><br />Un algorithme correct et complet pour décider la logique est proposé, accompagné d'une analyse détaillée de sa complexité computationnelle, et des techniques d'implantation cruciales pour la réalisation d'un solveur efficace en pratique. Des expérimentations avec l'implantation complète du système sont présentées. Le système apparaît efficace et utilisable en pratique sur plusieurs scénarios réalistes.<br /><br />La principale application de ce travail est une nouvelle classe d'analyseurs statiques pour les langages de programmation utilisant des requêtes XPath et des types réguliers d'arbres. De tels analyseurs permettent de s'assurer, au moment de la compilation, de propriétés importantes comme le typage correct des programmes ou leur optimisation, pour un traitement plus sûr et plus efficace des données XML.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00133591 |
| Date | 04 December 2006 |
| Creators | Genevès, Pierre |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.1929 seconds