Résumé | 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, Aautomata,
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. |