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.