Special issue on Automated Specification and Verification of Web Systems

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 foundational model of distributed systems. The article by Jonathan Michaux, Elie Najm and Alessandro Fantechi addresses a problem similar to that of the previous contribution, namely ensuring interaction safety in a distributed setting, but relying on a formal model closer to practical systems. In fact, the paper proposes a session-based formalism for specifying Web service orchestrations, together with a related type discipline for prescribing the correct ordering of interactions. Researchers working on session-types or on service orchestrations could be interested in this paper. The article by David Insa, Josep Silva and Salvador Tamarit introduces a technique to automatically extract the main content of webpages. The proposed process is based on the information contained in the DOM structure of pages and analyses hierarchical relations of page elements and the distribution of textual information. This paper can be interesting for all researchers working on content extraction or on some of its many applications. The article by Maria Alpuente, Demis Ballis, Moreno Falaschi, Francisco Frechina and Daniel Romero presents a rewriting-based framework for XML document verification and repairing. In particular, the paper addresses the issue of maintaining the consistency of ever-larger, complex XML repositories through a methodology for semi-automatically repairing faulty reposi- tories. To this aim, a rewriting-based verification engine is exploited. Interested readers can experiment with the proposed repairing strategies by means of a prototype implementation. These five papers have been selected out of the ten high-quality submissions we have received. We thank the authors for their contributions and the referees for their careful and thorough work. We thank also Inge Bethke, the Editorial Assistant of the Journal of Logic and Algebraic Programming, and Allwyn Richard, an Elsevier Journal Manager, for their support and assistance during the editorial process