Published: 10th August 2011
DOI: 10.4204/EPTCS.61
ISSN: 2075-2180

EPTCS 61

Proceedings 7th International Workshop on
Automated Specification and Verification of Web Systems
Reykjavik, Iceland, 9th June 2011

Edited by: Laura Kovacs, Rosario Pugliese and Francesco Tiezzi

Preface
A theorem proving framework for the formal verification of Web Services Composition
Petros Papapanagiotou and Jacques D. Fleuriot
1
Specification and Verification of Context-dependent Services
Naseem Ibrahim, Vangalur Alagar and Mubarak Mohammad
17
Product Lines for Service Oriented Applications - PL for SOA
Maurice H. ter Beek, Stefania Gnesi and Mercy N. Njima
34
Automated Functional Testing based on the Navigation of Web Applications
Boni García and Juan Carlos Dueñas
49
Debugging of Web Applications with Web-TLR
María Alpuente, Demis Ballis, Javier Espert, Francisco Frechina and Daniel Romero
66
An Abstract Semantics for Inference of Types and Effects in a Multi-Tier Web Language
Letterio Galletta and Giorgio Levi
81
A type checking algorithm for qualified session types
Marco Giunti
96

Preface

This volume contains the final and revised versions of the papers presented at the 7th International Workshop on Automated Specification and Verification of Web Systems (WWV 2011). The workshop was held in Reykjavik, Iceland, on June 9, 2011, as part of DisCoTec 2011.

The aim of the WWV workshop series is to provide an interdisciplinary forum to facilitate the cross-fertilization and the advancement of hybrid methods that exploit concepts and tools drawn from Rule-based programming, Software engineering, Formal methods and Web-oriented research. Nowadays, indeed, 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.

In response to this year's call for papers, we received 9 paper submissions. The Program Committee of WWV 2011 collected three reviews for each paper and held an electronic discussion leading to the selection of 7 papers for presentation at the workshop.

The scientific programme consisted of three sessions. The first session was about Service-Oriented Applications and has seen the presentation of a framework for Web Services composition based on a higher-order logic theorem prover, a composition theory for specifying and verifying services with context-dependent contracts, and a formalism for modeling variability in SOA product lines. The second session has concerned Web Applications and has seen the presentation of a navigation-based, functional testing approach for web applications, and a Web debugging facility supporting the efficient manipulation of WEB-TLR counterexample traces. Finally, the third session was about Typing Systems and has seen the presentation of an abstract interpretation technique to reconstruct a types-and-effects system for a multi-tier Web language, and a type checking algorithm for qualified session types in pi-calculus.

In addition to the selected papers, the scientific programme included an invited lecture by Elie Najm from Telecom ParisTech (France) on a type-based approach for controlling sessions in an orchestration language inspired by WS-BPEL. We would like to thank him for having accepted our invitation.

We would also like to thank all the members of the Program Committee and all the reviewers for their careful work in the review and selection process. Many thanks to the authors of the submitted papers and to all workshop participants. Thanks also go to the steering committee members of WWV for their valuable advice. We thank EasyChair for hosting the WWV 2011 submission and reviewing process, and the DiscoTec 2011 local organizers for their support and guidance. Finally, we wish to thank the editorial board of the Electronic Proceedings in Theoretical Computer Science (EPTCS) for publishing these proceedings in their series.


Laura Kovacs, Rosario Pugliese and Francesco Tiezzi
WWV 2011 Program Chairs and Proceedings Editors
July 2011



WORKSHOP ORGANIZATION

Program Chairs

Laura Kovacs   (Vienna University of Technology, Austria)
Rosario Pugliese   (University of Florence, Italy)
Francesco Tiezzi   (IMT Advanced Studies Lucca, Italy)

Program Committee

Maria Alpuente   (Technical University of Valencia, Spain)
Demis Ballis   (University of Udine, Italy)
Maurice ter Beek   (ISTI-CNR, Pisa, Italy)
Santiago Escobar   (Technical University of Valencia, Spain)
Jean-Marie Jacquet   (University of Namur, Belgium)
Laura Kovacs   (Vienna University of Technology, Austria)
Temur Kutsia   (Johannes Kepler University Linz, Austria)
Tiziana Margaria   (Universitat Potsdam, Germany)
Manuel Mazzara   (Newcastle University, United Kingdom)
Catherine Meadows   (Naval Research Laboratory, USA)
Yasuhiko Minamide   (University of Tsukuba, Japan)
Rosario Pugliese   (University of Florence, Italy)
I.V. Ramakrishnan   (State University of New York, Stony Brook, USA)
Francesco Tiezzi   (University of Florence, Italy)
Franz Weitl   (National Institute of Informatics, Tokyo, Japan)
Nobuko Yoshida   (Imperial College London, United Kingdom)

External Reviewers

Romain Demangeon   (Queen Mary London, United Kingdom)
Javier Espert   (Technical University of Valencia, Spain)
Falk Howar   (Uppsala University, Sweden)
Fernando Martinez Plumed   (Technical University of Valencia, Spain)
Nicola Mezzetti   (Di.Tech SpA, Bologna)
Bardia Mohabbati   (Simon Fraser University, Canada)
Stephan Windmueller   (Technical University of Dortmund, Germany)