Choreography-driven Programming and Security

New technologies and styles of software systems such as multi-core processors, web services and ubiquitous computing are contributing to a shift in software architectures and systems, where communication is the norm rather than the exception. Programming such distributed communicating systems, however, is known to be hard as it exposes programmers to several new levels of complexity including deadlock/livelock and diverse forms of partial failure, and current programming languages and methodologies lack formal foundations and techniques for ensuring safety and security properties.

Choreography-driven programming is an emerging paradigm for communication-based systems based on the idea that the pattern of interactions among individual peers (known as end-points) is specified by a global description (often referred to as choreography). Such a global description allows to abstract from local input/output primitives and focus on the system global flow of interactions avoiding typical concurrency problems, such as races over a synchronisation and deadlocks. However, since communication-based systems ultimately consist of end-point behaviour, global descriptions demand a mapping into programs containing the necessary input/output operations for each endpoint. Such a translation is often referred to as end-point projection (EPP). EPP is often coupled with its reverse operation, known as global view extraction (GVE), which maps end-point behaviour into a choreography. EPP and GVE provide what is best known as round-trip engineering: existing source code can be abstracted and converted into a specification, subjected to software engineering methods and then converted back.

The aim of this project is to provide mathematical foundations for choreography driven programming covering realistic communication and security protocols and supporting algorithms for provable correct mappings between choreography and end-points. Our hypothesis is that this foundation can be built starting from the recent work by the PI and collaborators. The aim is made feasible by the PI’s experience on formal foundations of communication-based and service-oriented computing, the local competences at the host organisation and a unique combination of expertise among the PI’s international collaborators, namely Dr. K. Honda and Dr N. Yoshida, both experts in concurrency theory, Prof. J. Guttman, a security expert, and Dr. S. Ross-Talbot, W3C WS-CDL working group co-chair.