The system GVERDI (Graphical VErification and Rewriting for Debugging Internet Sites) is a Web verifier prototype that is able to detect missing/incomplete Web pages and incorrect/forbidden information inside a Web site w.r.t. a given formal specification.

GVerdi Screenshot

GVERDI implements a rewriting-based, formal specification language which allows us to define syntactic as well as semantic properties of Web sites, that are given as finite sets of semistructured expressions, and a verification technique that obtains the requirements not fulfilled by the Web site, and helps to repair the errors by finding out incomplete information and/or missing pages as well as incorrect/forbidden information. The methodology is based on a novel rewriting-based technique, called partial rewriting, in which the traditional pattern matching mechanism is replaced by tree simulation, a suitable technique for recognizing patterns inside semistructured documents.

GVERDI is written in Haskell. The implementation consists of about 120 function definitions (approximately 1100 lines of source code). It includes a parser for semistructured expressions and Web specifications, and several modules implementing the graphical user interface, the partial rewriting mechanism and the verification technique. The system allows the user to load a Web site directory together with a Web specification. Additionally, he/she can inspect the loaded data and finally check the Web pages w.r.t the Web site specification. The graphical user interface is (hopefully) friendly and self-explaining.

You can download GVerdi.zip (10 Mb), which includes the executable for Win 98/NT/XP, source code, libraries, examples and documentation.

IMPORTANT: For a correct execution, you must indicate in the file "Path.ini", the complete path name where GVerdi is installed in your system (where the directory GVerdi is stored). For instance, you must write "C:\GVerdi" as the first line of Path.ini, if you uncompress GVerdi.zip in "C:\"

In the following we provide some examples in order to show how to use the system prototype.
 

Consider a Web site containing information about a research group such as group member affiliation, scientific publications and personal data. A Web site W containing such information is provided here.
We are interested to first model and, then, check the following properties in W.

• Whenever a home page of a professor is recognized, then that page must also include some teaching information.

• Whenever there exists a Web page containing information about scientific publications, each author of a publication should be a member of the research group.

• For each member, the fullname must be obtained appending the name and the surname of that member.

• Whenever there exists a course link, it must make reference to a course page included in the Web site.

• Blinking text is forbidden in the whole Web site.

• For each research project, the total project budget must be equal to the sum of the funds, which has been granted for the first and the second research periods.

• Only recent publications are referred in the Web site (from the last five years).

• In order to avoid sexual contents from being published in the home pages of the group members, the word "sex" cannot occur in any home page.

A GVERDI Web specification S which is suitable for modeling these properties follows.

    hpage(status('Professor'))->#hpage(#status(#'Professor'),teaching())))
    pubs(pub(name(X),surname(Y)))->#member(name(X),surname(Y)))
    member(name(X),surname(Y))->#member(name(X),surname(Y),full(&append X Y&))
    courselink(url(X),urlname(Y))->#cpage(title(Y)))
    blink(X)->error
    project(grant1(X),grant2(Y),total(Z))->error : &(read X)+(read Y)/=(read Z)&
    pub(year(X))->error : &(read X)<1999&
    hpage(links(link(url(X)))) -> error : &match X [a-zA-Z]*sex[a-zA-Z]*&

By executing GVERDI with Web site W and Web Specification S as input, we are able to detect the following errors in W:

Example 2

Consider a Web site (written in XHTML) containing personal information of a research fellow such as software, research interests, teaching, etc. You can download here this Web site W.
We want to model and check the following properties:

• For each link to a page (excepting "Home" page)  inside  the Web site, the title of the page must match the name given in the link reference.

• The home page must have as title the string "CLG-" (Computational Logic Group) followed by the title given in the link references to the home page (in  upper case).

• The Menu page must contain the tags "meta" and "body" (it can't be void).

• The Publications page must show the publications infomation as a list.

• The Home page must contain the image "logo.jpg".

• A publication can not be referred in the Web site if it's still "to appear".

A GVERDI Web specification S which is suitable for modeling these properties follows.

  a(href('Courses.html'),X) -> #html(#head(#title(#X)))
  a(href('Publications.html'),X) -> #html(#head(#title(#X)))
  a(href('Software.html'),X) -> #html(#head(#title(#X)))
  a(href('Home.html'),X) -> #html(#head(#title(#&'CLG-'++(map toUpper X)&)))
  head(title('CLG MENU')) -> #html(#head(#title(#'CLG MENU'),meta()),body())
  head(title('Publications'))->#html(#head(#title(#'Publications')),body(ul(li())))
  head(title('CLG HOME'))->#html(#head(#title(#'CLG HOME')),body(img(src('logo.jpg'))))
  li(X) -> error : &match X [Tt]o [Aa]ppear&

By executing GVERDI with Web site W and Web Specification S as input, we are able to detect the following errors in the Web site:

• D. Ballis and J. García Vivó
  A Rule-based System for Web site Verification
  In Proc. of 1st International Workshop on Automated Specification and Verification of Web Sites (WWV'05), Valencia (Spain).
  ENTCS to appear. 2005.  pdf (263 Kb)
   
• A Rule-based System for Web site Verification. Power Point Presentation from the 1st International Workshop on Automated Specification and Verification of Web Sites (WWV'05), Valencia (Spain). ppt   (200 Kb).
   
• M. Alpuente , D. Ballis and M. Falaschi
  Automated Verification of Web Sites Using Partial Rewriting
  In Proc. of 1st International Symposium on Leveraging Applications of Formal Methods (ISoLA'04), Paphos (Cyprus).
  Technical report TR-2004-06, Department of Computer Science, University of Cyprus. pdf (195 Kb).
   
• M. Alpuente , D. Ballis and M. Falaschi
  VERDI: an Automated Tool for Web sites Verification
  In Proc. of the 9th European Conference on Logics in Artificial Intelligence (JELIA '04), Lisbon (Portugal)
  © Springer LNCS 3229, pages 726-729, Springer-Verlag, Berlin, 2004. System Demonstration. pdf (113 Kb).
   
• M. Alpuente , D. Ballis and M. Falaschi
  A Rewriting-Based Framework for Web Sites Verification
  RULE '04, Electronic Notes in Theoretical Computer Science, volume 124.1, 2004
  © Elsevier, North-Holland. pdf (243 Kb)
   
• GVerdi User´s Manual (To appear)

• Haskell Main page. http://www.haskell.org
• wx-Haskell page. http://wxhaskell.sourceforge.net/
• Haskell communities and activities report. http://www.haskell.org/communities/05-2005/html/report.html
• 1st International Workshop on Automated Specification and Verification of Web Sites (WWV'05), Valencia (Spain).
  http://www.dsic.upv.es/workshops/wwv05