Published: 8th September 2014
DOI: 10.4204/EPTCS.163
ISSN: 2075-2180


Proceedings 10th International Workshop on
Automated Specification and Verification of Web Systems
Vienna, Austria, July 18, 2014

Edited by: Maurice H. ter Beek and António Ravara

Maurice H. ter Beek and António Ravara
Invited Presentation: A Formal Approach to Legacy Modernization: Baby Steps
Steve Ross-Talbot
Automatic Detection of Webpages that Share the Same Web Template
Julián Alarte, David Insa, Josep Silva and Salvador Tamarit
A Local Logic for Realizability in Web Service Choreographies
R Ramanujam and S Sheerazuddin
Static Enforcement of Role-Based Access Control
Asad Ali and Maribel Fernández


These proceedings contain the papers presented at the 10th International Workshop on Automated Specification and Verification of Web Systems (WWV 2014), which was held on 18 July 2014 in Vienna, Austria. WWV 2014 was a satellite workshop of the Federated Logic Conference (FLoC 2014), associated to the 7th International Joint Conference on Automated Reasoning (IJCAR 2014), as part of the Vienna Summer of Logic (VSL 2014), the largest event in the history of logic with over 2500 participants.

Nowadays many companies and institutions have diverted their Web sites into interactive, completely automated, Web-based applications for areas such as e-business, e-learning, e-government, and e-health. The increased complexity and the explosive growth of Web systems has made their design and implementation a challenging task. Systematic, formal approaches to their specification and verification allow to address the problems of this specific domain by means of effective automated techniques and tools.

The international workshop on Automated Specification and Verification of Web Systems is a yearly workshop that aims at providing an interdisciplinary forum to facilitate the cross-fertilization and the advancement of hybrid methods that exploit concepts and tools drawn from rule-based programming, formal methods, software engineering and Web-oriented research. The previous nine WWV workshops were held in Florence (2013), Stockholm (2012), Reykjavik (2011), Vienna (2010), Hagenberg (2009), Siena (2008), Venice (2007), Cyprus (2006), and Valencia (2005).

This year, four papers were submitted to the workshop, and the Program Committee decided to accept two papers, based on their scientific quality, originality, and relevance to the workshop. Each paper was reviewed by at least three Program Committee members. In addition to presentations of these regular papers, this year's workshop included invited talks by Josep Silva (Universidad Politécnica de Valencia, Spain) and Steve Ross-Talbot (Cognizant Technology Solutions, UK). At VSL 2014, WWV 2014 was scheduled as a joint session with the 2nd International Workshop on Verification and Program Transformation (VPT 2014), associated to the 26th International Conference on Computer Aided Verification (CAV 2014).

We want to thank the Program Committee members for their swift yet careful reviewing. We are grateful to the VSL organizers, the FLoC 2014 Workshop Chair Stefan Szeider, and the IJCAR 2014 Workshop Chair Matthias Horbach for accepting WWV as a satellite workshop at VSL 2014. We thank Alexei Lisitsa and Andrei Nemytykh for smoothly organizing a joint WWV+VPT session. We would also like to take this opportunity to thank Andrei Voronkov for his excellent EasyChair system that automates many of the tasks involved in organizing and chairing a conference. Finally, we thank EPTCS and its editor-in-chief, Rob van Glabbeek, for publishing the proceedings of WWV 2014.

Program Chairs

Program Committee

Steering Committee

A Formal Approach to Legacy Modernization: Baby Steps

Steve Ross-Talbot (Cognizant Technology Solutions, UK)

In excess of 80% of IT sits today in old legacy systems from mainframes of old to Java of 10 years past. All of the theory in the world has little use unless this legacy can be unlocked, reasoned over and understood. But the old problems of software engineering processes dog this area with little in the way of up-to-date accurate documentation of process, business rules and the lineage of data as it travels through a system. Recent work on optimising process flows to extract maximum throughput whilst leveraging concurrency shows great promise if we can only unlock the legacy. It turns out that session types and the technique of bi-simulation can be applied to unlock processes, determine business rules and expose data lineage. In this short talk I shall explain how we can do it, and show what it looks like and then talk a little of what the future may hold.