Service adaptation
Antonio Brogi, University of Pisa, Italy

Software integration needs to face various kinds of incompatibilities that unavoidably arise when composing services developed by different parties. To overcome signature, behaviour, or security mismatches, various techniques supporting flexible and non-intrusive service adaptation have been developed. In this talk, we will first exemplify the problems and the potential of behaviour adaptation, also when in adverse conditions. We will then try to discuss some of the general issues involved in service adaptation, such as dynamicity, correctness, cross-layerness, and cost.

Short Biography: Antonio Brogi, Ph.D., is full professor at the Department of Computer Science of the University of Pisa. His research interests include service-oriented computing, coordination and adaptation of software elements, formal methods and design of programming languages. He has published the results of his research in over 140 papers in international journals and conferences. He is currently member of the editorial board of the journals "Advances in Computer Science and Engineering", "Computer Languages, Systems and Structures", and "International Journal of Web Science", of the steering committee of the CIbSE, ESOCC, FLACOS, and FOCLASA conference series, and he has participated in the program committee of various international conferences in his areas of research. He has been participating as project or site leader in various international research projects. He spent one year as visiting professor at UCLA (USA) and he has spent invited research stays in Spain, Portugal and Peru.

CLOSE
Towards accountability by design
Daniel Le Métayer

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".

CLOSE
Conformance Verification of Normative Specifications using C-O Diagrams
Gregorio Díaz, Luis Llana, Valentin Valero and Jose Antonio Mateo

C-O Diagrams have been introduced as a means to have a visual representation of normative texts and electronic contracts, where it is possible to represent the obligations, permissions and prohibitions of the different signatories, as well as what are the penalties in case of not fulfillment of their obligations and prohibitions. In such diagrams we are also able to represent absolute and relative timing constrains. In this paper we consider a formal semantics for C-O Diagrams based on a network of time automata and we present several relations to check the consistency of a contract in terms of realizability, to analyze whether an implementation satisfies the requirements defined on its contract, and to compare several implementations using the executed permissions as criteria.

CLOSE
Contracts for Interacting Two-Party Systems
Gordon J. Pace and Fernando Schapachnik

This article deals with the interrelation of deontic operators in contracts – an aspect often neglected when considering only one of the involved parties. On top of an automata-based semantics we formalise the onuses that obligations, permissions and prohibitions on one party impose on the other. Such formalisation allows for a clean notion of contract strictness and a derived notion of contract conflict that is enriched with issues arising from party interdependence.

CLOSE
What if contracts are violated? (short paper)
Massimo Bartoletti, Alceste Scalas, Emilio Tuosto and Roberto Zunino

We develop a theory of contracting systems, where behavioural contracts may be violated by dishonest participants after they have been agreed upon - unlike in traditional approaches based on behavioural types.

We consider a generic contract model, and we embed it in a calculus that allows distributed participants to advertise contracts, reach agreements, and realise them (or choose not to). We highlight some research directions about the problem of determining the honesty of participants.

CLOSE
Simplifying Contract-Violating Traces
Adrian Francalanza, Christian Colombo and Ian Grima

Contract conformance is hard to determine statically, prior to the deployment of large pieces of software. A scalable alternative is to monitor for contract violations post-deployment: once a violation is detected, the trace characterising the offending execution is analysed to pinpoint the source of the offense. A major drawback with this technique is that, often, contract violations take time to surface, resulting in long traces that are hard to analyse. In this paper proposes a methodology and presents an accompanying tool for simplifying traces thus assisting contract-violation debugging.

CLOSE
Dynamic Contracts for Ensuring Component Interoperability
Kaisa Sere and Linas Laibinis

The approaches based on the notions of a contract and contract-based development (e.g., design-by-contract programming) are steadily gaining popularity in software engineering. Traditionally, contracts are used as static formal annotations of a particular component that can be referred while validating or verifying the design and functionality of the overall system. In this presentation, we will offer a slightly different take on the notion of contracts, making them a part of the dynamic system state. In our representation of a component system, components can dynamically engage into and disengage from different contracts, each of which defines possible activities of several involved components. Moreover, since active contracts are a part of the dynamic system state, contract definitions can directly refer to other contracts a particular contract component may be required to be involved in. The presentation will briefly describe a formalisation of dynamic contracts as well as give some examples of such contracts.

