A Theory of Composing Protocols
A Theory of Composing Protocols
复制标题
DOI：
10.22152/programming-journal.org/2023/7/6
复制
发表时间：
2022-03
期刊：
影响因子：
--
通讯作者：
L. Bocchi;Dominic A. Orchard;A. Voinea
中科院分区：
文献类型：
--
作者：
L. Bocchi;Dominic A. Orchard;A. Voinea
在编程中，协议无处不在。协议描述了软件系统之间的交互(或通信)模式，例如，用户空间程序和内核之间，或者本地应用程序和在线服务之间。确保符合协议可以避免一类重要的软件错误。随后，在对照正式协议规范验证代码方面进行了大量工作。普及的方法侧重于涉及在单个整体协议描述中并行组合进程的分布式设置。然而，我们观察到，在单个线程/进程的级别上，现代软件通常必须同时实现多个相互依赖的清晰描述的协议，例如银行API和一个或多个认证协议。代码必须将多个协议重新集成到单个组件中，而不是将遵循模块化协议的组件插入在一起。我们通过一种新的概念来解决合并协议的问题，该概念通过进程代数描述的协议的“交织”组合。用户指定的、领域特定的约束可被插入到各个协议中，以充当指导该合成过程的“接触点”，该合成过程输出可针对其进行编程的单个组合协议。我们的方法允许工程师针对已组合(重新集成)的多个协议进行编程，这反映了必须同时处理多个协议的应用程序的真实性质。我们证明了组合的各种期望的属性，包括行为保持：组合的协议实现了两个组件协议的行为。我们将在Erlang的实际环境中演示我们的方法，使用一个实现协议组合的工具，该工具既可以从协议生成Erlang代码，也可以从Erlang代码生成协议。该工具表明，对于一系列样本协议(包括真实世界的示例)，可以插入一组适度的约束，以产生少量可供选择的候选组合。随着我们越来越多地构建与许多程序和子系统交互的软件，这种新的视角为在多协议环境下通过协议一致性来提高软件质量提供了基础。
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.