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.
翻译:用户平面函数(UPF)旨在为3GPP 5G核心网络提供网络服务,这些服务需要按需求廉价地以可核实的特性实施,现有的网络数据机编程语言不适宜于完成这项任务。为UPF提供了一个新的软件范例。它受到一个并行的被动反应系统模型的启发,该系统的每个组成部分在概念上都以一个扩展的有限状态机器为模型,并核查其产品。我们展示了如何为UPF的一个例子计算出这种产品,以及如何推断出其变化状态,从而消除了正式单独核实产品的必要性。代码可以从产品中产生,再在苍蝇上生成,以保持对UPF必须处理的网络流量概率分布的最佳性。