Expressive specification and verification of choreographies

Distributed computing is becoming ever more important. However, designing and implementing distributed systems correctly is notoriously difficult. An important factor in this is the interplay between participants in such a system: certain tasks are allowed concurrently, while others are dependent on each other. Coordinating participants requires communication between them, which can be specified using communication protocols. Choreographies are a specific notation for communication protocols, which specifies them from a global perspective and have the benefit of guaranteeing certain desirable properties by construction. As a drawback, there are also more restrictions on the communication patterns they can specify. The first part of this thesis contributes to removing these restrictions. We study an existing operator from formal language theory, called shuffle on trajectories, and show how it can be used in a choreography language to specify a large class of behaviour, while preserving desirable properties.

A second problem is that it may be impossible to implement certain communication patterns in a way that precisely matches a specification; we then say that that specification is not realisable. In general, determining realisability takes exponential time or is undecidable. The second part of this thesis contributes to the development of a rich yet polynomial realisability analysis. We introduce a new model for the behaviour of choreographies, based on partially ordered sets: these `branching pomsets’ are capable of compactly modelling combinations of concurrency and choice, which typically occur in choreographies. We then compare this model with the existing literature on event structures, a class of related models. We define well-formedness conditions on the structure of branching pomsets, which are easy to check, and we show that they are sufficient to prove realisability of the modelled communication protocol. Finally, we discuss an implementation of branching pomsets and the described analysis.