基于可计算乘积的网络编程

用户面功能（UPF）旨在 3GPP 5G 核心网中提供网络服务。这些服务需以低成本按需实现并具备可证明的性质。现有的网络数据面编程语言无法胜任此任务。我们提出了一种用于 UPF 的新软件范式。其受并发反应式系统模型检测启发，在概念上将该系统的每个组件建模为扩展有限状态机，并验证其乘积。我们展示了对一个 UPF 实例如何计算此类乘积，以及如何推断其状态不变量，从而无需单独对乘积进行形式化验证。代码可由该乘积生成，并动态重新生成以对 UPF 必须处理的网络流量概率分布保持最优。