Querying Schemas With Access Restrictions
The authors 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. They look at verifying properties of a schema describing the possible accesses of such a system. They 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.