论文标题
通过可计算产品进行网络编程
Network Programming via Computable Products
论文作者
论文摘要
用户平面功能（UPF）旨在在3GPP 5G核心网络中提供网络服务。这些服务需要用可证明的属性廉价地按需实施。现有的网络数据平台编程语言不符合任务。为UPF提供了新的软件范式。它的启发是通过模型检查并发的反应系统，从概念上讲，系统的每个组件都被建模为扩展有限状态机，并验证其产品。我们展示了如何为UPF的一个示例及其状态不变性的一个示例计算，从而消除了单独正式验证产品的需求。代码可以从产品中生成，并可以随时再生，以保持UPF必须处理的网络流量的概率分布最佳。
The User Plane Function (UPF) aims to provide network services in the 3GPP 5G core network. These services need to be implemented on demand inexpensively with provable properties. Existing network dataplane programming languages are not up to the task. A new software paradigm is presented for the UPF. It is inspired by model checking a concurrent reactive system where conceptually each component of the system is modeled as an extended finite-state machine and their product is verified. We show how such a product can be computed for one example of a UPF and how its state invariants can be inferred, thereby eliminating the need to formally verify the product separately. Code can be generated from the product and regenerated on the fly to remain optimal for the probability distribution of network traffic the UPF must process.
