Model Checking the World Wide Web

Luca de Alfaro

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


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.

Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Start Conference Manager
Conference Systems