Published: 8th September 2012
DOI: 10.4204/EPTCS.94
ISSN: 2075-2180


Proceedings Sixth Workshop on
Formal Languages and Analysis of Contract-Oriented Software
Bertinoro, Italy, 19 September 2012

Edited by: Gordon J. Pace and Anders P. Ravn

Gordon J. Pace and Anders P. Ravn
Invited Presentation: Accountability by Design
Daniel Le Métayer
Conformance Verification of Normative Specifications using C-O Diagrams
Gregorio Díaz, Luis Llana, Valentín Valero and Jose Antonio Mateo
Simplifying Contract-Violating Traces
Christian Colombo, Adrian Francalanza and Ian Grima
Contracts for Interacting Two-Party Systems
Gordon J. Pace and Fernando Schapachnik
A History of BlockingQueues
Marina Zaharieva-Stojanovski, Marieke Huisman and Stefan Blom


Preface of FLACOS 2012

The importance of identifying and enforcing contracts regulating the behaviour of different entities has steadily increased over the past years. A major driving force is the fast evolution of the Internet which has popularized service-oriented architectures with their promise of dynamic IT-supported inter-business collaborations and rich repositories in the cloud. The effective deployment of such architectures requires solutions to complex integration issues between a variety of organizations which may not fully trust each other. Wherever trust is perceived as insufficient, people turn to contracts as a mechanism to reduce risks and to ensure a minimum level of trust, thus enabling effective collaboration to take place.

The ability to negotiate contracts for a wide range of aspects and to provide services conforming to them is a most pressing need in service-oriented architectures. High-level models of contracts are making their way into the area, but application developers are still left to their own devices when it comes to writing code that will comply with a contract concluded before service provision. At the programming language level, contracts appear as separate concerns that crosscut through application logic. Therefore there is a need for contract analysis tools that extract abstracted models from applications so they become amenable to formal reasoning using formal language techniques.

Since its inception, the aim of of FLACOS has been that of bringing together researchers and practitioners working on language- or application-based solutions to these problems through the formalization of contracts, the design of appropriate abstraction mechanisms, and tools and techniques for analysis of contracts, and analysis, testing and monitoring of conformance to contracts by applications.

This is the sixth edition of the workshop, which has been held on an annual basis since 2007. This edition is being held in conjunction with the European Conference on Service-Oriented and Cloud Computing (ESOCC 2012), which gives an appropriate context to the theme of the workshop.

We wish to thank the members of the Programme Committee and the participants for their contributions to the workshop.

Gordon J. Pace
Anders P. Ravn
August 2012

Accountability by Design

Daniel Le Métayer (Inria Insa Lyon - Citi)

Many efforts have been devoted in the computer science community to "a priori" verifications of properties of IT systems. In many situations however, properties cannot be controlled or imposed a priori. This can be the case for a variety of reasons: certain actions can be out of control of a given system (they may depend on other systems or on human beings), the compliance property itself may be impossible to check on the fly (it can depend on contextual information or on future events) or it may just be too cumbersome to impose a priori verifications in practice. Typical illustrations of this situation are the compliance with privacy or intellectual property protection rules, or the verification of Service Level Agreement commitments for on-line services. Accountability is an attractive alternative that relies on "a posteriori" controls to check that a system has complied with the rules. Accountability has been studied in a variety of contexts such as politics, sociology, ethics, law and also computer science, sometimes with slightly different meanings. But accountability also raises challenges that should not be underestimated. In this talk, we will review the definitions of accountability and their relationships with the notions of responsibility and liability. We will identify the main challenges raised by accountability and argue that it should not be taken for granted but should result from a deliberate "accountability by design approach".