Special issue on Automated Specification and Verification of Web Systems

• Published in: The Journal of Logic and Algebraic Programming
• Main Authors: L. Kovács, R. Pugliese, J. Silva, TIEZZI, Francesco
• Other Authors: L., Kovác, R., Pugliese, J., Silva, Tiezzi, Francesco
• Format: Other/Unknown Material
• Language: English
• Published: Elsevier 2013
• Subjects: Iceland
• Online Access: http://hdl.handle.net/11581/362996; https://doi.org/10.1016/j.jlap.2013.05.007

This special issue has been organised after the 7th and 8th editions of the International Workshop on Automated Speci- fication and Verification of Web Systems (WWV), which took place in Reykjavik, Iceland, on June 9, 2011, and in Stockholm, Sweden, on June 16, 2012, respectively. Nowadays, many companies and institutions have diverted their Web sites into interactive, completely-automated, Web- based applications for, e.g., e-business, e-learning, e-government and e-health. The increased complexity and the explosive growth of Web systems have made their design and implementation a challenging task. Systematic, formal approaches to their specification and verification can permit to address the problems of this specific domain by means of automated and effective techniques and tools. The papers published in this special issue address some of these topics, such as Web browser security, interaction safety in distributed systems, content extraction on webpages, and repository consistency verification and repairing. More specifically, the contribution of these papers is as follows. The article by Nataliia Bielova provides a survey of dynamic techniques to enforce Web script security and privacy poli- cies in Web browsers. This paper can be instructive for both computer security researchers and Web developers. The former group of readers would be mainly interested in security-relevant components of Web browsers and security poli- cies based on these components, while the latter in classification and comparison of security policies and enforcement mechanisms. The article by Marco Giunti presents a type checking algorithm for establishing a session-based discipline in a dialect of π-calculus. The paper illustrates a type system based on a notion of context splitting and proves that it satisfies the expected standard properties: subject reduction and type-safety. A type checking algorithm implementing the type system is then defined. Thus, this paper provides an effective approach for ensuring relevant properties in a ...