Thesis Title

Formal Verification of Sites and Web Applications
Daniel Romero

Thesis Intro

There is a great quantity of Web applications, in use or in advanced process of planning or implementation, oriented to topics of high sensibility such as health, finance, defense, e-business critical applications, and e-government. The expansion of the development and utilization of these applications has not been accompanied by the development of methods, models and verification tools that allow to adapt and evaluate the aspects related with their reliability and security.
      The sudden growth of Web applications requires methods, models, and highly effective verification tools which are also highly productive considering the amount of work to be done.
      In addition to this, methods, models and tools of formal verification will be developed to detect different types of weaknesses of Web applications which already exist or which are in design / implementation process. Flaws in quality and throughput must be accurately detected and an appropriate solution mechanism must be proposed.
      The methods, models, and tools proposed must work in the available real time Web applications to be studied because the partial or total interruption of the service is unthinkable in certain applications such as banking systems.

Thesis Info

This doctoral thesis project aims at:

• Proposing methodological approaches guided to the formal verification of web sites and web applications in service or in design / implementation process.
• Generating models that facilitate the verification of Web systems which are existent or in design / implementation process. These models will facilitate the verification of static aspects such as content and structures of Web pages as well as dynamic aspects such as transitions, evolution of Web sites, and security. In addition, computational models, rigorous semantics, and specification techniques will be studied.
       
• Developing tools that contribute to the optimization of existing Web systems operating on the models previously mentioned.
       
• Implementing algorithms that allow the verification of the static properties and the dynamics of Web applications which already exist or which are in design process.
       
• Developing automatic methods that allow to verify an existing Web application with reference to a particular quality standard. Besides, algorithm verification techniques in this context using multiparadigm declarative programming will be studied.

     

Thesis References

[1] Haydar, May, Petrenko Alexandre, Sahraoui Houari, "Formal Verification of Web Applications Modeled by Communicating Automata" CRIM, Centre de recherche informatique de Montréal 550 Sherbrooke West, Suite 100, Montreal, Quebec, H3A 1B9, Canada, 2004

[2] M. Alpuente, D. Ballis, and M. Falaschi A Rewriting-based Framework for Web sites Verification Electronic Notes in Theoretical Computer Science, 124(1):41-61, 2005

[3] Lucas, Salvador, “Rewriting-Based Navigation of Web Sites: Looking for Models and Logics” © Elsevier Electronic Notes in Theoretical Computer Science, to appear, 2005.

[4] M. Alpuente. S. Escobar, and M. Falaschi (Eds.) 1st International Workshop on Automated Specification and Verification of Web Sites, WWV'05
ENTCS, to appear, 2005. © Elsevier Science, North-Holland

[5] Muruguesan, S., Desphande, Y.: Web Engineering. Software Engineering and Web Application Development. Springer LNCS – Hot Topics (2001).

[6] Pastor O., Abrahao S., and Fons J. J. An Object-Oriented approach to automate web applications development. In 2nd International Conference on Electronic Commerce and Web Technologies (EC-Web'01), Springer-Verlag, LNCS 2115. ISBN: 3-540-42517-9. Munich, Germany, Septiembre, 2001

[7] Fons, J., Valderas, P., Pastor, O. Specialization in Navigational Models. Argentine Conference on Computer Science and Operacional Research. Subserie ICWE, Iberoamerican Conference on Web Engineering. Volume 31 of Anales JAIIO., SantaFe, Argentina (2002) 16-31 ISSN: 1666-6526.

[8] Abrahao S., Fons J., Gonzalez M. and Pastor O. Conceptual Modeling of Personalized Web Aplications. In 2nd International Conference on Adaptive Hipermedia and Adaptive Web Based Systems, Malaga, Spain, 2002.

[9] Koch, N., Wirsing, M.: Software Engineering for Adpatative Hypermedia Applications. In: 3rd Workshop on Adaptative Hypertext and Hypermedia (2001).

[10] Jessica Chen, Xiaoshan Zhao: Formal Models for Web Navigations with Session Control and Browser Cache. ICFEM 200: 46-60

[11] Luca de Alfaro: Model Checking the World Wide Web. CAV 2001: 337-349