Skip to main content

A Theory of Composing Protocols

Bocchi, Laura, Orchard, Dominic A., Voinea, Laura (2022) A Theory of Composing Protocols. The Art, Science, and Engineering of Programming, 7 (2). Article Number 6. ISSN 2473-7321. (doi:10.22152/ (KAR id:98303)

PDF Publisher pdf
Language: English

Click to download this file (1MB) Preview
[thumbnail of main.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF (short version) Publisher pdf
Language: English

Click to download this file (721kB) Preview
[thumbnail of short version]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


In programming, protocols are everywhere. Protocols describe the pattern of interaction (or communication) between software systems, for example, between a user-space program and the kernel or between a local application and an online service. Ensuring conformance to protocols avoids a significant class of software errors. Subsequently, there has been a lot of work on verifying code against formal protocol specifications. The pervading approaches focus on distributed settings involving parallel composition of processes within a single monolithic protocol description. However we observe that, at the level of a single thread/process, modern software must often implement a number of clearly delineated protocols at the same time which become dependent on each other, e.g., a banking API and one or more authentication protocols. Rather than plugging together modular protocol-following components, the code must re-integrate multiple protocols into a single component.

We address this concern of combining protocols via a novel notion of ‘interleaving’ composition for protocols described via a process algebra. User-specified, domain-specific constraints can be inserted into the individual protocols to serve as ‘contact points’ to guide this composition procedure, which outputs a single combined protocol that can be programmed against. Our approach allows an engineer to then program against a number of protocols that have been composed (re-integrated), reflecting the true nature of applications that must handle multiple protocols at once.

We prove various desirable properties of the composition, including behaviour preservation: that the composed protocol implements the behaviour of both component protocols. We demonstrate our approach in the practical setting of Erlang, with a tool implementing protocol composition that both generates Erlang code from a protocol and generates a protocol from Erlang code. This tool shows that, for a range of sample protocols (including real-world examples), a modest set of constraints can be inserted to produce a small number of candidate compositions to choose from.

As we increasingly build software interacting with many programs and subsystems, this new perspective gives a foundation for improving software quality via protocol conformance in a multi-protocol setting.

Item Type: Article
DOI/Identification number: 10.22152/
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: Engineering and Physical Sciences Research Council (
European Union (
Depositing User: Laura Bocchi
Date Deposited: 24 Nov 2022 12:57 UTC
Last Modified: 25 Nov 2022 10:26 UTC
Resource URI: (The current URI for this page, for reference purposes)
Bocchi, Laura:
Orchard, Dominic A.:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.