组合协议的理论
摘要：在编程中，协议无处不在。协议描述了软件系统之间的交互（或通信）模式，例如用户空间程序与内核之间或本地应用程序与在线服务之间的交互。确保符合协议可以避免一类重要的软件错误。随后，在验证代码与正式协议规范的工作方面进行了大量工作。普遍的方法集中在涉及单个统一协议描述中的进程的并行组合的分布式环境中。然而，我们观察到，在单个线程/进程的级别上，现代软件往往必须同时实现多个明确定义的协议，这些协议相互依赖，例如银行API和一个或多个认证协议。代码不是将模块化的遵循协议的组件连接在一起，而是必须将多个协议重新集成到一个单一的组件中。 我们通过一种新颖的通过进程代数描述的协议的“交错”组合概念来解决这个关注点。用户可以在各个协议中插入特定于领域的约束，作为“接触点”来指导此组合过程，输出一个可以进行编程的单个组合协议。我们的方法允许工程师编写针对已经组合（重新集成）的多个协议的程序，反映了必须同时处理多个协议的应用程序的真实性质。 我们证明了组合的各种期望属性，包括行为保持：组合的协议实现了两个组件协议的行为。我们在实际的Erlang环境中演示了我们的方法，使用一个实现协议组合的工具，该工具从协议生成Erlang代码，并从Erlang代码生成协议。该工具显示，对于一系列示例协议（包括真实世界的示例），可以插入一组适度的约束来产生少量可供选择的候选组合。 随着我们越来越多地构建与许多程序和子系统交互的软件，这种新的观点为通过多协议环境中的协议符合性提高软件质量奠定了基础。
作者：Laura Bocchi (University of Kent, UK), Dominic Orchard (University of Kent, UK / University of Cambridge, UK), A. Laura Voinea (University of Glasgow, UK)
论文ID：2203.02461
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-11-08