We present an approach to automatic checking of thecorrectness of web applications structure during their life-cycle.The approach adopts the well-established symbolicmodel checking technique and the associated tool SMV. A formalism allows the designer to describe the modelof a web-based system. Computation Tree Logic (CTL) isadopted as language to define the properties to be verified.The approach has been implemented in a tool to provideautomatic support in the design of web applications.The system embeds the NuSMV  model checker to performverification. Verification is carried out after buildingthe finite state model of a site in the model checkerinput language. To this purpose the system parses theHTML source code of web pages, including code for dynamicpages. Properties are expressed using a user friendlyinterface for web application developers that automaticallytranslates properties in CTL formulas.
|Titolo:||Web Applications Design and Maintenance using Symbolic Model Checking|
|Data di pubblicazione:||2003|
|Nome del convegno:||7th European Conference on Software Maintenance and Reengineering, CSMR 2003|
|Digital Object Identifier (DOI):||10.1109/CSMR.2003.1192411|
|Appare nelle tipologie:||4.1 Contributo in Atti di convegno|