Web design is an inherently error-prone process.
To help with the detection of errors in the structure and connectivity
of web pages, we propose to apply model-checking techniques to the
analysis of the World Wide Web.
Model checking the Web is different in many respects from ordinary
model checking of system models, since the Kripke structure of the Web
is not known in advance, but can only be explored in a gradual
fashion.
In particular, the model-checking algorithms cannot be phrased in
mu-calculus, since some operations, such as the computation of sets
of predecessor web pages to the computations of greatest fixpoints,
are not possible on the Web.
We introduce constructive mu-calculus, a fixpoint
calculus similar to mu-calculus, but whose formulas can be
effectively evaluated over the Web;
and we show that its expressive power is very close to
that of ordinary mu-calculus.
Constructive mu-calculus can be used not only for phrasing Web
model-checking algorithms, but also for the analysis of systems having
a large, irregular state space that can be only gradually explored,
such as software systems.
On the basis of these ideas, we have implemented the Web model checker
MCWEB, and we describe some of the issues that arose in its
implementation, as well as the type of errors that it was able to
find.
