Rewrite-Based Verification of XML Updates

Florent Jacquemard 1 Michael Rusinowitch 2
1 DAHU - Verification in databases
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : We propose a model for XML update primitives of the W3C XQuery Update Facility as parameterized rewriting rules of the form: "insert an unranked tree from a regular tree language L as the first child of a node labeled by a". For these rules, we give type inference algorithms, considering types defined by several classes of unranked tree automata. These type inference algorithms are directly applicable to XML static typechecking, which is the problem of verifying whether, a given document transformation always converts source documents of a given input type into documents of a given output type. We show that typechecking for arbitrary sequences of XML update primitives can be done in polynomial time when the unranked tree automaton defining the output type is deterministic and complete, and that it is EXPTIME-complete otherwise. We then apply the results to the verification of access control policies for XML updates. We propose in particular a polynomial time algorithm for the problem of local consistency of a policy, that is, for deciding the non-existence of a sequence of authorized update operations starting from a given document that simulates a forbidden update operation.
Type de document :
Communication dans un congrès
Kutsia, Temur and Schreiner, Wolfgang and Fernández, Maribel. 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), Jul 2010, Hagenberg, Austria. ACM, 2010, 〈http://portal.acm.org/citation.cfm?doid=1836089.1836105〉. 〈10.1145/1836089.1836105〉
Liste complète des métadonnées

Littérature citée [38 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00578916
Contributeur : Florent Jacquemard <>
Soumis le : mardi 22 mars 2011 - 16:30:53
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : jeudi 23 juin 2011 - 02:50:41

Fichier

ppdp06a-jacquemard-HAL.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Florent Jacquemard, Michael Rusinowitch. Rewrite-Based Verification of XML Updates. Kutsia, Temur and Schreiner, Wolfgang and Fernández, Maribel. 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming (PPDP), Jul 2010, Hagenberg, Austria. ACM, 2010, 〈http://portal.acm.org/citation.cfm?doid=1836089.1836105〉. 〈10.1145/1836089.1836105〉. 〈inria-00578916〉

Partager

Métriques

Consultations de la notice

404

Téléchargements de fichiers

134