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[13]. 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 [1] 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.
Web Applications Design and Maintenance using Symbolic Model Checking / DI SCIASCIO, Eugenio; F. M., Donini; Mongiello, Marina; G., Piscitelli. - (2003), pp. 63-72. (Intervento presentato al convegno 7th European Conference on Software Maintenance and Reengineering, CSMR 2003 tenutosi a Benevento, Italy nel 26-28 March, 2003) [10.1109/CSMR.2003.1192411].
Web Applications Design and Maintenance using Symbolic Model Checking
DI SCIASCIO, Eugenio;MONGIELLO, Marina;
2003-01-01
Abstract
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[13]. 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 [1] 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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
