  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.

Software Engineering;Computation and Language;Programming Languages