Web applications design and maintenance using symbolic model checking

We present an approach to automatic checking of the correctness of Web applications structure during their lifecycle. The approach adopts the well-established symbolic model checking technique and the associated tool SMV. A formalism allows the designer to describe the model of a Web-based system. Computation Tree Logic (CTL) is adopted as language to define the properties to be verified. The approach has been implemented in a tool to provide automatic support in the design of Web applications. The system embeds the NuSMV model checker to perform verification. Verification is carried out after building the finite state model of a site in the model checker input language. To this purpose the system parses the HTML source code of Web pages, including code for dynamic pages. Properties are expressed using a user friendly interface for Web application developers that automatically translates properties in CTL formulas.