Rule-based Web site verification

Web verification methodology

• Roughly speaking, the verification methodology works as follows. First, we check whether the left-hand side l of some Web specification rule is embedded into a given page p of the considered Web site. When the embedding test l p succeeds, by extending the proof, we construct the biggest substitution for the variables in Var(l), such that l instantied p. Then, depending on the nature of the Web specification rule (correction or completeness rule), it is as follows:

  (Correction rule) evaluating the condition of the rule (instantiated); a correctness error is signalled in the case when the error condition is fulfilled.
  
  (Completeness rule) by a new homeomorphic embedding test, checking whether the right-hand side of the rule (instantiated) is recognized in some page of the considered Web site. Otherwise, a completeness error is signalled. Moreover, from the incompleteness symptom computed so far, a fixpoint computation is started in order to discover further missing information, which may involve the execution of other completeness rules.