Rule-based Web site verification

We briefly recall the formal verification methodology proposed in ABF06, which allows us to detect forbidden/erroneous information as well as missing information in a Web site. By executing a Web specification on a given Web site, we are able to recognize and exactly locate the source of a possible discrepancy between the Web site and the properties required in the Web specification.

In this framework, we assume a Web page to be a well-formed XML document. Since XML documents are provided with a tree-like structure, they can be straightforwardly encoded as ground Herbrand terms of a given term algebra ז (Text U Tag), where Text represents the set of all the finite strings over a given alphabet and Tag is a set of tag symbols ABF06. Note that XML tag attributes can be considered as common tagged elements, and hence be translated analogously. Therefore, a Web site can be seen as a finite set of ground terms belonging to ז (Text U Tag). In the following, we will also consider terms of the non-ground term algebra ז (Text U Tag , V), which may contain variables. An element s ε ז (Text U Tag , V) is called XML document template. In our methodology, Web page templates are used to specify properties of Web sites.

A Web specification is a triple (R,IN,IM), where R, IN, and IM are a finite set of rules. The set R contains the definition of some auxiliary functions which the user would like to provide, such as string processing, arithmetic, boolean operators, etc. R is formalized as a term rewriting system, which is handled by standard rewriting. The rewriting mechanism executes function calls by simply reducing them to their irreducible form (that is, a term that cannot be rewritten further). The set IN describes constraints for detecting erroneous Web pages (correctNess rules). A correctness rule has the following syntax:

l -> error |C

where l is a term, error is a reserved constant, and C is a (possibly empty) finite sequence containing

    - membership tests of the form X \in rexp w.r.t. a given regular language rexp;
    - equations/inequalities over terms.

When C is empty, we simply write l -> error. Informally, the meaning of a correctness rule l -> error |C is the following. Whenever (i) a "piece" of a given Web page can be "recognized" to be an instance of l, and (ii) the corresponding instantiated condition holds, then Web page is marked as an incorrect page. The third set of rules IM specifes some properties for discovering incomplete/missing Web pages ( coMpleteness rules). A completeness rule is defined as

l -> r {q}

where l and r are terms and q can be A or E. Completeness rules of a Web specification formalize the requirement that some information must be included in all or some pages of the Web site. We use attributes {A} and {E} to distinguish "universal" from "existential" rules, as explained below. Right-hand sides r of completeness rules can contain functions, which are defined in R. In addiction, some symbols in the right-hand sides of the rules may be marked by means of the symbol #. Marking information of a given rule r is used to select the subset of the Web site in order to check the condition formalized by r. Intuitively, the interpretation of a universal rule l -> r {A} (respectively, an existential rule l -> r {E}) w.r.t. a Web site \Website is as follows: if (an instance of) l is "recognized" in the Web Site, (an instance of) the irreducible form of r must also be "recognized" in all (respectively, some) of the Web pages that embed (an instance of) the marked structure of r. Let R be a TRS, we define X ++Y , which concatenates two strings; we also define X+Y, which sums two natural numbers. Let (R,IN,IM) be a Web specification where IN and IM are defined as follows:

	member(name(X),surname(Y)) -> #hpage(fullname(X++Y)),status)  {E} 
	hpage(status(professor)) -> #hpage(#status(#professor),teaching)) {A} 
	project(grant1(X),grant2(Y),total(Z)) -> error X+Y <> Z
	

This Web specification models some required properties for a Web site of a research group. The first rule formalizes the following property: if there is a Web page containing a member list, then for each member, a home page should exist which contains (at least) the full name and the status of this member. The full name is computed by applying the function ++ to the name and the surname of the member. The marking information establishes that the property must be checked only on home pages (i.e., pages containing the tag "hpage"). The second rule states that, whenever a home page of a professor is recognized, that page must also include some teaching information. The rule is universal since it must hold for each professor home page (i.e., all the Web pages embedding the marked structure home(status(professor)). The third rule states that, for each research project, the total project budget must be equal to the sum of the funds, which have been granted for the first and the second research periods. The membership tests in the conditions ensure that the values assigned to the variables are natural numbers. Diagnoses are carried out by running Web specifications on Web sites. The operational mechanism is based on a novel, flexible matching technique ABF06 that is able to "recognize" the partial structure of a term (Web template) within another and select it by computing homeomorphic embeddings of Web patterns within Web documents.