CLOSE
A History of BlockingQueues (short paper)
Marina Zaharieva-Stojanovski, Marieke Huisman and Stefan Blom

This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object’s state, we specify it in terms of the object’s state history. A history is defined as a list of state updates, which at all points can be related to the actual object’s state.

We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.

CLOSE
Towards a Framework for Conflict Analysis of Normative Texts in Controlled Natural Language
Gerardo Schneider

Our aim is to detect whether texts written in natural language contain normative conflicts (i.e., whether there are conflicting obligations, permissions and prohibitions). We present AnaCon, a framework where such texts are written in a Controlled Natural Language (CNL) and automatically translated into the formal language CL using the Grammatical Framework (GF). In AnaCon such CL expressions are analyzed for normative conflicts by the tool CLAN which gives a counter-example in case a conflict is found. We also discuss the practicality of the approach, and give a short overview on the research challenges and future directions in the area.

CLOSE
Using UML 2.0 to Model Web Service with Distributed Resources
María Emilia Cambronero

Web services managing distributed resources is a technology that allows the user to have an easier and cheaper mechanism to access and manage distributed resources. The formal modeling of web services with distributed resources thus becomes very important in order to understand accuratelytheir behavior. In this paper, we present a framework to model web services with distributed resources by using a widely adopted standard (UML 2.0), enriched with resource management capabilities, on the basis on a standard for the management of distributed resources, WSRF.

CLOSE
Session Types for Trustworthy Pervasive Healthcare Services
Thomas Hildebrandt

The talk takes outset in and discuss how to combine work presented as a poster at DEBS 2012 joint with Zanitti in the Genie project and work presented in a paper at FHIES 2012 joint with Henriksen, Nielsen, Yoshida and Henglein in the Trustworthy Pervasive Healthcare Services (TrustCare) project.

In the DEBS 2012 poster we propose a declarative, Process-oriented Event-based Programming Language (PEPL) aimed at pervasive, context-sensitive workflow management and process-oriented systems.

In the FHIES 2012 paper we propose a new theory of multiparty session types extended with propositional assertions and symmetric sum types for modeling collaborative distributed workflows. Multiparty session types statically guarantee that workflows are type-safe and deadlock-free, facilitate automatic generation of participant-specific (local) workflow protocols from global descriptions, and support flexible implementation of local workflows guaranteed to be compliant with the (global) workflow protocols. The extensions with assertions and symmetric sum types support expressing state-based (pre)conditions and consensual multiparty synchronisation, which are common in complex distributed workflows.

We have demonstrated in the FHIES 2012 paper the theory's applicability to clinical practice guidelines (CPGs) by a prototype implementation targeting mobile healthcare applications. The prototype compiles declarative healthcare workflows specified in a flexible spreadsheet-formatted process matrix into type-checked multiparty processes, which are subsequently interpreted on a server. The interpreter provides interface hooks for access by mobile clients. For demonstration purposes we have implemented a role-tailored graphical user interface (GUI) running on Android tablet computers, which reflects the pervasiveness requirements common to clinical and home healthcare scenarios. A physician has, with little prior training, successfully used the prototype to design her own healthcare workflow as a process matrix, employing instantaneous test and usage feedback from the automatically generated client.

In the talk we discuss the possibilities of using the PEPL language as source language in place of the spreadsheet-formattet process matrix.

CLOSE
 

FLACOS 2012
Sixth Workshop on
Formal Languages and Analysis of
Contract-Oriented Software



Bertinoro, Italy, 19 September 2012
Co-located with ESOCC

About FLACOS

