  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.
