Network slicing is a modern 5G technology that provides efficient network experience for diverse use cases. It is a technique for partitioning a single physical network infrastructure into multiple virtual networks, called slices, each equipped for specific services and requirements. In this work, we particularly deal with radio access network (RAN) slicing and resource allocation to RAN slices. In 5G, physical resource blocks (PRBs) being the fundamental units of radio resources, our main focus is to allocate PRBs to the slices efficiently. While addressing a spectrum of needs for multiple services or the same services with multi-priorities, we need to ensure two vital system properties: i) fairness to every service type (i.e., providing the required resources and a desired range of throughput) even after prioritizing a particular service type, and ii) PRB-optimality or minimizing the unused PRBs in slices. These serve as the core performance evaluation metrics for PRB-allocation in our work. We adopt the 3-layered hierarchical PRB-partitioning technique for allocating PRBs to network slices. The case-specific, AI-based solution of the state-of-the-art method lacks sufficient correctness to ensure consistent system performance. To achieve guaranteed correctness and completeness, we leverage formal methods and propose the first approach for a fair and optimal PRB distribution to RAN slices. We formally model the PRB-allocation problem as a 3-layered framework, FORSLICE, specifically by employing satisfiability modulo theories. Next, we apply formal verification to ensure that the desired system properties: fairness and PRB-optimality, are satisfied by the model. The proposed method offers an efficient, versatile and automated approach compatible with all 3-layered hierarchical network structure configurations, yielding significant system property improvements compared to the baseline.

翻译：网络切片是一种现代5G技术，可为多样化用例提供高效网络体验。该技术通过将单一物理网络基础设施划分为多个虚拟网络（称为切片），每个切片针对特定服务与需求进行配置。本研究聚焦于无线接入网（RAN）切片及RAN切片的资源分配问题。在5G中，物理资源块（PRB）作为无线资源的基本单元，我们的核心目标是将PRB高效分配给各切片。在满足多服务或多优先级同类服务的频谱需求时，需确保两个关键系统属性：i) 公平性——即使在优先处理某类服务后，仍为所有服务类型公平分配所需资源与目标吞吐量范围；ii) PRB最优性——最小化切片中未使用的PRB。这些指标构成了本工作中PRB分配的核心性能评估标准。我们采用三层分层PRB划分技术进行网络切片资源分配。现有最先进方法基于特定场景的AI解决方案，缺乏确保系统性能一致性的充分正确性。为实现可保证的正确性与完备性，我们引入形式化方法，首次提出面向RAN切片的公平最优PRB分配方案。具体而言，我们通过可满足性模理论（SMT）将PRB分配问题形式化为三层框架FORSLICE，并通过形式化验证确保模型满足公平性与PRB最优性这两个关键系统属性。所提方法提供了一种兼容所有三层分层网络结构配置的高效、通用且自动化方案，与基线方法相比，显著提升了系统属性性能。