Published: 31st July 2013
DOI: 10.4204/EPTCS.123
ISSN: 2075-2180


Proceedings 9th International Workshop on
Automated Specification and Verification of Web Systems
Florence, Italy, 6th June 2013

Edited by: António Ravara and Josep Silva

António Ravara and Josep Silva
Invited Presentation: Self-Healing Service-Based Processes
Gerhard Friedrich
Invited Presentation: Deconstructing Complex Distributed Platforms: A Report from the Trenches
François Taïani
Blind-date Conversation Joining
Luca Cesari, Rosario Pugliese and Francesco Tiezzi
Local Type Checking for Linked Data Consumers
Gabriel Ciobanu, Ross Horne and Vladimiro Sassone
Amending Choreographies
Ivan Lanese, Fabrizio Montesi and Gianluigi Zavattaro
Proving Properties of Rich Internet Applications
James Smith


This volume contains the final and revised versions of the papers presented at the 9th International Workshop on Automated Specification and Verification of Web Systems (WWV 2013). The workshop was held in Firenze, Italy, on June 6, 2013, as part of DisCoTec 2013, the 8th International Federated Conference on Distributed Computing Techniques. Previous WWV workshops were held in Stockholm (2012), Reykjavik (2011), Vienna (2010), Hagenberg (2009), Siena (2008), Venice (2007), Cyprus (2006), and Valencia (2005). Information about the workshop can be found at:

WWV 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, Software engineering, Formal methods and Web-oriented research. WWV has a reputation for being a lively, friendly forum for presenting and discussing work in progress. The proceedings have been produced after the symposium to allow the authors to incorporate the feedback gathered during the event in the published papers.

All papers submitted to the workshop were reviewed by at least three Program Committee members or external referees. In response to this year's call for papers, we received 10 paper submissions. The Program Committee of WWV 2013 collected three reviews for each paper and held an electronic discussion leading to the selection of 6 papers for presentation at the workshop, and 4 papers for publication in the Electronic Proceedings in Theoretical Computer Science (EPTCS). In addition to the presentation of the contributed papers, the scientific programme included the invited talks by two outstanding speakers: Gerhard Friedrich (Universität Klagenfurt, Austria) and François Taïani (Université de Rennes 1, France). We would like to thank them for having accepted our invitation.

We want to thank the Program Committee members, who worked diligently to produce high-quality reviews for the submitted papers, as well as all the external reviewers involved in the reviewing 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 are very grateful to the DisCoTec 2013 General Chair Michele Loreti (Università di Firenze, Italy), the DisCoTec 2013 Workshops Chair Rosario Pugliese (Università di Firenze, Italy), and the local organizers for the great job they did in preparing the event. We would also like to thank Andrei Voronkov for his excellent EasyChair system that automates many of the tasks involved in chairing a conference. Finally, we wish to thank the editorial board of the Electronic Proceedings in Theoretical Computer Science (EPTCS) for publishing these proceedings in their series.

18th of July, 2013 António Ravara
Josep Silva

Self-Healing Service-Based Processes

Gerhard Friedrich (Institut fur Angewandte Informatik, Alpen-Adria Universität Klagenfurt, Austria)

In [FFM+10] we introduce a self-healing approach to handle exceptions in service-based processes and to repair the faulty activities with a model-based approach. During execution, whenever an exception arises, diagnosis of the failure is performed and repair plans are generated by taking into account information about the process execution, constraints posed by the process structure, dependencies among data, and available repair actions. We also describe the main features of the prototype developed to validate the proposed repair and diagnosis approach for composed Web services. The self-healing architecture for repair handling and the experimental results are illustrated.

However, in practice complete specifications of process activities are not available. Therefore, diagnosis and repair methods for partial behavior models are of great importance. In [MFS12] we show that if the assumption of complete behavioral models is lifted, basic diagnosis and repair problems reside on the second level of the Polynomial Hierarchy. A method for diagnosing process trajectories under partially known behavior is described in [FMS10].


[FFM+10] Gerhard Friedrich, Mariagrazia Fugini, Enrico Mussi, Barbara Pernici, and Gaston Tagni. Exception handling for repair in service-based processes. IEEE Trans. Software Eng., 36(2):198-215, 2010.
[FMS10] Gerhard Friedrich, Wolfgang Mayer, and Markus Stumptner. Diagnosing process trajectories under partially known behavior. In Helder Coelho, Rudi Studer, and Michael Wooldridge, editors, ECAI, volume 215 of Frontiers in Artificial Intelligence and Applications, pages 111-116. IOS Press, 2010.
[MFS12] Wolfgang Mayer, Gerhard Friedrich, and Markus Stumptner. On computing correct processes and repairs sing partial behavioral models. In Luc De Raedt, Christian Bessière, Didier Dubois, Patrick Doherty, Paolo Frasconi, Fredrik Heintz, and Peter J. F. Lucas, editors, ECAI, volume 242 of Frontiers in Artificial Intelligence and Applications, pages 582-587. IOS Press, 2012.

Deconstructing Complex Distributed Platforms: A Report from the Trenches

François Taïani (Université de Rennes 1 / IRISA, Rennes, France)

Wading in unfamiliar software in modern distributed systems

Distributed services play an increasing role in our daily lives and our economy. Unfortunately, as their importance grows, so does their complexity, and the difficulty to analyse, verify, and validate them. Popular distributed applications such as social networks (Facebook, Twitter) or collaborative websites (Wikipedia, reddit) typically involve millions of users, support external developers through publicly available APIs (involving REST and JSON), and run in the cloud (e.g. Netflix and Foursquare). None of these technological feats would be possible without the use of complex software stacks, usually constructed from reusable third party components, many of which are available in open source.

Integrating these third party components is however challenging, and often requires developers to modify or analyse the behaviour of software they know little about. This happens for instance when hardening a piece of software (e.g. an RPC engine, or a message-oriented middleware) to use it in a mission-critical environment. This can also happen when diagnosing non-functional issues such as performance.

How to analyse 6,466,652 Java method calls

Analysing distributed platforms for hardening or diagnosing is a hard and multifaceted problem. One key challenge arises from the fact that the software stacks at the heart of many distributed applications usually combine many pieces of legacy and third-party software developed by different teams, in different projects, hosted by different organisations. Because of their size and complexity, these stacks typically cannot be fully analysed with entirely automated approaches. In this talk, I provide an overview of our experience with two real life platforms (a C++ RPC middleware [2], and Java web-service grid platform [1]) using two different kinds of strategy (graph manipulation, and interactive visualisation). Our work shows the importance of pragmatic approaches to analyse the dynamic behaviour of real platforms, and the potential for strategies based on incremental abstraction to construct representative models of said platforms that are intuitively understandable by practitioners.


  1. Shen Lin, François Taïani, Thomas C. Ormerod & Linden J. Ball (2010): Towards anomaly comprehension: using structural compression to navigate profiling call-trees.
    In: SOFTVIS '10, ACM, pp. 103-112.
    Available at
  2. François Taïani, Matti Hiltunen & Rick Schlichting (2005): The Impact of Web Service Integration on Grid Performance.
    In: HPDC-14, IEEE, pp. 14-23.
    Available at

Francois Taiani 2013-07-18