Analysis of Schemas with Access Restrictions

Michael Benedikt 1 Pierre Bourhis 2 Clemens Ley 1
2 LINKS - Linking Dynamic Data
Inria Lille - Nord Europe, CRIStAL - Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189
Abstract : We study verification of systems whose transitions consist of accesses to a Web-based data-source. An access is a lookup on a relation within a relational database, fixing values for a set of positions in the relation. For example, a transition can represent access to a Web form, where the user is restricted to filling in values for a particular set of fields. We look at verifying properties of a schema describing the possible accesses of such a system. We present a language where one can describe the properties of an access path, and also specify additional restrictions on accesses that are enforced by the schema. Our main property language, AccLTL, is based on a first-order extension of linear-time temporal logic, interpreting access paths as sequences of relational structures. We also present a lower-level automaton model, A-automata, which AccLTL specifications can compile into. We show that AccLTL and A-automata can express static analysis problems related to " querying with limited access patterns " that have been studied in the database literature in the past, such as whether an access is relevant to answering a query, and whether two queries are equivalent in the accessible data they can return. We prove decidability and complexity results for several restrictions and variants of AccLTL, and explain which properties of paths can be expressed in each restriction.
Type de document :
Article dans une revue
ACM Transactions on Database Systems, Association for Computing Machinery, 2015, 40 (1), pp.Article No. 5. 〈10.1145/2699500〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01211288
Contributeur : Inria Links <>
Soumis le : mardi 6 octobre 2015 - 15:30:58
Dernière modification le : jeudi 11 janvier 2018 - 06:27:32
Document(s) archivé(s) le : jeudi 7 janvier 2016 - 10:15:47

Fichier

BenediktQuerying.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Michael Benedikt, Pierre Bourhis, Clemens Ley. Analysis of Schemas with Access Restrictions. ACM Transactions on Database Systems, Association for Computing Machinery, 2015, 40 (1), pp.Article No. 5. 〈10.1145/2699500〉. 〈hal-01211288〉

Partager

Métriques

Consultations de la notice

171

Téléchargements de fichiers

73