Published: 12th September 2011
DOI: 10.4204/EPTCS.68
ISSN: 2075-2180


Proceedings Fifth Workshop on
Formal Languages and Analysis of Contract-Oriented Software
Málaga, Spain, 22nd and 23rd September 2011

Edited by: Ernesto Pimentel and Valentín Valero

Ernesto Pimentel and Valentín Valero
Invited Presentation: Behaviour-Aware Generation of Mashups
Antonio Brogi
Invited Presentation: Contracts as Dynamic Condition Response Graphs
Thomas Hildebrandt
Timed Automata Semantics for Visual e-Contracts
Enrique Martínez, M. Emilia Cambronero, Gregorio Díaz and Gerardo Schneider
Distributed System Contract Monitoring
Adrian Francalanza Ph.D, Andrew Gauci M.Sc and Gordon Pace Ph.D
Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages
Francois Hantry and Mohand-Said Hacid
From Contracts in Structured English to CL Specifications
Seyed M. Montazeri, Nivir K.S. Roy and Gerardo Schneider
A Software Tool for Legal Drafting
Daniel Gorín, Sergio Mera and Fernando Schapachnik


This volume includes the proceedings of the 5th Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'11). The FLACOS Workshops serve as annual meeting places to bring together researchers and practitioners working on language-based solutions to contract-oriented software development. High-level models of contracts are needed as a tool to negotiate contracts and provide services conforming to them. This Workshop provides language-based solutions to the above issues through formalization of contracts, design of appropriate abstraction mechanisms, and formal analysis of contract languages and software. Detailed information about the FLACOS 2011 Workshop can be found at . The 5th edition of the FLACOS Workshop was organized by the University of Málaga. It took place in Malaga, Spain, during September 22-23, 2011.

The program of this edition consisted of 5 regular papers, selected by the following international Program Committee:

The selected papers tackle different issues of great relevance for the FLACOS community: semantics of visual contracts, distributed monitoring of contracts, derivation of formal specifications from natural language descriptions of contracts, automated support for legal drafting, evolution of rules in contract and service-based systems. The workshop also included two invited presentations by Antonio Brogi and Thomas Hildebrandt.

The Organizing Committee was chaired by Ernesto Pimentel, from the University of Málaga, together with the following team: Carlos Canal, Javier Cámara, Javier Cubo, J. Antonio Martín, and Meriem Quederni.

We would like to thank all the members of the program committee for their great work during the review process, the authors for submitting papers, and the participants for attending the workshop in Málaga.

Ernesto Pimentel
Valentín Valero

Behaviour-Aware Generation of Mashups

Antonio Brogi (University of Pisa, Italy)

So called service behaviour — i.e., the (partial) order according to which service operations are invoked and offered — plays an important role in the generation of correct service compositions and mashups. In this talk we discuss how behavioural information can be simply included in service descriptions and fruitfully exploited to verify the correctness of service mashups. We will exemplify some of the advantages of including behavioural information in service descriptions by illustrating a concrete example of design of a plug-in for an existing service composition framework. The plug-in analyses service behaviour information —represented as simple constraints overs service operations— to support a behaviour-aware generation of mashups.

Contracts as Dynamic Condition Response Graphs

Thomas Hildebrandt (IT University of Copenhagen, Denmark)

The declarative process language Dynamic Condition Response (DCR) Graphs has been developed in the Trustworthy Pervasive Healthcare Services (TrustCare) research project as a formalization of the workflow language employed by the industrial partner, Resultmaker. It serves both as a formal specification/contract language and as an executable workflow language. In the talk we present the formalism and give examples of its applications. In particular we present a recent technique for synthesizing a set of local, communicating DCR Graphs from a global process description. We will also present ongoing work on extending DCR Graphs with time, data and exceptions/compensations.