Sept 4-5, 2015, Madrid


WSFM/BEAT is a symposium held on two days. The programme on Saturday is joined with the FOCLASA workshop Details about the programme can be found below.

Friday September 4: WSFM/BEAT

Session 1: 15:00 - 16:30

The analysis of concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give imprecise answers or do not scale.

This talk presents a proof technique that we have used to analyse these programs for deriving properties such as deadlock freedom, upper bounds of resource usages and of the computational cost. The proof technique is modular and consists of two parts:

  • a type (inference) system that associates a behavioural type to a program and an algorithm for analysing the behavioural type. Behavioural types are simple terms that also feature recursion and name creation -- therefore their underlying model is infinite state.
  • The proof technique, being modular, may be applied to several languages by simply changing the type system and support several behavioural type verification algorithms.

Session 2: 17:00 - 19:15

In this paper we present an algorithm for session type inference for the pi-calculus. Type inference for session types has previously been achieved by either imposing limitations and restriction on the pi-calculus, or by converting the problem to linear types, conducting type inference on the new problem, and converting the result back to session types. Our approach is based on constraint generation and solving. We generate constraints for a process based on its syntactical components, and afterwards solve the generated constraints in a predetermined order. We prove the soundness, completeness, and termination of this approach.

In this paper we propose a formal framework for studying privacy preserving access control based on the notion of purpose. Our framework employs the pi-calculus with groups accompanied by a type system for capturing privacy requirements. It also incorporates a privacy policy language which captures how different entities within a system, which are distinguished by their roles, may access sensitive information and the purposes for which they are allowed to process the data. We show that a system respects a policy if the typing of the system is compatible with the policy. We illustrate our methodology via analysis of privacy-aware services of a health-care system.

We address the problem of designing distributed applications which require the interaction of loosely-coupled and mutually distrusting services. In this setting, services can use contracts to protect themselves from unsafe interactions with the environment: when their partner in an interaction does not respect its contract, it can be be blamed (and punished) by the service infrastructure. We extend a core calculus for contract-oriented services, by using a semantic model of contracts which subsumes various kinds of behavioural types. In this formal framework, we study some notions of honesty for services, which measure their ability to respect contracts, under different assumptions about the environment. In particular, we find conditions under which these notions are (un)decidable.

20:30: Symposium Dinner

The dinner is at: "Sazadon", Calle de Gaztambide, 44, 28015 Madrid.

Saturday September 5: Joint programme WSFM/BEAT and FOCLASA

Session 3: 08:50 - 10:30

Programmers often code up asynchronous message-passing systems as communicating finite-state actors. An actor in some state listens for messages, responds to those messages, and transitions to another state. Most of these systems allow messages to carry actor addresses.

This paper presents a kernel language for implementing and specifying such systems. A specification consists of finite-state machines, expressing what kind of messages each component should expect and what kind of actions it should take in response. In addition, a specification may prescribe how a component may use an address received from a message as well as how a component handles inputs on addresses that it sends out. Finally, a conformance relation articulates when an implementation meets such a specification.

Session 4: 11:00 - 13:00

We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service communication: synchronous communication with patient non-preemptable or impatient invocations, or asynchronous communication. Correspondingly, relations concerning behavioural contracts and choreographic descriptions are considered, where a contract for each communicating party is, e.g., derived by projection.

Contract refinement relations are induced as the maximal preoders which preserve contract compliance and global traces. The obtained preorders are then characterized in terms of a new form of testing, called compliance testing (where not only tests must succeed but also the system under test), and compared with classical preorders. Moreover, recent work about adaptable choreographies and behavioural contracts is presented, where the theory above is extended to update mechanisms allowing choreographies/contracts to be modified at run-time by internal (self-adaptation) or external intervention.

Session 5: 14:45 - 16:00
Session 6: 16:30 - 18:15


Symposium dinner
The dinner starts at 20:30. The location is "Sazadon", Calle de Gaztambide, 44, 28015 Madrid, closeby Moncloa.
Programme known
The Programme of the symposium has been posted on this website!
Invited speakers known
We are happy to anounce that Cosimo Laneve and Javier Esparza will give an invited talk.
Deadline extension
The deadlines have been extended to July 1 and 3.
February, 2015
Website of WSFM/BEAT 2015 is online.