Architecture

In the scenario we consider, a Web application is provided by an interactive Web site that posts data, takes input from the user, and responds to the input by posting more data and/or taking some actions. The Web site can access an underlying database, as well as state information updated as the interaction progresses.

Interactive Website Specification

A Web page schema describes the structure of the web page the user sees at any given point. The content of a Web page is determined dynamically by querying the underlying database as well as the state. The actions taken by the Web site, and transitions from one Web page to another are determined by the input, state, and database.

Webpage Schema

  • Static schema
    • Posted data: Query(Database, State)
    • Input options: Query(Database, State)
  • Transitions
    • Triggered by user input
    • Target Webpage: Query(Database, State, Input)
    • State: Query(Database, State, Input)
    • Actions: Query(Database, State, Input)

Properties Satisfied by Interactive Web Applications

Our goal is to facilitate the design of sound and robust interactive Web applications. To this end, we allow the designer to express properties that the Web application should satisfy, and we verify these properties statically, at design time. The properties refer to runs, i.e. sequences of inputs, actions, and states that may result from interactions with a user. This covers a wide variety of useful properties. For example, in a Web application supporting an e-commerce application, it may be desirable to verify that no product is delivered before payment of the right amount is received. Or, we may wish to verify that the specification of Web page transitions is unambiguous, (the next Web page is uniquely defined at each point in a run), that each Web page is reachable from the home page, that all runs eventually terminate, etc.

To express such properties, we rely on temporal logic. Specifically, we consider two kinds of properties. The first requires that all runs must satisfy some condition on the sequence of inputs, actions, and states. To describe such properties we use a variant of linear-time temporal logic. Other properties involve several runs simultaneously. For instance, we may wish to check that for every run leading to some Web page, there exists a way to return to the home page. To capture such properties, we use the branching-time logics CTL and CTL*. Our results identify classes of Web applications for which temporal properties in the above temporal logics can be checked, and establish their complexity. As justification for the choice of these classes, we show that even slight relaxations of our restrictions lead to undecidability of verification.

Examples of Desirable Properties We Can Express and Verify:

  • Semantic properties:
    • "the user cannot cancel an order that has already been shipped."
    • "no product is delivered before payment of the right amount is received."
  • Workflow properties:
    • "There is a way to reach the home page from any page."
  • Soundness properties:
    • "The next Web page is unambiguously defined at any point."

Status

We are currently in the final stage of the project. We have worked out the framework for specifying interactive web sites and expressing properties. The main challenge was striking the balance between the expressivity of web application specifications and properties, and the decidability of static property verification.  This demo illustrates the framework. In the second stage, we have automatically generated web sites from user-provided specifications. Of course, the ultimate goal of this project is verification, which is demonstrated here. We are still currently working on a verifier, whose delivery will complete the third stage of our project.