Formal Verification of Web Sites
Authors
Sonia Flores, Salvador Lucas and Alicia Villanueva
Abstract
In this paper, a model for websites is presented. The model is
well-suited for the formal verification of dynamic as well as static
properties of the system. A website is defined as a collection of
web pages which are semantically connected in some way. External
web pages (which are related pages not belonging to the website) are
treated as the environment of the system. We also present
the logic which is used to specify properties of websites, and
illustrate the kinds of properties that can be specified and
verified by using a model-checking tool on the system. In this
setting, we discuss some interesting properties which often need to
be checked when designing websites. We have encoded the model using
the specification language Maude which allows us to use the
Maude model-checking tool.
Keywords
Models of the Web, Graph representation, Formal Verification, Model
Checking.