The fast evolution of the Internet has popularized service-oriented architectures with their promise of dynamic IT-supported inter-business collaborations and rich repositories in the cloud. Realizing this promise involves integrating services which are geographically distant and are offered by a variety of organizations which do not fully trust each other.Indeed, collaboration presumes a minimum level of mutual trust. Wherever trust is perceived as insufficient, people turn to contracts as a mechanism to reduce risks.

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 analysis requires that contracts are abstracted from applications to become amenable to formal reasoning using formal language techniques.

The aim of this workshop is to bring together researchers and practitioners working on language- or application-based solutions to the above problem 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.

Scope

Topics of interest to the workshop include, but are not strictly limited to:

  • Formal languages for contracts
  • Contract-oriented software development
  • Formal analysis of contracts, including static analysis, runtime verification, and model checking techniques
  • Contract testing
  • Contract synthesis
  • Contract transformation and contract refinement
  • Contract negotiation, discovery and monitoring
  • Rich and behavioural interfaces
  • Service modeling, service-oriented analysis and design
  • Contract- and model-driven Web service engineering
  • Service quality and service interface design guidelines
  • Service Level Agreements for Web services
  • Contracts for service security and privacy concerns
Programme

09:00-10:00Joint invited speaker with ESOCC: Service Adaptation
Antonio Brogi ABSTRACT
10:00-10:25Coffee break
10:25-10:30Welcome to FLACOS
10:30-11:00Invited talk: Towards accountability by design
Daniel Le Métayer ABSTRACT
11:00-11:30Conformance Verification of Normative Specifications using C-O Diagrams
Gregorio Díaz, Luis Llana, Valentin Valero and Jose Antonio Mateo ABSTRACT
11:30-12:00Contracts for Interacting Two-Party Systems
Gordon J. Pace and Fernando Schapachnik ABSTRACT
12:00-12:30What if contracts are violated? (short paper)
Massimo Bartoletti, Alceste Scalas, Emilio Tuosto and Roberto Zunino ABSTRACT
12:30-14:00Lunch
14:00-14:30Simplifying Contract-Violating Traces
Adrian Francalanza, Christian Colombo and Ian Grima ABSTRACT
14:30-15:00Dynamic Contracts for Ensuring Component Interoperability
Kaisa Sere and Linas Laibinis ABSTRACT
15:00-15:30A History of BlockingQueues (short paper)
Marina Zaharieva-Stojanovski, Marieke Huisman and Stefan Blom ABSTRACT
15:30-16:00Coffee break
16:00-16:30Towards a Framework for Conflict Analysis of Normative Texts in Controlled Natural Language
Gerardo Schneider ABSTRACT
16:30-17:00Using UML 2.0 to Model Web Service with Distributed Resources
María Emilia Cambronero ABSTRACT
17:00-17:30Session Types for Trustworthy Pervasive Healthcare Services
Thomas Hildebrandt ABSTRACT
17:30-17:35Closing session

Registration Information

Registration to the workshop, as well as hotel reservation, can be done directly via the ESOCC 2012 webpage - managed by the "University Residential Center of Bertinoro". Click here to proceed directly with your registration and reservation. Note that early registration closes on 18 August 2012.

Important Dates
Paper submission deadline (extended)       June 22, 2012
Notification of acceptance: July 12, 2012
Final version due: July 30, 2012
Early registration deadline: August 18, 2012
WORKSHOP: September 19, 2012
Call for Papers

Authors are invited to submit papers presenting their contributions in two different categories. Regular research papers will correspond to original unpublished work, and they must be at most 10 pages long. Work-in-progress and contributions previously submitted for formal publication elsewhere are also permitted with a limit of 5 pages.

Submissions must be formatted in EPTCS style, and they should be submitted in pdf format electronically via the web-based Easychair website.

Accepted regular papers will be published in Electronic Proceedings in Theoretical Computer Science (EPTCS). After the workshop, selected papers will be published in a special issue of the Journal of Logic and Algebraic Programming (Elsevier), following the standard reviewing process of the journal.

A text version of the call for papers can be found here.

Programme Committee
Steering Committee
Previous Editions of FLACOS
Contact information

For any further information, you may contact us at flacos12@cs.um.edu.mt