Projet ANR-14-CE28-0005 – PRODAQ : Systèmes de preuves pour requêtes avec données
Programme : Sciences et technologies logicielles (DS0704) 2014
Année de financement : 2014
Coordinateur du projet : Monsieur Sylvain Schmitz (Laboratoire Spécification et Vérification)
Partenaires : Laboratoire public
Montant : 145080.0 euros
Date de début : 2014
Durée : 60 mois
Résumé : L'archivage et l'accès aux données sur Internet se fait maintenant
sous la forme de données semi-structurées, notemment sous la forme de
documents XML. Dans ce cadre, la brique de base pour accéder aux
données est le langage de requêtes XPath, qui permet de sélectionner
des éléments dans un document XML. Il est omniprésent dans les
langages pour XML comme XSLT ou XQuery, mais aussi dans des langages
généraux comme Java ou C#. Le langage XPath combine la possibilité de
naviguer dans un document XML, héritée de la logique modale, avec
celle de comparer les données trouvées dans plusieurs éléments
distants d'un document. L'analyse statique des requêtes, exprimées en
XPath ou dans une des logiques de données de la même famille, vise à
optimiser et vérifier les requêtes.
La présence de tests sur les données rend la vérification formelle de
requêtes XPath indécidable. La quête de restrictions et de variantes
d'XPath cherche de ce fait à trouver un équilibre entre utilité
pratique (est-ce que les requêtes usuelles peuvent encore être
exprimées dans le langage restreint ?) et possibilité d'une analyse
formelle (peut-on vérifier les requêtes écrites dans le langage
?). Notre objectif général est de fonder rigoureusement des outils
automatiques de vérification des requêtes dans des programmes qui
manipulent des données.
Le projet explore une nouvelle voie inédite à l'interface entre
plusieurs communautés scientifiques, en théorie des bases de données,
vérification de systèmes infinis et théorie de la preuve. La
principale motivation du projet est l'étude de systèmes de preuve pour
les logiques de données, en utilisant en particulier les notions
issues des logiques sous-structurelles. Le projet s'intéresse ce
faisant à plusieurs problèmes ouverts difficiles dans chacune de ces
communautés.
Plus précisément, la première tâche du projet vise à développer des
systèmes de preuve pour les logiques de données. Nous nous inspirerons
en particulier de notions développées pour les logiques modales et les
automates. Le lien entre logiques de données et logiques
sous-structurelles en tant que tel sera l'objet de la seconde tâche,
qui cherche à considérer des structures avec données (comme les
documents XML) comme des modèles de logiques sous-structurelles. La
troisième tâche devrait approfondir l'utilisation de systèmes à
compteurs comme moyens d'obtenir des algorithmes et des complexités
algorithmiques autant pour les logiques de données que pour les
logiques sous-structurelles. En dépit d'un penchant théorique
prononcé, nous souhaitons nous appuyer sur des considérations
pratiques : ainsi, la première tâche devrait aboutir au développement
d'un prototype de vérificateur de requêtes XPath, et nous souhaitons
aussi assembler une suite de tests pour XPath avec données.
Le consortium du projet est basé au Laboratoire Spécification et
Vérification, et inclut deux enseignants-chercheurs ainsi qu'un
chercheur doctorant qui sera financé par le projet. Nous demandons un
financement pour une thèse de trois ans et un financement de visites
de recherche pour nos collaborateurs externes. La durée souhaitée du
projet est de quatre années, ce qui devrait faciliter le recrutement
d'un doctorant.