Model checking the world wide web

Abstract

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 ordinary μ-calculus, since some operations, such as the computation of sets of predecessor Web pages and the computations of greatest fix points, are not possible on the Web. We introduce constructive μ-calculus, a fix point calculus similar to μ-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 μ-calculus. Constructive μ-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.