Web Services and Formal Methods

9th International Workshop on Web Services and Formal Methods, WS-FM 2012
September 6-7, 2012, Tallinn, Estonia

co-located to BPM 2012

Logo of the BPM 2012 conference. WS-FM was co-located to the 10th International Conference on Business Process Management, BPM 2012 (September 3-6, 2012).

Springer LNCS Proceedings

The proceedings are be published by Springer as LNCS, Volume 7843.

Logo of Springer's LNCS.

Program Online

The program of WS-FM is available. For each talk, we also linked the presentation slides.


The workshop will be held on Thursday afternoon and Friday morning in room Grande 3. There will be a workshop dinner on Thursday evening at Olde Hansa.

Thursday, 6 September 2012

Time Title
13:45-14:00 Opening (PC Chairs)
14:00-15:00 Invited talk: Formal approaches for automatic synthesis of web service business protocols (Farouk Toumani) [slides]
15:00-15:30 Coffee Break
15:30-16:30 Session 1: WS modeling and analysis with Petri nets and CSP, part 1
Chair: Andreas Lehmann
  • Jan Sürmeli. Service discovery with cost thresholds
  • Richard Müller, Wil M. P. Van Der Aalst and Christian Stahl. Private View Conformance Checking [slides]
16:30-16:45 Short Break
16:45-17:45 Session 2: WS modeling and analysis with Petri nets and CSP, part 2
Chair: Artem Polyvyanyy
  • Abel Armas-Cervantes, Luciano García-Bañuelos and Marlon Dumas. Event Structures as a Foundation for Process Model Differencing, Part 1: Acyclic Processes [slides]
  • Xi Wu, Yue Zhang, Huibiao Zhu, Yongxin Zhao, Zailiang Sun and Peng Liu. Formal Modeling and Analysis of the REST Architecture Using CSP [slides]
19:00-23:00 Workshop dinner at Olde Hansa

Friday, 7 September 2012

Time Title
9:00-10:00 Invited talk: "I have read and agree with the terms and conditions"...so what?
Taking contracts for services seriously.
(Emilio Tuosto) [slides]
10:00-10:30 Coffee Break
10:30-11:30 Session 3: FM applied to service discovery and coordination, part 1
  • Guillaume Demarty, Fabien Maronnaud, Gabriel Le Breton and Sylvain Hallé. SiteHopper: Abstracting Navigation State Machines for the Efficient Verification of Web Applications
  • Farhad Arbab and Francesco Santini. Preference and Similarity-based Behavioral Discovery of Services [slides]
11:30-11:45 Coffee Break
11:45-12:45 Session 4: FM applied to service discovery and coordination, part 2
  • Nuno Oliveira and Luis Barbosa. Reconfiguration mechanisms for service coordination
  • Peng Liu and Huibiao Zhu. Linking the Semantics of BPEL using Maude [slides]
12:45-13:45 Closing and lunch


Farouk Toumani

Formal approaches for automatic synthesis of web service business protocols

One of the ultimate goals of the web service technology is to enable rapid low-cost development and easy composition of distributed applications, a goal that has a long history strewn with only partial successes. The research problems underlying service composition are varied in nature and depend on several parameters such as the model used to describe the services, the communication model or the composition language. A line of demarcation between existing works in this area lies in the nature of the composition process: manual v.s. automatic. The first category of work deals generally with high-level composition design and programming details related to implementation issues while automatic service composition focuses on different issues such as composition verification, planning or synthesis.

In this talk, we consider more particularly the composition synthesis problem, i.e., the automated construction of a new target service by reusing some existing ones. We will review recent research works and challenges related to automatic synthesis of service composition and discuss the associated computational problems both in bounded and unbounded settings.

Emilio Tuosto

"I have read and agree with the terms and conditions"...so what?
Taking contracts for services seriously.

The customary practice to regulate the functioning of services is to set terms & conditions. These are legal documents constraining the way services should be used and (sometimes) specifying what providers offer. In such documents it is not rare to find statements like

"We do our best to keep Facebook safe, but we cannot guarantee it" (http://www.facebook.com/legal/terms, revision date June 8, 2012; notably, 'safety' is not defined in the terms & conditions of facebook!)

In this talk, I will argue that -despite being a practical way out- this is far from being ideal. For instance, the lack of precise guarantees is a main deterrent for industries wishing to move their applications and business to the cloud. Quoting from http://cacm.acm.org/magazines/2010/4/81493-a-view-of-cloud-computing/fulltext,

"Absent radical improvements in security technology, we expect that users will use contracts and courts, rather than clever security engineering, to guard against provider malfeasance".

The key point is that terms & conditions should not be left to lawyers and courts only; rather computer scientists and IT practitioners should strive for robust techniques and methodologies capable of specifying formal 'contracts' amenable of verification. To support my claims I will overview some research recently carried out to address those issues.


There will be pre-proceedings handed out at the workshop. Post-proceedings will later appear as LNCS volume.

New June 6, 2013
LNCS proceedings now also available online.
May 8, 2013
WS-FM 2013 will be colocated to BPM 2013 and take place on August 29-30, 2013 in Beijing, China.
May 7, 2013
LNCS Proceedings appeared as LNCS volume 7843 and will be shipped to the authors soon.
July 27, 2012
List of accepted papers and information on the registration published.
June 4, 2012
Submission deadline extended.
February 20, 2012
Program Committee confirmed.
January 16, 2012
Website launched.

Important Dates

Paper submission deadline
June 9, 2012 June 16, 2012
Author notification
July 21, 2012 July 26, 2012
Camera-ready copy
August 4, 2012
Workshop dates
September 6-7, 2012