https://programming-journal.org/2023/7/6/

The Art, Science, and Engineering of Programming
 [?]  Upcoming Submission Deadline: June 1, 2024

A Theory of Composing Protocols

Laura Bocchi^1 OrcidLogo, Dominic Orchard^2 OrcidLogo, and A. Laura
Voinea^3 OrcidLogo

The Art, Science, and Engineering of Programming, 2023, Vol. 7, Issue
2, Article 6

ae_reusable

Submission date: 2022-06-01
Publication date: 2022-10-15
DOI: https://doi.org/10.22152/programming-journal.org/2023/7/6
Full text: PDF
Related Artifact: https://doi.org/10.5281/zenodo.7105666

Abstract

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.

 1. University of Kent, UK
    OrcidLogo https://orcid.org/0000-0002-7177-9395

 2. University of Kent, UK / University of Cambridge, UK
    OrcidLogo https://orcid.org/0000-0002-7058-7842

 3. University of Glasgow, UK
    OrcidLogo https://orcid.org/0000-0003-4482-205X

Toggle navigation

  * Volume 8, Issue 3
  * Volume 8, Issue 2
  * Volume 8, Issue 1
  * Volume 7, Issue 3
  * Volume 7, Issue 2
  * Volume 7, Issue 1
  * Volume 6, Issue 3
  * Volume 6, Issue 2
  * Volume 6, Issue 1
  * Volume 5, Issue 3
  * Volume 5, Issue 2
  * Volume 5, Issue 1
  * Volume 4, Issue 3
  * Volume 4, Issue 2
  * Volume 4, Issue 1
  * Volume 3, Essays
  * Volume 3, Issue 3
  * Volume 3, Issue 2
  * Volume 3, Issue 1
  * Volume 2, Issue 3
  * Volume 2, Issue 2
  * Volume 2, Issue 1
  * Volume 1, Issue 2
  * Volume 1, Issue 1
  * About
  * Purpose
  * Boards
  * Awards
  * Publisher
  * Volumes
  * Call for Papers
  * Artifact Evaluation
  * Timeline
  * Submissions
  * Copyright
  * Article feed (atom)
  * Article feed (RSS)

  * The Journal
  * 
      + About
      + Purpose and Operation
      + Boards
      + Awards
      + Publisher
      + Volumes
  * For Authors
  * 
      + Call for Papers
      + Artifact Evaluation
      + Timeline
      + Submissions
      + Copyright
  * Issues
  * 
      + Volume 8, Issue 3
      + Volume 8, Issue 2
      + Volume 8, Issue 1
      + Volume 7, Issue 3
      + Volume 7, Issue 2
      + Volume 7, Issue 1
      + Volume 6, Issue 3
      + Volume 6, Issue 2
      + Volume 6, Issue 1
      + Volume 5, Issue 3
      + Volume 5, Issue 2
      + Volume 5, Issue 1
      + Volume 4, Issue 3
      + Volume 4, Issue 2
      + Volume 4, Issue 1
      + Volume 3, Essays
      + Volume 3, Issue 3
      + Volume 3, Issue 2
      + Volume 3, Issue 1
      + Volume 2, Issue 3
      + Volume 2, Issue 2
      + Volume 2, Issue 1
      + Volume 1, Issue 2
      + Volume 1, Issue 1

AOSA, Inc
AOSA, Inc

 1. The Art, Science, and Engineering of Programming
 2. ISSN 2473-7321
 3. DOI 10.22152/programming-journal.org
 4. (c) 2016-2024 AOSA