FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services
arXiv:2604.08244v1 [cs.NI] 9 Apr 2026
DEBARPITA BANERJEE∗ , Indian Statistical Institute Kolkata, India SUMANA GHOSH, Indian Statistical Institute Kolkata, India SNIGDHA DAS, Ericsson Research, India SHILPA BUDHKAR, Ericsson Research, India RANA PRATAP SIRCAR, Ericsson Research, India 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 to RAN slices, 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. Additional Key Words and Phrases: RAN Slicing, PRB-Allocation, Network Performance, Formal Verification, Satisfiability Modulo Theories
1 Introduction In telecommunication, network slicing is a technology that allows a shared physical network infrastructure to support multiple, diverse and service-specific virtual networks, called slices. A network slice functions as an independent, secure, and fully operational network environment with its own service level agreements (SLAs). It can be customized to serve different essential system parameters like speed, latency, throughput, reliability, etc., depending on the needs of specific services or user groups. For instance, a network slice designed for IoT devices might prioritize high latency, while another slice for streaming video might focus on high bandwidth. In this work, we consider radio access network (RAN) slicing and specifically focus on the aspect of radio-resource allocation to RAN slices. The fundamental unit of radio resources, available for data transmission, is a physical resource block or PRB. PRB-allocation is an elemental aspect of RAN resource scheduling, which distributes resources (divided ∗
This is the corresponding author
Authors’ Contact Information: Debarpita Banerjee, [email protected], Indian Statistical Institute Kolkata, Kolkata, India; Sumana Ghosh, [email protected], Indian Statistical Institute Kolkata, Kolkata, India; Snigdha Das, [email protected], Ericsson Research, India; Shilpa Budhkar, [email protected], Ericsson Research, India; Rana Pratap Sircar, [email protected], Ericsson Research, India.
1
2
D. Banerjee et al.
into resource blocks) to user equipment (UEs). This work aims to obtain an efficient PRB-allocation strategy for a RAN slicing scenario. In 5G networks and beyond, PRBs need to be distributed among multiple RAN slices corresponding to various services such as, ultra-reliable low-latency communications (URLLC), enhanced mobile broadband (eMBB), massive machinetype communications (mMTC), fixed wireless access (FWA), etc., and also multiple priorities of a single service, e.g., eMBB Premium and eMBB Normal under the eMBB service. Hence, efficiently allocating PRBs is vital to meet differentiated quality of service (QoS) requirements (i.e., the ability to meet the service demands of different types of traffic). A substantial body of existing literature addresses PRB-allocation and RAN slicing in several contexts, such as, media access control layer scheduling perspective [6, 24], resource allocation in remote radio heads [22], virtual network function activation [19], etc. However, our work addresses a different context — the PRB-partitioning technique for allocating PRBs to RAN slices by considering a 3-layered hierarchical network structure of slices and partitions (RAN is divided into physical partitions, which are further sub-divided into logical units or slices). This is Ericsson’s approach to RAN slicing [9] which we follow in this work. To our knowledge, PRB-allocation in such a context remains mostly unexplored in the literature, except the one studied in [15]. We show that our proposed PRB-allocation approach is robust and more efficient as compared to the baseline [15] despite adopting the same PRB-partitioning technique [9].
Motivation. In the context of PRB-partitioning, to cope with the diverse needs for multi-services or the same service with multi-priorities, there must be fair allocations of PRBs to different RAN slices. But at the same time, the optimal distribution of the PRBs among the multi-service-based slices is also a need, especially in the resource-constrained scenarios. A dependable design strategy for PRB-allocation to RAN slices focuses on guaranteeing system properties, like ensuring fairness to each service type, optimal PRB distribution, meeting resource demands for higher priority service types, etc. These are essential factors to be addressed to uphold consistent network performance. The literature specifically lacks a dependable, generic PRB-allocation approach that takes as input any service-partition-slice configuration of the 3-layered hierarchical network structure, and efficiently allocates PRBs to partitions and slices while ensuring the system properties. Although the method ‘Convergence’ proposed in [15] explores PRB-allocation to RAN slices in the 3-layered hierarchical network structure, yet, their AI-planning based solution method is confined to a single case study, generating PRB-allocations only for a fixed configuration of service types, partitions, and slices. Moreover, the AI-based solution of ‘Convergence’ fails to guarantee an acceptable degree of correctness, thus, not sufficient to ensure the continuity of the system performance in the deployment phase all the time. In contrast, to address the issue of correctness, we leverage formal methods [8], a well-proven mathematical technique for specifying and developing correct-by-construction designs of hardware and software systems. It not only verifies and ensures the correct functionalities of the underlying system but also ensures its completeness. Consequently, there is a recent trend of using formal methods in various industrial applications, such as, Internet of Things (IoT) [16], cloud computing [23], cyber-physical systems [11, 12], real-time scheduling [7], design automation [10], etc., over the last decade. Interestingly, in telecommunications, formal methods have been used in call admission control [14], 5G service orchestration [17], secure transmission [5], etc., but not in the domains of RAN slicing and PRB-allocation. Keeping the potential of correctness and completeness of any formal technique, we leverage formal methods to propose strategies for PRB-allocation to RAN slices in a 3-layered hierarchical network structure, which guarantees
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services3 underlying system properties. The novelty of this work lies in being the first to apply formal methods to design an efficient, dependable PRB-allocation framework that ensures system properties and provides differentiated QoS. Overview of the Work. The two important system properties accounted for in our work are: fairness and PRBoptimality, functioning as the key network performance metrics in this work. Here, fairness particularly indicates the guarantee of providing the desired amount of PRBs and maintaining the throughput requirements for every service type, while PRB-optimality indicates minimized unused PRBs in slices. Furthermore, best-effort services (services having no specific QoS requirements like eMBB, FWA, etc.) are served with the unallocated PRBs (i.e., the unused spectrum or the PRBs not yet allocated to the slices). Given a fixed total of available PRBs within a specific time interval, we incorporate user arrival data that follows the prescribed user distributions for different service types, as defined by 5G network protocols. The objective is to judiciously allocate PRBs to partitions and slices, thereby leaving sufficient unallocated resources to support besteffort services effectively. However, fairness to all service types (like eMBB, FWA, URLLC, mMTC) must be guaranteed simultaneously, preserving the service type priorities. In this work, we prioritize the eMBB Premium service type above all others, guaranteeing its throughput requirements are met throughout runtime. To this end, we develop a hierarchical 3-layered framework, FORSLICE, that formally models the 3-layered hierarchical network structure, and our goal is to ensure that the system properties are satisfied throughout the runtime. This formal framework is fully-automated to handle the automatic generation of PRB-allocations for any 3-layered hierarchical network structure as input. In particular, we use satisfiability modulo theories (SMT), a popular constraint-solving technique as the underlying formal method. We formulate a set of constraints for each layer modeling its functionality and working semantics. We also formalize the system properties. All the constraints are then fed to the SMT-solver for verification. A satisfiable answer returned by the solver provides an optimal PRB-allocation guaranteeing the system properties. Primary Contributions. This work contributes to the literature as follows. (1) To our knowledge, for the first time, we leverage formal methods to propose an efficient, dependable PRBallocation approach in the context of RAN slicing, ensuring system properties (fairness and PRB-optimality) while prioritizing the eMBB Premium service type and catering to best-effort services. To accomplish this, we formally model the PRB-allocation problem as a 3-layered framework, FORSLICE, which guarantees that all system properties remain valid throughout runtime. (2) The proposed framework ensures generality and automated execution; it takes as input any service-partitionslice configuration of a 3-layered hierarchical network structure and automatically generates the PRB-allocation of slices and partitions, that ensures the system properties and preserves the service priority. As a result, FORSLICE exhibits greater robustness than the baseline method ‘Convergence’ [15], which is limited to a particular case study. (3) The SMT-based simulations show that FORSLICE ensures all the system properties, for each network configuration considered as input. Additionally, we present a case study discussion on network performance evaluation, to demonstrate that the throughput offered by the PRB-allocation in FORSLICE matches the throughput observed in actual network simulations, while maintaining the priority to the eMBB Premium service type. (4) Although the baseline ‘Convergence’ [15] addresses fair PRB distribution, the experimental comparisons show that our proposed method reports a 44.45% improvement in system properties as compared to [15].
4
D. Banerjee et al. Organization. The paper is organized as follows. Section 2 discusses the basic background of RAN slicing and
system properties. Section 3 presents a case study discussion to highlight the motivation behind the proposed formal modeling. Section 4 first elaborates on the constraint formulation in FORSLICE for the case study, and then generalizes it for any input configuration. Section 5 presents experimental observations that justify the efficiency of the proposed framework. Section 6 discusses network performance evaluation scenarios. Section 7 lists some related work and their limitations. Finally, Section 8 concludes the entire work and its future directions.
2 RAN Slicing Background We here describe the basic background of RAN slicing, PRB-allocation and system properties. In general, network slicing is a technology that carves up a shared physical network into multiple logical networks, i.e., slices. To achieve RAN slicing, a common technique involves distribution and allocation of radio resources among different slices based on user requirements. A physical resource block (PRB) is the unit of radio resource denoting the specific allocated spectrum block (defined as 12 consecutive subcarriers in the frequency domain). In this work, we follow Ericsson’s PRB-partitioning technique [9] for RAN slicing, that divides the RAN into physical partitions, where a partition is a configured share of radio resources within a cell dedicated to specific user categories. Each partition is further comprised of logical or virtual segments called slices based on the user category. For example, an eMBB Premium slice is dedicated for 4K/8K video streaming applications. The unallocated PRBs, i.e., the remaining PRBs, from the total available amount, which are not allocated to the partitions (i.e., basically its slices), are residual and
Fig. 1. RAN slicing scenario [5QI: 5G quality identifier]
form the residual partition. This residual partition is mainly applicable for the best-effort services like background data transfers, email and messaging, etc., that have no specific QoS requirements like eMBB, FWA and others. Figure 1 depicts an example scenario of PRBpartitioning and RAN slicing; where Partition 1 has
2 slices: eMBB Premium (Pre1) and eMBB Normal (Norm1), and Partition 2 has 2 slices: eMBB Premium (Pre2) and FWA (FWA1), and the rest is the residual partition. On entering the network, a user is assigned to a slice based on its service type (e.g., eMBB Premium, eMBB Normal, etc.). The hierarchical 3-layered network structure for Fig. 2. 3-layered hierarchical network structure for the RAN-slicing this example is illustrated in Figure 2. The first layer scenario portrayed in Figure 1 is comprised of logical units or network slices; the upper layer includes the first layer along with two partitions; and the final or third layer supervises all the components of the RAN system: the first and second layers and the residual partition.
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services5 PRBs are dynamically allocated or de-allocated to or from slices to meet the resource demands of different service types. For example, fair partitioning of PRBs involves allocating additional PRBs to an eMBB Normal slice when the number of users requesting that service is high in the day. Whereas, to optimize PRB usage, it necessitates to de-allocate some PRBs from a FWA slice on having a considerable low demand of FWA service during the late night hours. Thus, in diverse service scenarios with varying QoS requirements, fairness and PRB-optimality are two vital system properties that need to be addressed while allocating PRBs to slices. Below, we define the notions of these properties that we consider in this work. Definition 2.1 (Fairness). Fairness is the guarantee of providing each service type with its desired amount of resources (i.e., PRBs) and throughput at all times, except when the residual partition is overused (i.e., using up 𝑥% of total PRB-share). Definition 2.2 (PRB-optimality). PRB-optimality indicates minimizing unused PRBs in the slices which are not used by the users assigned to the respective slices. The two system properties described above exhibit opposing characteristics — the former typically indicates towards allocating extra PRBs to slices to meet resource demands, whereas the latter suggests for de-allocation of PRBs for judicious usage of resources. The goal of our work is to ensure that the properties are simultaneously satisfied throughout runtime. ‘Minimizing unused PRBs’ necessitates balancing optimality with fairness, indicating that a reduction or de-allocation of PRBs beyond the specified threshold, compromises the constraint of fairness. For a given input configuration of partitions and slices, the proposed formal framework FORSLICE determines a suitable PRB-allocation that preserves the system properties while prioritizing the eMBB Premium service type, thereby maintaining the desired network performance. Next, we consider an example scenario to present the motivation behind the proposed formal modeling. 3 An Illustrative Example Let us consider the example of the RAN-slicing and PRB-partitioning scenario shown in Figure 1. It deals with 3 service types, viz., eMBB Premium, eMBB Normal and FWA; has 2 partitions with two slices each: slices Pre1 and Norm1 in Partition 1, and slices Pre2 and FWA1 in Partition 2. The hierarchical 3-layered network structure for this example is shown in Figure 2. In this work, we present a 3-layered formal framework, FORSLICE, which introduces various layer-specific techniques for efficient PRB-allocation in RAN-slicing scenarios. The rationale for this modeling approach is discussed here with reference to the above case study. On entering the network, a user is assigned to a slice based on its service type. The primary processes executed in the slice layer (i.e., the first layer) after user assignment are as follows. There is an increase in the user count and PRBusage with an increase in the number of users, and consequently, the remaining or residual amount of PRBs in the slice decreases. Users exiting the network trigger the reverse process. At any point of time, i) when there is an over-usage of PRBs and further requirement of extra resources, or ii) when an excess of PRBs remain residual, i.e., unutilized, for a long duration, some appropriate signals get generated in slices to indicate the needs for PRB-allocation and de-allocation, respectively. We name the respective signals as top-up and ramp-down signals in our proposed method. Any monitoring agent (in the upper or second layer) that controls and supervises over a partition and its slices, promptly takes the action for allocating or de-allocating PRBs to/from slices, based on the signals (top-up and rampdown) generated. Since there are two slices (Pre1 and Norm1) in Partition 1, it may happen that at some point of time,
6
D. Banerjee et al.
both the slices require top-up (i.e., requirement of extra PRBs), or ramp-down (i.e., the need to de-allocate unused PRBs), or either of them requires a top-up and the other demands for a ramp-down, and so on. The potential top-up and ramp-down scenarios for slices in Partition 1 are as follows: (𝜙𝑠 , 𝜙𝑠 ), (𝜙𝑠 , TU), (TU, 𝜙𝑠 ), (𝜙𝑠 , RD), (RD, 𝜙𝑠 ), (TU, TU), (RD, RD), (TU, RD) and (RD, TU). Here, the first and second elements of the tuple correspond to signal generation scenarios in slices Pre1 and Norm1 in Partition 1; and 𝜙𝑠 , TU and RD refer to the scenarios when neither top-up nor ramp-down, only top-up, and only ramp-down signal is generated in a slice, respectively. Thus, each slice generates a signal in one of three ways at any given time: no activity (neither top-up nor ramp-down), only top-up, and only ramp-down. Simultaneous top-up and ramp-down in a single slice is not possible. For two slices in Partition 1, this results in a total of 32 = 9 possible combinations of signal generations, to be handled by the monitoring agent of Partition 1. Similar arguments follow for Partition 2 as well. Based on such scenarios, the PRB-allocations or de-allocations have to be decided. For example, if both slices in Partition 1 require top-up, then PRBs need to be allocated to the slices, i.e., to Partition 1. However, in a scenario where Pre1 requests a top-up (say, of 10 PRBs) and Norm1 concurrently requests a ramp-down (to free 15 PRBs, say), an intrapartition adjustment can be made: allocate the 10 PRBs from the Norm1 slice to the Pre1 slice, and then de-allocate the remaining 5 PRBs from Partition 1. The PRB-allocations need to be adjusted accordingly for each of the nine distinct signal generation scenarios observed in Partition 1. Similar arguments also work for Partition 2. On de-allocating PRBs from Partition 1 in the above example, an obvious intuition that occurs is that the de-allocated PRBs must be re-allocated to the residual partition. But the following scenario may also occur — 5 PRBs are de-allocated from Partition 1 and simultaneously Partition 2 demands an allocation of extra 8 PRBs. Hence, a monitoring agent that supervises the entire system needs to decide on how to manage the residual partition’s PRB-share. For example, it can design the following inter-partition adjustment: allocate 5 PRBs from Partition 1 to Partition 2; de-allocate 3 PRBs from the residual partition and allocate those to Partition 2. Since we have two partitions in this example, there are 32 = 9 possible ways for PRB-adjustments: (𝜙𝑝 , 𝜙𝑝 ), (𝜙𝑝 , A), (A, 𝜙𝑝 ), (𝜙𝑝 , D), (D, 𝜙𝑝 ), (A, A), (D, D), (A, D) and (D, A). Here, the first and second elements of the tuple correspond to the allocation requirements in Partitions 1 and 2; and 𝜙𝑝 , A and D refer to the scenarios when a partition requires neither allocation nor de-allocation, only allocation, and only de-allocation, respectively. Only one of these nine scenarios is possible at any given time; the necessary PRB-allocation and residual partition share adjustments must be implemented accordingly . Furthermore, the monitoring agent tasked with system supervision is also responsible for user assignment based on its service type, i.e., user-to-slice mapping. For example, each partition contains a Premium slice: Pre1 and Pre2 in Partitions 1 and 2 respectively. The monitoring agent hence needs to determine to which slice an eMBB Premium type user must be assigned after entering the network. If a random user assignment occurs, then that may lead to clustering of users and over usage of PRBs in one partition, thereby de-allocating excess PRBs from the residual partition. Hence, users must be proportionately assigned to slices — assign a user to a slice within a partition such that it does not trigger excessive PRB-usage and a top-up scenario in the slice soon. Our proposed strategies and user assignment policy address PRB-partitioning by ensuring fairness, PRB-optimality, and balanced use of the residual partition to benefit best-effort services while prioritizing the eMBB Premium service type over the others. The 3-layered formal framework FORSLICE therefore, provides the formal modeling of the aforementioned strategies in the three layers that generates PRB-allocations while ensuring the system properties.
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services7 4 The Design of FORSLICE This work aims to develop a dependable RAN resource (i.e., PRB) allocation strategy that provides differentiated QoS guarantees. The design is engineered to achieve two main goals: i) Ensure fairness in PRB provisioning to all service types based on their specific demands. ii) Minimize unused PRBs to serve the best-effort services accessing the residual-partition. Crucially, the eMBB Premium service type is designated the highest priority. We leverage formal methods in our work to design such a dependable framework for a RAN slicing scenario, that efficiently meets the objectives. As mentioned earlier, FORSLICE is 3-layered hierarchical framework where layers are modeled as follows. Layer 1: The lowest layer that models the slices. Layer 2: The middle layer that models the partitions and their monitoring agents. These monitoring agents administer the partitions and their slices. Layer 3: The topmost layer that models the central monitoring agent, monitoring over the entire system: slices, partitions and monitoring agents, as well as the residual partition. Figure 3 presents the 3-layered framework FORSLICE for the example of 3 service types, 2 partitions and 2 slices per partition, discussed in the previous section.
Central monitoring agent
Layer 3
Residual partition
Here, Layer 1 consists of the four slices — Pre1, Norm1, Pre2 and FWA1. Layer 2 comprises two monitoring agents that monitor over Partitions 1 and 2 respectively,
Layer 2
and also administer the slices in the respective partitions. Finally, the central monitoring agent in Layer 3 man-
Layer 1
Partition 1
Partition 2
Monitoring agent 1
Monitoring agent 2
Pre1
Pre2
Norm1
ages the three layers and all the components, namely the
FWA1
Slices
slices, partitions, the monitoring agents and the residual partition. This indicates that the layer above governs the functions of all underlying layers.
Fig. 3. The proposed 3-layered framework, FORSLICE, for the sample example of 3 service types, 2 partitions and 2 slices per partition
Given any configuration of services (𝒮), partitions (𝒦) and slices (𝒩), FORSLICE formally models these three layers and their properties one after another, starting from the lowest layer (i.e., Layer 1). Figure 4 provides a pictorial representation of the workflow, which we have entirely automated. The (𝒮, 𝒦, 𝒩) configuration of service-partition-slice and the model simulation time range, are the inputs to our model. For example, let us suppose it requires to generate a fair and optimal PRB distribution during the busy hour, 9:00 AM-10:00 AM. Hence, we consider a fixed user distribution of services for the given time range based on the 5G telecommunication network protocols, like a heavy-tailed distribution for the eMBB service. The simulation time range being an input, the simulation begins with an initial state of zero active users. In this work, we leverage SMT as the underlying formal technique for modeling and verification. A set of constraints is formulated during the sequential modeling of Layers 1, 2, and 3, using the provided inputs. The cumulative constraint — the logical conjunction of all the individual constraints obtained in the three layers — is supplied to the SMT solver for verification.
8
D. Banerjee et al. A satisfiable or SAT answer from the solver indicates that FORSLICE is able to generate PRB-allocations for the
partitions and slices satisfying all the design objectives, i.e., ensuring the system properties and maintaining the priority to the eMBB Premium service type. For the ease of presentation and feasibility of the SMT-based modeling, we develop a discretized version of the formal model. Therefore, the entire simulation on a time horizon of length 𝑇̂ is discretized into multiple steps of length
ℎ (say in the range of 1 min), which means any discrete timestep 𝑡 signifies the actual time of ℎ𝑡 units. Thus, we simulate ̂
the model for 𝑇 = ⌈ 𝑇ℎ ⌉ timesteps.
Moreover, for modeling purposes, we make a key assump-
tion: we scale the user count to a unit range in our model assuming transition of at most one user (i.e., one UE can enter or leave a slice) per timestep 𝑡 . This simplification is essential for model abstraction, functioning similarly to how we might scale large data inputs (e.g., aggregating 1000 users into a single data point) to manage complexity. For the sake of clarity and readability, we first delineate the entire formal modeling for the running example of 2 partitions and 2 slices per partition, discussed in Section 3. Later, we generalize the proposed modeling approach, described in Figure 4, for any given (𝒮, 𝒦, 𝒩) configuration of service-partitionslice as input. For our running example, we first elaborate on all the variables and then the linear real arithmetic (LRA) constraints needed for the SMT-based formal modeling of each layer.
4.1
Layer 1: Modeling the Slices
We first present the structure of slices in Layer 1. The variables used for formally modeling any slice sl are listed in Table 1. For simplicity and readability, we mostly refer to any slice as sl in the text and drop the subscript 𝑖 from 𝑠𝑙𝑖,𝑗 . Initially, when the simulation begins (at timestep 𝑗 = 0),
Fig. 4. FORSLICE: Automated design workflow
there is no user entitled to the slice sl, leading to, sl-usr0 = 0, sl-usg0 = 0 and sl-resi0 = sl-shr0 . Maximum possible usage of PRB over a time interval: Given the time-window of slice sl as sl-t-win, different time intervals respecting sl-t-win, that we consider in our modeling, are [((n-1) × sl-t-win) + 1, n × sl-t-win], for 𝑛 ∈ ℕ. Without loss of generality, we assume that only one user can enter the slice at one timestep. Hence, at maximum sl-twin many users can enter the slice during any such interval. Table 1 defines sl-m as the number of users who use up one PRB in slice 𝑠𝑙 . This justifies the following relation,
𝑚𝑎𝑥𝑖𝑚𝑢𝑚 𝑝𝑜𝑠𝑠𝑖𝑏𝑙𝑒 𝑃𝑅𝐵-𝑢𝑠𝑎𝑔𝑒 𝑖𝑛 𝑎𝑛 𝑖𝑛𝑡𝑒𝑟𝑣𝑎𝑙 = ⌈
𝑠𝑙 -𝑡 -𝑤𝑖𝑛 ⌉. 𝑠𝑙 -𝑚
(1)
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services9 The term ‘maximum’ in the above equation reflects the fact that, this usage corresponds to the maximum number of possible users, sl-t-win, in any interval [((n-1) × sl-t-win) + 1, n × sl-t-win]. Next, we define the following terminologies that help in managing the PRB-allocation and de-allocation in slices. Definition 4.1 (Top-Up Signal). A top-up signal is generated in a slice if it requires additional PRBs. Definition 4.2 (Ramp-Down Signal). A ramp-down signal is generated in a slice to decrease the excess unused PRBs. Since no PRB-allocation/de-allocation is allowed during intervals [((𝑛 − 1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛) + 1, 𝑛× 𝑠𝑙 -𝑡 -𝑤𝑖𝑛), for all 𝑛 ∈ ℕ (see definition of sl-t-win𝑖 in Table 1), thus, after every sl-t-win units, i.e., at 𝑗 = 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛, 𝑛 ∈ ℕ, it is checked
whether slice sl requires a top-up or a ramp-down. Initially (at 𝑗 = 0), we set 𝑠𝑙 -𝑠ℎ𝑟0 = ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉, so that there are 𝑚 sufficiently many PRBs till the next window, following Eq. (1). During the formal modeling, we need to design the
constraints for top-up and ramp-down signals in such a way, that a slice sl does not require any PRBs during the interval [((𝑛 − 1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛) + 1, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛), for 𝑛 ∈ ℕ. A larger time interval, [((𝑛 −1)×𝑠𝑙 -𝑡 -𝑤𝑖𝑛)+1, 𝑛 ×𝑠𝑙 -𝑡 -𝑤𝑖𝑛] of length 𝑠𝑙 -𝑡 -𝑤𝑖𝑛 indicates a higher value of the maximum
⌉. possible PRB-usage in that interval, which is ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 𝑚
Inference 1: A larger time-window is desirable for the slices corresponding to service types with a higher user-count
and PRB-usage. Inference 2: Conversely, a smaller time-window is preferable for the slices corresponding to the services with considerably fewer users. This leaves an option to frequently check whether the PRBs in the respective slices remain unused and if so, a ramp-down signal is generated soon to ensure PRB-optimality. The PRB-consumption, sl-m, is chosen based on the resource demands of the service type of the slice sl. The eMBB Premium users have the highest priority, followed by eMBB Normal users, and then FWA users, in our running example. This prioritization ensures that eMBB Premium users consistently receive the required quality of service. Inference 3: We consider a smaller PRB-consumption value for any slice corresponding to a higher priority service type, e,g., smaller PRB-consumption for eMBB Premium type indicates that the PRB-consumption by a single eMBB Premium user is higher as compared to other services. Symbols
Meanings
𝑇 𝑠𝑙 -𝑒𝑛𝑖,𝑗 𝑠𝑙 -𝑙𝑣𝑖,𝑗 𝑠𝑙 -𝑢𝑠𝑟𝑖,𝑗 𝑠𝑙 -𝑠ℎ𝑟𝑖,𝑗 𝑠𝑙 -𝑢𝑠𝑔𝑖,𝑗 𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗
total timesteps derived from the simulation time horizon
𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖
user entry flag (Boolean variable) for 𝑖-th slice at 𝑗 -th timestep user exit flag (Boolean variable) for 𝑖-th slice at 𝑗 -th timestep number of users in 𝑖-th slice at 𝑗 -th timestep number of PRBs allocated to 𝑖-th slice at 𝑗 -th timestep number of PRBs utilized by 𝑖-th slice at 𝑗 -th timestep number of residual PRBs (allocated but unused) in 𝑖-th slice at 𝑗 -th timestep time window of 𝑖-th slice i.e., no PRBs allocated or de-allocated to/from 𝑖-th slice during interval [((𝑛 − 1)× 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ) + 1, 𝑛× 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ), ∀𝑛 ∈ ℕ
𝑠𝑙 -𝑚𝑖 𝑠𝑙 -𝐸𝑖,𝑗
PRB-consumption of 𝑖-th slice: 𝑠𝑙 -𝑚𝑖 users use up one PRB
𝑠𝑙 -𝑡𝑜𝑝𝑖,𝑗 𝑠𝑙 -𝑟𝑎𝑚𝑝𝑖,𝑗 𝑟𝑝 -𝑜𝑣𝑟𝑗
top-up-signal flag (Boolean variable) in 𝑖-th slice at 𝑗 -th timestep
number of users entered since the last time-window, in 𝑖-th slice at 𝑗 -th timestep ramp-down-signal flag (Boolean variable) in 𝑖-th slice at 𝑗 -th timestep residual partition-overuse flag (Boolean variable) at 𝑗 -th timestep Table 1. Variables associated with Layer 1
10
D. Banerjee et al. Let us consider an example. Usually there are more eMBB Normal type customers in comparison to the Premium
type customers in the network, hence, we select the time-windows of the slices as, 𝑠𝑙 -𝑡 -𝑤𝑖𝑛 > 𝑠𝑙 ′ -𝑡 -𝑤𝑖𝑛, where 𝑠𝑙 and 𝑠𝑙 ′ are any slices corresponding to the eMBB Premium and eMBB Normal service types respectively. Let 𝑠𝑙 -𝑚 = ′
2, 𝑠𝑙 -𝑡 -𝑤𝑖𝑛 = 28 and 𝑠𝑙 ′ -𝑚 = 3, 𝑠𝑙 ′ -𝑡 -𝑤𝑖𝑛 = 40. Therefore, we obtain, ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉ = 14 and ⌈ 𝑠𝑙 𝑠𝑙-′𝑡 --𝑤𝑖𝑛 ⌉ = 14. Thus, the same 𝑚 𝑚 number of PRBs, i.e., 14 PRBs, are allocated to a Premium and to a Normal slice, but for intervals of lengths 28 units and 40 units respectively. This clearly infers that a larger number of PRBs are allocated to the Premium type customers over a smaller time interval, thereby, prioritizing them over other service types. Relationship between the throughput and PRB-usage: The key performance indicator (KPI) that we consider in this work is throughput. We desire to maintain a particular range of throughput for a particular service type (part of fairness, ref. Definition 2.1). We follow the equation given in [3] to calculate the maximum throughput, which is, 𝐽
𝐵𝑊 (𝑗),𝜇
(𝑗)
𝑇ℎ = 10−6 ∑ (𝑣 (𝑗) 𝑄𝑚 𝑓 (𝑗) 𝑅𝑚𝑎𝑥 𝑗=1
𝑁𝑃𝑅𝐵
𝜇 𝑇𝑠
× 12
(1 − 𝑂𝐻 (𝑗) ) ) .
Here, 𝐽 is the PRB-usage, 𝑣 (𝑗) is the maximum number of supported MIMO layers (separate data stream enabled by (𝑗)
using multiple antennas at the base station), 𝑄𝑚 is the maximum supported modulation order (the number of distinct symbols a digital communication system uses to encode data), 𝑓 (𝑗) is the scaling factor, 𝜇 is numerology (the flexible 𝜇
scaling of orthogonal frequency-division multiplexing (OFDM) waveform parameters), 𝑇𝑠 is the average OFDM symbol 𝐵𝑊 (𝑗),𝜇
duration in a subframe for numerology 𝜇 , 𝑁𝑃𝑅𝐵
numerology 𝜇 , 𝑂𝐻 𝑗 is the overhead and 𝑅
is the maximum resource block allocation in bandwidth 𝐵𝑊 with
𝑚𝑎𝑥 is a scalar.
(𝑗)
The Ericsson-specific choice for the values of these parameters are as follows: 𝑣 (𝑗) = 8, 𝑄𝑚 = 64, 𝑓 (𝑗) = 1, 𝑅𝑚𝑎𝑥 = −3 𝐵𝑊 (𝑗),𝜇 𝜇 80×𝑇ℎ 948 , 𝜇 = 1, 𝑁 = 38, 𝑇𝑠 = 10 𝜇 and 𝑂𝐻 (𝑗) = 0.14. We set the value of throughput as 𝑇ℎ̂ = (since 𝑇ℎ is
1024
𝑃𝑅𝐵
14×2
the maximum), hence, we obtain the following equation,
100
𝑇ℎ̂ = 4163.798 × 𝐽 .
(2)
This proves that the throughput and PRB-usage are constant multiples of each other. Definitions 4.1 and 4.2 indicate that the top-up or ramp-down signals occur based on the PRB-usage in a slice at that timestep. Using Eq. (2), we can also interpret this as following — upon the arrival of new users within a slice, additional PRB provisioning is necessary to achieve target throughput levels. Inference 4: It is equivalent to consider any one of the two parameters, PRB-usage or throughput, to formalize the conditions for top-up/ramp-down signals. Therefore, if the PRB-allocation in FORSLICE ensures the underlying system properties, it analogously validates the network performance efficacy by maintaining the intended throughput range. Next, we present the constraint formulation of Layer 1 for our running example. In this work, we assume that the residual partition should have at least 50% of the total PRBs; if that is violated, then it is a residual partition-overuse scenario. The 50% limit particularly guarantees adequate resource availability to the best-effort services. 4.2
Constraints For Layer 1
We now formally write down all the constraints pertaining to Layer 1. A slice and a timestep are indexed with 𝑖 and 𝑗 respectively, in all the constraints written below. (1) Total user-count update for a particular timestep: We use two Boolean variables, 𝑠𝑙 -𝑒𝑛𝑖,𝑗 and 𝑠𝑙 -𝑙𝑣𝑖,𝑗 , to design this constraint. The variables are defined as follows.
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 11 i) 𝑠𝑙 -𝑒𝑛𝑖,𝑗 is set to True (𝕋) if a user enters 𝑖-th slice at 𝑗 -th timestep, and is False (𝔽) otherwise. ii) 𝑠𝑙 -𝑙𝑣𝑖,𝑗 is set to True (𝕋) if a user leaves 𝑖-th slice at 𝑗 -th timestep, and is False (𝔽) otherwise. The user leaves a slice under two scenarios: a) leaving the network, and b) switching the service types (e.g., a Premium user shifts to the Normal type when its dedicated plan is exhausted). The user-count update constraint for our running example of four slices is as follows. 4 𝑇 𝐿1,1 : ∧𝑖=1 ∧𝑗=1
[ ( sl-en𝑖,𝑗 = 𝕋 ∧ sl-lv𝑖,𝑗 = 𝔽 ⇒ sl-usr𝑖,𝑗 = sl-usr𝑖,𝑗 -1 + 1 ) ∧ ( sl-en𝑖,𝑗 = 𝔽 ∧ sl-lv𝑖,𝑗 = 𝕋 ⇒ sl-usr𝑖,𝑗 = sl-usr𝑖,𝑗 -1 − 1 ) ∧ ( sl-en𝑖,𝑗 = 𝕋 ∧ sl-lv𝑖,𝑗 = 𝕋 ⇒ sl-usr𝑖,𝑗 = sl-usr𝑖,𝑗 -1 ) ∧ ( sl-en𝑖,𝑗 = 𝔽 ∧ sl-lv𝑖,𝑗 = 𝔽 ⇒ sl-usr𝑖,𝑗 = sl-usr𝑖,𝑗 -1 ) ] At any 𝑗 -th timestep, at most one user can enter into and can leave from a slice. Hence, the user-count is updated at the 𝑗 -th timestep in the following two cases: I. it is incremented when a user enters but no user leaves (𝑠𝑙 -𝑒𝑛𝑖,𝑗 = 𝕋 ∧ 𝑠𝑙 -𝑙𝑣𝑖,𝑗 = 𝔽 ) and II. it is decremented when a user leaves and no user enters (𝑠𝑙 -𝑒𝑛𝑖,𝑗 = 𝔽 ∧ 𝑠𝑙 -𝑙𝑣𝑖,𝑗 = 𝕋 ). The user-count remains the same as that in the previous timestep for the other two cases: III. when one user enters and another leaves (𝑠𝑙 -𝑒𝑛𝑖,𝑗 = 𝕋 ∧ 𝑠𝑙 -𝑙𝑣𝑖,𝑗 = 𝕋 ) and IV. when users neither enter nor leave (𝑠𝑙 -𝑒𝑛𝑖,𝑗 = 𝔽 ∧ 𝑠𝑙 -𝑙𝑣𝑖,𝑗 = 𝔽 ). (2) User-count update for a particular time interval: The number of users who have entered the 𝑖-th slice till timestep 𝑗 , starting from timestep, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 (𝑛 ∈ ℕ), is denoted by 𝑠𝑙 -𝐸𝑖,𝑗 . The integer variable sl-E counts the number of users entering the slice 𝑠𝑙 during any time interval [((n-1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ) + 1, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ], for 𝑛 ∈ ℕ. For each 𝑛 ∈ ℕ, at timestep 𝑗 = (𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ) + 1, i.e., when 𝑗 ≡ 1 mod (𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ), 𝑠𝑙 -𝐸𝑖,𝑗 is set to 1 if any user enters the 𝑖-th slice, or else it is set to 0. This is because, the variable 𝑠𝑙 -𝐸𝑖,𝑗 is only specific to the time interval, [((n-1)
× 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ) + 1, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ], for each 𝑛 ∈ ℕ. At all other timesteps, 𝑠𝑙 -𝐸𝑖,𝑗 is incremented only if a user enters. This constraint is formulated as follows. 4 𝑇 𝐿1,2 : ∧𝑖=1 ∧𝑗=1 [ ( j ≡ 1 mod (sl-t-win𝑖 ) ⇒ ( sl-en𝑖,𝑗 = 𝕋 ⇒ sl-E𝑖,𝑗 = 1 ) ∧ ( sl-en𝑖,𝑗 = 𝔽 ⇒ sl-E𝑖,𝑗 = 0 ) )
∧ ( j ≢ 1 mod (sl-t-win𝑖 ) ⇒ ( sl-en𝑖,𝑗 = 𝕋 ⇒ sl-E𝑖,𝑗 = sl-E𝑖,𝑗 -1 + 1 ) ∧ ( sl-en𝑖,𝑗 = 𝔽 ⇒ sl-E𝑖,𝑗 = sl-E𝑖,𝑗 -1 ) ) ]
This variable helps to design the constraint for ramp-down signal generation (𝐿1,5 in Section 4.2). (3) PRB-usage and residual PRB-count update: We consider that one PRB is used up by 𝑠𝑙 -𝑚𝑖 users (ref. Table 1). Precisely, at the 𝑗 -th timestep, when a user enters (i.e., 𝑠𝑙 -𝑒𝑛𝑖,𝑗 = 𝕋) and no user leaves (i.e., 𝑠𝑙 -𝑙𝑣𝑖,𝑗 = 𝔽) and 𝑠𝑙 -𝑢𝑠𝑟𝑖,𝑗 ≡ 1 mod (𝑠𝑙 -𝑚𝑖 ), then the PRB-usage (𝑠𝑙 -𝑢𝑠𝑔𝑖,𝑗 ) is incremented by 1 and residual PRB count (𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 ) is decremented by
1. For example, let 𝑠𝑙 -𝑚𝑖 = 3. Thus, when the 1-st, 4-th, 7-th and so on, users enter the slice (i.e., 𝑠𝑙 -𝑢𝑠𝑟𝑖,𝑗 ≡ 1 mod 3), 𝑠𝑙 -𝑢𝑠𝑔𝑖,𝑗 is incremented by 1 and 𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 drops by 1. Similarly, if a user leaves (i.e., 𝑠𝑙 -𝑙𝑣𝑖,𝑗 = 𝕋) and no user enters (i.e., 𝑠𝑙 -𝑒𝑛𝑖,𝑗 = 𝔽) and 𝑠𝑙 -𝑢𝑠𝑟𝑖,𝑗 ≡ 0 mod (𝑠𝑙 -𝑚𝑖 ), then 𝑠𝑙 -𝑢𝑠𝑔𝑖,𝑗 is decremented by 1 and 𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 is incremented by 1. For example, there are four users in the 𝑖-th slice at timestep 𝑗 = 5, and suppose at 𝑗 = 6, one user leaves. Thus, the second PRB allocated to the 4-th user is made free and one PRB is sufficient for the first three users, as 𝑠𝑙 -𝑚𝑖 = 3. Hence, when users leave and the user-count drops to 3, 6, 9 and so on, one PRB is freed, hence, 𝑠𝑙 -𝑢𝑠𝑔𝑖,𝑗 is decremented and 𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 is incremented by 1. The constraint written below describes these two cases. For the other cases, both the variables, 𝑠𝑙 -𝑢𝑠𝑔𝑖,𝑗 and 𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 remain the same as that in the previous timestep.
12
D. Banerjee et al. 4 𝑇 𝐿1,3 : ∧𝑖=1 ∧𝑗=1
[ [ ( sl-en𝑖,𝑗 = 𝕋 ∧ sl-lv𝑖,𝑗 = 𝔽 ∧ sl-usr𝑖,𝑗 ≡ 1 mod (sl-m𝑖 ) ) ⇒ ( sl-usg𝑖,𝑗 = sl-usg𝑖,𝑗 -1 + 1 ∧ sl-resi𝑖,𝑗 = sl-resi𝑖,𝑗 -1 − 1 ) ] ∧ [ ( sl-en𝑖,𝑗 = 𝔽 ∧ sl-lv𝑖,𝑗 = 𝕋 ∧ sl-usr𝑖,𝑗 ≡ 0 mod (sl-m𝑖 ) ) ⇒ ( sl-usg𝑖,𝑗 = sl-usg𝑖,𝑗 -1 − 1 ∧ sl-resi𝑖,𝑗 = sl-resi𝑖,𝑗 -1 + 1 ) ] ] (4) Top-up signal generation: The requirement for top-up in the 𝑖-th slice is checked after every 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 time units, beginning at the timestep 𝑗 = 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 . If in any interval [((n-1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ) + 1, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ), 𝑛 ∈ ℕ, there has been a considerable amount of PRB-usage and there is not enough PRBs till the next window, then a top-up signal is generated at 𝑗 = 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 . This is checked by the condition: whether the residual number of PRBs (𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 ) in the slice is less than or equal to 𝑠𝑙 -𝑡 -𝑤𝑖𝑛
the maximum usage (⌈ 𝑠𝑙 -𝑚 𝑖 ⌉) in the next interval. If the condition is true, then a top-up signal is generated. 𝑖
Moreover, the residual partition should not be overused (ref. Section 4.1) before generating a top-up signal, otherwise
allocation of additional PRBs is not possible. We use a Boolean variable 𝑟𝑝 -𝑜𝑣𝑟𝑗 to indicate a residual partition-overuse scenario (using up 50% of total PRBs). At the 𝑗 -th timestep, 𝑟𝑝 -𝑜𝑣𝑟𝑗 is True if the residual partition has less than 50% of the total PRBs, else it is False. The constraint below highlights the case when the top-up signal, 𝑠𝑙 -𝑡𝑜𝑝𝑖,𝑗 , is True, and in all other cases, it is False.
𝐿1,4 : ∧4𝑖=1 ∧𝑇𝑗=1 [ ( rp-ovr𝑗 = 𝔽 ∧ j ≡ 0 mod (sl-t-win𝑖 ) ∧ sl-resi𝑖,𝑗 ≤ ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ ) ⇒ sl-top𝑖,𝑗 = 𝕋 ] 𝑠𝑙 -𝑡 -𝑤𝑖𝑛 𝑖
(5) Ramp-down signal generation: Similar to top-up, the condition for ramp-down in the 𝑖-th slice is checked at every 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 time units. The condition to be checked is — if at some timestep, 𝑗 = 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 , the number of residual 𝑠𝑙 -𝑡 -𝑤𝑖𝑛
PRBs is quite large in amount, even after considering that the maximum usage amount (⌈ 𝑠𝑙 -𝑚 𝑖 ⌉) is available till the 𝑖
next time-window, 𝑗 = (𝑛 + 1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 , then a ramp-down signal (𝑠𝑙 -𝑟𝑎𝑚𝑝𝑖,𝑗 ) is generated at 𝑗 = 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 . At the 𝑗 -th timestep, this ‘quite large’ is quantified by two conditions:
i) the residual number of PRBs (𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 ) is larger than twice the maximum usage in a time-interval, i.e., there are 𝑠𝑙 -𝑡 -𝑤𝑖𝑛
𝑠𝑙 -𝑡 -𝑤𝑖𝑛
𝑖
𝑖
more than ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ amount of PRBs, even after subtracting ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ from 𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 (i.e., the residual PRBs can be utilized for the next two time intervals and even more),
ii) no users have entered the 𝑖-th slice during the interval [((n-1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ) + 1, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 ], 𝑛 ∈ ℕ, checked by the constraint, 𝑠𝑙 -𝐸𝑖,𝑗 = 0. If these two conditions are true, this clearly indicates a requirement to reduce the unused PRBs through a ramp-down. The following constraint captures this idea. 𝐿1,5 : ∧4𝑖=1 ∧𝑇𝑗=1 [ ( j ≡ 0 mod (sl-t-win𝑖 ) ∧ sl-resi𝑖,𝑗 − ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ ≥ ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ ∧ sl-E𝑖,𝑗 = 0 ) ⇒ sl-ramp𝑖,𝑗 = 𝕋 ] 𝑠𝑙 -𝑡 -𝑤𝑖𝑛
𝑠𝑙 -𝑡 -𝑤𝑖𝑛
𝑖
𝑖
(6) Conflict removal: The constraint below describes that both top-up and ramp-down signals cannot be generated at the same timestep, in the 𝑖-th slice, 1 ≤ 𝑖 ≤ 4. 𝐿1,6 : ∧4𝑖=1 ∧𝑇𝑗=1 [sl-top𝑖,𝑗 = 𝕋 ⇒ sl-ramp𝑖,𝑗 = 𝔽 ∧ sl-ramp𝑖,𝑗 = 𝕋 ⇒ sl-top𝑖,𝑗 = 𝔽 ]
4.3
Layer 2: Modeling the Partitions
Next, we proceed to formally model the partitions in Layer 2. This layer consists of the monitoring agents. A monitoring agent monitors over a partition 𝑃 and all its slices (i.e., the set 𝑆𝑃 ), by updating the PRB-shares of both 𝑃 and 𝑆𝑃 . The PRB-share of partition 𝑃 is the total number of PRBs allocated to the slices in 𝑆𝑃 . A slice may generate a top-up or ramp-down signal at any of the timesteps, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛, 𝑛 ∈ ℕ. Since, in our running example, each of the two partitions
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 13 has two slices, there may be a scenario that both the slices of the same partition generate top-up-signals together, or, one slice requires top-up and the other opts for ramp-down (see the discussion in Section 3). A partition’s monitoring agent adjusts the PRB-shares accordingly for all such cases. We next define some terminologies. Definition 4.3 (Top-Up-Slice). A top-up-slice is an action that allocates extra PRBs to a slice and increases its PRB-share, when the slice has generated a top-up signal. Definition 4.4 (Ramp-Down-Slice). A ramp-down-slice is an action that de-allocates excess unused PRBs from a slice and decreases its PRB-share, when the slice has generated a ramp-down signal. Definition 4.5 (Top-Up-Partition). A top-up-partition is an action which increases the PRB-share of a partition because a top-up-slice action is executed in at least one of its slices. Definition 4.6 (Ramp-Down-Partition). A ramp-down-partition is an action which decreases the PRB-share of a partition because a ramp-down-slice action is executed in at least one of its slices. 4.4 Constraints For Layer 2 For the constraint formulation, we use indices 𝑘 = 1 and 2 to represent the two partitions in our running example. The two slices in Partition 1 are, 𝑠𝑙1 (Pre1) and 𝑠𝑙2 (Norm1) and the two slices in Partition 2 are, 𝑠𝑙3 (Pre2) and 𝑠𝑙4 (FWA1). Most of the variables in Layer 1 (ref. Table 1) are used once again in Layer 2 (since the monitoring agents in Layer 2 also monitor over slices). The new variables introduced in Layer 2 are listed in Table 2. Symbols
Meaning
𝑝𝑡 -𝑠ℎ𝑟𝑘,𝑗
the PRB-share of 𝑘 -th partition at 𝑗 -th timestep
𝜋𝑘 𝑊̂ 𝑖
slice indices in 𝑘 -th partition, e.g., 𝜋1 = {1, 2}, 𝜋2 = {3, 4}, for our example 𝑠𝑙 -𝑡 -𝑤𝑖𝑛
the maximum usage amount ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ for 𝑖-th slice 𝑖
Table 2. New variables associated with Layer 2
In case of top-up-slice or ramp-down-slice actions, the amount of PRBs added or deducted to/from a slice 𝑠𝑙 , equals
⌉, in any interval [((𝑛-1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛) + 1, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛] (ref. Eq. (1) in Section 4.1). the maximum usage amount, ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 𝑚
After a top-up-slice action, this ensures that the PRB-share of slice 𝑠𝑙 is sufficient till the next time-window, thereby, guaranteeing fairness. Likewise, for the ramp-down-slice action, de-allocating ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉ many PRBs ensures fairness, 𝑚 as well as PRB-optimality.
The rationale behind this is explained as follows. The ramp-down signal generation constraint (𝐿1,5 ) in Layer 1 mentions that a ramp-down signal is generated in 𝑠𝑙 at timestep 𝑗 = 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛, when no users have entered the slice 𝑠𝑙 during the interval [((𝑛-1) × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛) + 1, 𝑛 × 𝑠𝑙 -𝑡 -𝑤𝑖𝑛], and also the unused PRBs (sl-resi) in 𝑠𝑙 are in excess (equal or more than 2 × ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉), i.e., there are sufficiently many PRBs to get through the next two time-windows. If 𝑚 𝑠𝑙 -𝑡 -𝑤𝑖𝑛
𝑠𝑙 -𝑡 -𝑤𝑖𝑛
𝑖
𝑖
sl-resi𝑖,𝑗 = 2 × ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ for the 𝑖-th slice at the 𝑗 -th timestep, then de-allocating more than ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ many PRBs from
the slice after a ramp-down-slice action may jeopardize the constraint of fairness; since the remaining PRBs would not 𝑠𝑙 -𝑡 -𝑤𝑖𝑛
be sufficient to cope up with the user requirements till the next time window. Therefore, we de-allocate ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉ many PRBs after a ramp-down-slice action to ensure fairness and PRB-optimality simultaneously.
𝑖
Inference 5: Allocating and de-allocating ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉ many PRBs after a top-up-slice and ramp-down-slice action 𝑚
respectively, ensure that there are sufficiently many PRBs till the next window (fairness) and also minimizes the unused PRBs (PRB-optimality).
14
D. Banerjee et al.
In all the constraints written below, we use 𝑖, 𝑖′ ∈ 𝜋𝑘 (ref. Table 2) to denote the two slices in the 𝑘 -th partition and 𝑠𝑙 -𝑡 -𝑤𝑖𝑛𝑖 𝑗 is used to denote the timestep. Also, the quantity ⌈ ⌉ (ref. Eq. (1)) is referred to as 𝑊̂ 𝑖 for the 𝑖-th slice in all the 𝑠𝑙 -𝑚𝑖
constraints, for simplicity. We now elaborate and formulate the constraint for all nine cases discussed in Section 3. (1) Neither top-up-slice nor ramp-down-slice action: None of the slices in each of the two partitions require topup-slice or ramp-down-slice action, maintaining the same partition shares as in previous timesteps. The constraint for this (case (𝜙𝑠 , 𝜙𝑠 ) in Section 3) is as follows.
𝐿2,1 : ∧2𝑘=1 ∧𝑇𝑗=1 [∧𝑖∈𝜋𝑘 (sl-top𝑖,𝑗 = 𝔽 ∧ sl-ramp𝑖,𝑗 = 𝔽) ⇒ pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 ]
(2) Top-up-slice action for any one slice: Only one of the two slices requires top-up and the other opts for no changes (i.e., cases (𝜙𝑠 , TU) and (TU, 𝜙𝑠 ) in Section 3). Hence, it gives rise to a top-up-partition action. For example, in Partition 1, slice 𝑠𝑙1 generates a top-up signal but slice 𝑠𝑙2 doesn’t generate any top-up or ramp-down signal at the 𝑗 -th timestep, which is formally written as, 𝑠𝑙 -𝑡𝑜𝑝1,𝑗 = 𝕋 ∧ 𝑠𝑙 -𝑡𝑜𝑝2,𝑗 = 𝔽 ∧ 𝑠𝑙 -𝑟𝑎𝑚𝑝2,𝑗 = 𝔽. Hence, there will be a top-up-slice action that increases the PRB-share, 𝑠𝑙 -𝑠ℎ𝑟1,𝑗 , and the residual PRB count, 𝑠𝑙 -𝑟𝑒𝑠𝑖1,𝑗 , of 𝑠𝑙1 . As the total PRB-share of 𝑠𝑙1 is increased and currently the blocks are unused, hence the residual PRB count is also increased. The top-up-slice action in 𝑠𝑙1 leads to a top-up-partition action in Partition 1 (increasing the partition’s PRB-share 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 ). The PRB-share of Partition 2, i.e., 𝑠𝑙 -𝑠ℎ𝑟2,𝑗 , and the residual PRB count, i.e., 𝑠𝑙 -𝑟𝑒𝑠𝑖2,𝑗 , of slice 𝑠𝑙2 , remain the same as that in the (𝑗 -1)-th timestep. The constraint is written as follows. 𝐿2,2 : ∧2𝑘=1 ∧𝑇𝑗=1 ∧𝑖,𝑖′ ∈𝜋𝑘 , 𝑖≠𝑖′
[ (sl-top𝑖,𝑗 = 𝕋 ∧ sl-top𝑖′ ,𝑗 = 𝔽 ∧ sl-ramp𝑖′ ,𝑗 = 𝔽) ⇒ ( sl-shr𝑖,𝑗 = sl-shr𝑖,𝑗 -1 + 𝑊̂ 𝑖 ∧ sl-resi𝑖,𝑗 = sl-resi𝑖,𝑗 -1 + 𝑊̂ 𝑖 ∧ sl-shr𝑖′ ,𝑗 = sl-shr𝑖′ ,𝑗 -1 ∧ sl-resi𝑖′ ,𝑗 = sl-resi𝑖′ ,𝑗 -1 ∧ pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 + 𝑊̂ 𝑖 ) ]
(3) Ramp-down-slice action for any one slice: Only one of the two slices generates a ramp-down signal and the other opts for no changes (i.e., cases (𝜙𝑠 , RD) and (RD, 𝜙𝑠 ) in Section 3), resulting in a ramp-down-partition action. The constraint formulation in this case is similar to that of the previous case. Here, PRB-shares of a partition and its corresponding slice are decreased. 𝐿2,3 : ∧2𝑘=1 ∧𝑇𝑗=1 ∧𝑖,𝑖′ ∈𝜋𝑘 ,𝑖≠𝑖′
[ (sl-ramp𝑖,𝑗 = 𝕋 ∧ sl-top𝑖′ ,𝑗 = 𝔽 ∧ sl-ramp𝑖′ ,𝑗 = 𝔽) ⇒ ( sl-shr𝑖,𝑗 = sl-shr𝑖,𝑗 -1 − 𝑊̂ 𝑖 ∧ sl-resi𝑖,𝑗 = sl-resi𝑖,𝑗 -1 − 𝑊̂ 𝑖 ∧ sl-shr𝑖′ ,𝑗 = sl-shr𝑖′ ,𝑗 -1 ∧ sl-resi𝑖′ ,𝑗 = sl-resi𝑖′ ,𝑗 -1 ∧ pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 − 𝑊̂ 𝑖 ) ]
(4) Top-up-slice action for both the slices: Both the slices of a partition generate top-up signals simultaneously (i.e., case (TU, TU) in Section 3), and thus initiate a top-up-partition action. For example, slices 𝑠𝑙1 and 𝑠𝑙2 of Partition 1 (note that 𝜋1 = {1, 2}) require top-up at the 𝑗 -th timestep concurrently, which is denoted as, 𝑠𝑙 -𝑡𝑜𝑝1,𝑗 = 𝕋 ∧ 𝑠𝑙 -𝑡𝑜𝑝2,𝑗 = 𝕋. The top-up slice action increases the PRB-share (𝑠𝑙 -𝑠ℎ𝑟𝑖,𝑗 ) as well as the residual PRB count (𝑠𝑙 -𝑟𝑒𝑠𝑖𝑖,𝑗 ) of the 𝑖-th slice, by an amount of 𝑊̂ 𝑖 (for all 𝑖 ∈ 𝜋𝑘 ). Moreover, the top-up-partition action increases the PRB-share of Partition 1 (𝑝𝑡 -𝑠ℎ𝑟1,𝑗 ) 𝑠𝑙 -𝑡 -𝑤𝑖𝑛 𝑠𝑙 -𝑡 -𝑤𝑖𝑛 by the amount, ⌈ 𝑠𝑙 -𝑚 1 ⌉ + ⌈ 𝑠𝑙 -𝑚 2 ⌉ = 𝑊̂ 1 + 𝑊̂ 2 . We write the constraint below. 1
2
𝐿2,4 : ∧2𝑘=1 ∧𝑇𝑗=1 ∧𝑖,𝑖′ ∈𝜋𝑘 , 𝑖<𝑖′ [ ( sl-top𝑖,𝑗 = 𝕋 ∧ sl-top𝑖′ ,𝑗 = 𝕋 ) ⇒ ( ∧𝑖∈𝜋 ( sl-shr𝑖,𝑗 = sl-shr𝑖,𝑗 -1 + 𝑊̂ 𝑖 ∧ sl-resi𝑖,𝑗 = sl-resi𝑖,𝑗 -1 + 𝑊̂ 𝑖 ) ∧ ( pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 + ∑𝑖∈𝜋 𝑊̂ 𝑖 ) ) ] 𝑘
𝑘
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 15 (5) Ramp-down-slice action for both the slices: Both the slices generate ramp-down signals simultaneously (i.e., case (RD, RD) in Section 3) and thus, ramp-down-slice and ramp-down-partition actions occur. The constraint formulation is similar to the previous case.
𝐿2,5 : ∧2𝑘=1 ∧𝑇𝑗=1 ∧𝑖,𝑖′ ∈𝜋𝑘 , 𝑖<𝑖′ [ ( sl-ramp𝑖,𝑗 = 𝕋 ∧ sl-ramp𝑖′ ,𝑗 = 𝕋 ) ⇒ ( ∧𝑖∈𝜋 ( sl-shr𝑖,𝑗 = sl-shr𝑖,𝑗 -1 − 𝑊̂ 𝑖 ∧ sl-resi𝑖,𝑗 = sl-resi𝑖,𝑗 -1 − 𝑊̂ 𝑖 ) ∧ ( pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 − ∑𝑖∈𝜋 𝑊̂ 𝑖 ) ) ] 𝑘
𝑘
(6) Top-up-slice action in one slice and ramp-down-slice action in another: Here, two slices of the same partition have conflicting requirements (i.e., cases (TU, RD) and (RD, TU) in Section 3). For example, in Partition 1, slice 𝑠𝑙1 generates a top-up signal and 𝑠𝑙2 generates a ramp-down signal or vice-versa. Let us consider the first case, similar arguments follow in the other case too. There can be three sub-cases in each such case, one giving rise to a top-up-partition action, another to a ramp-down-partition action and the last one demanding neither of the two. Sub-case 1: If the requirement of PRBs for the slice opting for top-up (slice 𝑠𝑙1 in this example, say), is larger in comparison to the amount of PRBs to be de-allocated from the slice requiring ramp-down (slice 𝑠𝑙2 ), i.e., 𝑊̂ 1 > 𝑊̂ 2 ,
then the net result is a top-up-partition. This is because slice 𝑠𝑙1 demanding a top-up first borrows 𝑊̂ 2 many PRBs from slice 𝑠𝑙2 that has generated a ramp-down signal. Since the borrowed amount is not sufficient (as 𝑊̂ 1 > 𝑊̂ 2 ), some extra PRBs (i.e., amount, 𝑊̂ 1 − 𝑊̂ 2 ) are allocated to the partition, resulting in a top-up-partition action.
Sub-case 2: Similarly, if the slice opting for ramp-down (slice 𝑠𝑙2 ), has a greater quantity of PRBs to be reduced compared to the slice requiring top-up (slice 𝑠𝑙1 ), i.e., 𝑊̂ 2 > 𝑊̂ 1 , then the net result is a ramp-down partition. First, the
slice asking for ramp-down (𝑠𝑙2 ) donates 𝑊̂ 2 PRBs to the slice that has demanded for a top-up (𝑠𝑙1 ). The extra PRBs (i.e., amount 𝑊̂ 2 − 𝑊̂ 1 ) that could not be donated, are de-allocated from the partition, causing its ramp-down. Sub-case 3: If the number of PRBs to be allocated to one slice is equal to the number to be de-allocated from another slice, i.e., 𝑊̂ 1 = 𝑊̂ 2 , then with intra-partition adjustments within the slices, there is no need to proceed for a top-up-partition or a ramp-down-partition action. In all three cases, the PRB-shares (sl-shr𝑖,𝑗 ) and residual PRB counts (sl-resi𝑖,𝑗 ) of the respective slices are updated
(i.e., increased for top-up and decreased for ramp-down). The constraint is given as follows. 𝐿2,6 : ∧2𝑘=1 ∧𝑇𝑗=1 ∧𝑖,𝑖′ ∈𝜋𝑘 , 𝑖≠𝑖′
[ ( sl-top𝑖,𝑗 = 𝕋 ∧ sl-ramp𝑖 ,𝑗 = 𝕋 ) ⇒ [ { ( 𝑊̂ 𝑖 > 𝑊̂ 𝑖 ⇒ pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗-1 + ( 𝑊̂ 𝑖 − 𝑊̂ 𝑖 ) ) ′
′
′
∨ ( 𝑊̂ 𝑖 < 𝑊̂ 𝑖′ ⇒ pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 − ( 𝑊̂ 𝑖′ − 𝑊̂ 𝑖 ) ) ∨ ( 𝑊̂ 𝑖 = 𝑊̂ 𝑖′ ⇒ pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 ) } ∧ ( sl-shr𝑖,𝑗 = sl-shr𝑖,𝑗 -1 + 𝑊̂ 𝑖 ∧ sl-resi𝑖,𝑗 = sl-resi𝑖,𝑗 -1 + 𝑊̂ 𝑖 ) ∧ (sl-shr𝑖′ ,𝑗 = sl-shr𝑖′ ,𝑗 -1 − 𝑊̂ 𝑖′ ∧ sl-resi𝑖′ ,𝑗 = sl-resi𝑖′ ,𝑗 -1 − 𝑊̂ 𝑖′ ) ]
]
4.5 Layer 3: Modeling Central Monitoring Agent The central monitoring agent in Layer 3 administers the entire system — the slices, the partitions and their monitoring agents, as well as the residual partition. It plays a vital role in uniformly allocating users to slices and manages the residual partition, making necessary system adjustments if overuse is detected. Next, we describe the detailed modeling of the central monitoring agent. Adjustment of PRB-share of the residual partition: As mentioned in Section 2, the PRBs that are not allocated to the slices form the residual partition. Hence, whenever a top-up-partition or a ramp-down-partition action occurs, there will be a de-allocation or allocation of PRBs from the residual partition accordingly. There could be another interesting case of an inter-partition adjustment. For example, Partition 1 has opted for 𝑚 extra PRBs and Partition 2 wants to free 𝑛 PRBs, where 𝑛 > 𝑚. Thus, first 𝑚 PRBs are directly given to Partition 1 from Partition 2. The remaining
16
D. Banerjee et al.
(𝑛 − 𝑚) will be ramped down from Partition 2 and added to the residual partition (as discussed in Section 3). There can be several such cases based on the type of actions the individual partitions require; all such cases are handled by the central monitoring agent in Layer 3. Uniform allocation of users: We have described how the user-count is updated in constraint 𝐿1,1 in Layer 1 (ref. Section 4.2). Since there are two slices Pre1 and Pre2 for eMBB Premium in our running example, when any user of this service type joins the network, it has to be assigned either to Pre1 or to Pre2. However, random assigning may create clustering of users to only one slice, causing one partition to be overused and another to be underused. For service types having provisions in both partitions (in this case only Premium type users 1 ), we design a strategy that analyzes the uniform allocation of users within the partitions and maintains a fair distribution. For this, we consider the situation of how far a slice is from its top-up scenario, i.e., a user is assigned to a partition where the corresponding slice (based on the user’s service type) has sufficiently many PRBs before opting for a top-up. As every ‘𝑠𝑙 -𝑚’ users use up one PRB in slice 𝑠𝑙 , thus the PRB-usage is directly proportional to the number of users. Inference 6: A slice with a lower number of users has a lower PRB-usage, thus, is farther from a top-up-slice action. Hence, a user is assigned to a slice with the minimum user-count. There are other service types which are permitted to only one partition, e.g., eMBB Normal and FWA in our example. Such users are directly assigned to their corresponding slices by the central monitoring agent. In both these cases, when the residual partition falls below 50% of the total PRBs, allocating additional PRBs to slices is no more feasible, thus preventing new users from acquiring necessary resources. This condition blocks new users from accessing the network.
⌉, minInference 7: The concept of the time-window (𝑠𝑙 -𝑡 -𝑤𝑖𝑛) and determination of the maximum usage, ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 𝑚
imizes the unused PRBs with the help of the partitions’ monitoring agents in Layer 2. Moreover, the uniform user allocation in Layer 3 proportionately assigns users to slices. This prevents overuse of one partition and an increase in the unused resources in another, thereby guaranteeing PRB-optimality. 4.6
Constraints For Layer 3
Based on the discussion above, we now formally write down the constraints for the central monitoring agent in Layer
3 for our running example. The new variables introduced in this layer are listed in Table 3. We first describe the residual partition’s PRB-share (𝑟𝑝 -𝑠ℎ𝑟𝑗 ) update at the j-th timestep, followed by a discussion of the user allocation technique.
Symbols
Meaning
𝑟𝑝 -𝑠ℎ𝑟𝑗 𝜌 𝑇𝑃
PRB-share of the residual partition at 𝑗 -th timestep
𝑟𝑝 -𝑜𝑣𝑟𝑗 𝑠𝑒𝑟 -𝑝𝑟𝑜𝑣𝜇 𝑠𝑒𝑟 -𝑒𝜇,𝑗
set of partition indices, 𝜌 = {1, 2}, in our example total available PRBs residual partition-overuse flag (Boolean variable), is True at 𝑗 -th timestep if residual partition is overused, else False provision flag (Boolean variable) for the 𝜇 -th service type user entry flag for 𝜇 -th service type at 𝑗 -th timestep Table 3. New variables associated with Layer 3
1
Only for the eMBB Premium service type, there are two slices Pre1 and Pre2 in Partitions 1 and 2 respectively, each of the other service types have a single slice; Norm1 for eMBB Normal and FWA1 for FWA.
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 17 (1) No change in residual partition: There is no requirement to add or reduce PRBs from the residual partition (i.e.,
𝑟𝑝 -𝑠ℎ𝑟𝑗 = 𝑟𝑝 -𝑠ℎ𝑟𝑗 -1 ) in two cases: i) Partitions 1 and 2 (indexed with 𝑘, 𝑘 ′ ) do not opt for top-up or ramp-down-partition action (i.e., case (𝜙𝑝 , 𝜙𝑝 ) in Section 3). Thus, their PRB-shares remain the same as that in the previous timestep: i.e., ∧𝑘∈𝜌 (𝑝𝑡 -𝑠ℎ𝑟𝑘,𝑗 = 𝑝𝑡 -𝑠ℎ𝑟𝑘,𝑗 -1 ), ii) even if top-up and ramp-down-partition actions occur, the net change is zero because of the inter-partition adjustments, i.e., the number of PRBs de-allocated from one partition (𝑘 ) after a ramp-down is equal to the number of PRBs allocated to the other partition (𝑘 ′ ) after a top-up, or vice-versa (corresponding to the cases (A, D) and (D, A) in Section 3). This is expressed as: ∨𝑘,𝑘 ′ ∈𝜌, 𝑘≠𝑘 ′ (𝑝𝑡 -𝑠ℎ𝑟𝑘,𝑗 -1 − 𝑝𝑡 -𝑠ℎ𝑟𝑘,𝑗 = 𝑝𝑡 -𝑠ℎ𝑟𝑘 ′ ,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟𝑘 ′ ,𝑗 -1 ). The entire constraint is given as follows. 𝐿3,1 : ∧𝑇𝑗=1 [ { ∧𝑘∈𝜌 ( pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗 -1 ) ∨ ∨𝑘,𝑘 ′ ∈𝜌, 𝑘≠𝑘 ′ ( pt-shr𝑘,𝑗 -1 − pt-shr𝑘,𝑗 = pt-shr𝑘 ′ ,𝑗 − pt-shr𝑘 ′ ,𝑗 -1 ) }
⇒ rp-shr𝑗 =rp-shr𝑗 -1 ]
(2) Reduction of PRB-share in residual partition: At least one of the two partitions demands a top-up and the topup-partition dominates over the ramp-down-partition actions (if occurred). This happens because the neutralization between the partitions’ PRB-shares is not applicable here like the previous case. As a result, PRBs are borrowed from the residual partition. There are cases where the partitions require only top-up and at first we discuss three such cases. For example, at the 𝑗 -th timestep, any of these three cases can occur: i) case (A, 𝜙𝑝 ), i.e., a top-up-partition action in Partition 1 and no ramp-down/top-up-partition action in Partition 2 (i.e., 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 > 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 -1 ∧ 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 = 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 -1 ), or ii) vice-versa (case (𝜙𝑝 , A)), or iii) case (A, A) or top-up-partition actions in both the partitions (i.e., 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 > 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 -1 ∧ 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 >
𝑝𝑡 -𝑠ℎ𝑟2,𝑗 -1 ). The residual partition’s PRB-share is accordingly updated in the respective cases as follows: i) 𝑟𝑝 -𝑠ℎ𝑟𝑗 = 𝑟𝑝 -𝑠ℎ𝑟𝑗 -1 − (𝑝𝑡 -𝑠ℎ𝑟1,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 -1 ) or, ii) 𝑟𝑝 -𝑠ℎ𝑟𝑗 = 𝑟𝑝 -𝑠ℎ𝑟𝑗 -1 − (𝑝𝑡 -𝑠ℎ𝑟2,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 -1 ) or, iii) 𝑟𝑝 -𝑠ℎ𝑟𝑗 = 𝑟𝑝 -𝑠ℎ𝑟𝑗 -1 − [∑𝑘∈𝜌 (𝑝𝑡 -𝑠ℎ𝑟𝑘,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟𝑘,𝑗 -1 )] (𝜌 = {1, 2} as in Table 3). Now, at the 𝑗 -th timestep, let there is a top-up-partition action in Partition 1 and a ramp-down-partition action in Partition 2 (corresponding to either of the cases (A, D) and (D, A) in Section 3). Also, let the number of PRBs to be allocated to Partition 1 after a top-up is greater than the number of PRBs to be de-allocated from Partition 2 after a ramp-down (i.e., 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 -1 > 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 -1 − 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 ). In such a case, at first (𝑝𝑡 -𝑠ℎ𝑟2,𝑗 -1 − 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 ) many PRBs are ramped down from Partition 2 and allocated to Partition 1. The number of PRBs which could not be de-allocated from Partition 2, i.e., net = ((𝑝𝑡 -𝑠ℎ𝑟1,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 -1 ) − (𝑝𝑡 -𝑠ℎ𝑟2,𝑗 -1 − 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 )), are borrowed from the residual partition, thereby, reducing its PRB-share, i.e., 𝑟𝑝 -𝑠ℎ𝑟𝑗 = 𝑟𝑝 -𝑠ℎ𝑟𝑗 -1 − ((𝑝𝑡 -𝑠ℎ𝑟1,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟1,𝑗 -1 ) − (𝑝𝑡 -𝑠ℎ𝑟2,𝑗 -1 − 𝑝𝑡 -𝑠ℎ𝑟2,𝑗 )). Constraint 𝐿3,2 is given as follows.
[ ( ∧𝑘∈𝜌 ( pt-shr𝑘,𝑗 > pt-shr𝑘,𝑗-1 ) ⇒ rp-shr𝑗 = rp-shr𝑗-1 − ∑𝑘∈𝜌 (pt-shr𝑘,𝑗 − pt-shr𝑘,𝑗-1 ) ) ∨ ∧𝑘,𝑘 ′ ∈𝜌, 𝑘≠𝑘 ′ ( ( pt-shr𝑘,𝑗 > pt-shr𝑘,𝑗 -1 ∧ pt-shr𝑘 ′ ,𝑗 = pt-shr𝑘 ′ ,𝑗 -1 ) ⇒ rp-shr𝑗 = rp-shr𝑗 -1 − (pt-shr𝑘,𝑗 − pt-shr𝑘,𝑗 -1 ) ) ∨ ∧𝑘,𝑘 ′ ∈𝜌, 𝑘≠𝑘 ′ ( ( pt-shr𝑘,𝑗 > pt-shr𝑘,𝑗 -1 ∧ pt-shr𝑘 ′ ,𝑗 < pt-shr𝑘 ′ ,𝑗 -1 ∧ pt-shr𝑘,𝑗 − pt-shr𝑘,𝑗 -1 > pt-shr𝑘 ′ ,𝑗 -1 − pt-shr𝑘 ′ ,𝑗 ) ⇒ ( [ net = ( pt-shr𝑘,𝑗 − pt-shr𝑘,𝑗 -1 ) − ( pt-shr𝑘 ′ ,𝑗 -1 − pt-shr𝑘 ′ ,𝑗 ) ] ∧ rp-shr𝑗 = rp-shr𝑗 -1 − net ) ) ]
𝐿3,2 : ∧𝑇𝑗=1
(3) Increment of PRB-share in residual partition: There is a ramp-down partition action for at least one of the two partitions and here the ramp-down-partition actions dominate over the top-up-partition actions (if occurred). Thus, the PRBs de-allocated from the partitions are re-allocated to the residual partition. The sub-cases (i.e., any one of the
18
D. Banerjee et al.
cases: (𝜙𝑝 , D), (D, 𝜙𝑝 ), (D, D), (A, D) or (D, A) occur) and the constraint generation in this case are handled similarly like the previous case. The constraint is given as follows. 𝐿3,3 : ∧𝑇𝑗=1
[ ( ∧𝑘∈𝜌 ( pt-shr𝑘,𝑗-1 > pt-shr𝑘,𝑗 ) ⇒ rp-shr𝑗 = rp-shr𝑗-1 + ∑𝑘∈𝜌 (pt-shr𝑘,𝑗-1 − pt-shr𝑘,𝑗 ) ) ∨
∧𝑘,𝑘 ′ ∈𝜌, 𝑘≠𝑘 ′ ( ( pt-shr𝑘,𝑗 -1 > pt-shr𝑘,𝑗 ∧ pt-shr𝑘 ′ ,𝑗 = pt-shr𝑘 ′ ,𝑗 -1 ) ⇒ rp-shr𝑗 = rp-shr𝑗 -1 + (pt-shr𝑘,𝑗 -1 − pt-shr𝑘,𝑗 ) ) ∨ ∧𝑘,𝑘 ′ ∈𝜌, 𝑘≠𝑘 ′ ( ( pt-shr𝑘,𝑗 > pt-shr𝑘,𝑗 -1 ∧ pt-shr𝑘 ′ ,𝑗 < pt-shr𝑘 ′ ,𝑗 -1 ∧ pt-shr𝑘,𝑗 − pt-shr𝑘,𝑗 -1 < pt-shr𝑘 ′ ,𝑗 -1 − pt-shr𝑘 ′ ,𝑗 ) ⇒ ( [ net = ( pt-shr𝑘 ′ ,𝑗 -1 − pt-shr𝑘 ′ ,𝑗 ) − ( pt-shr𝑘,𝑗 − pt-shr𝑘,𝑗 -1 ) ] ∧ rp-shr𝑗 = rp-shr𝑗 -1 + net ) ) ]
(4) Uniform user allocation: Only Premium users can be assigned to any one of the two partitions, as discussed before. For simplicity in writing the following constraint, we associate a flag prov with every service ser (i.e., ser-prov), having value True (i.e., ser-prov = 𝕋), if the user has a provision in both partitions or else it is False (𝔽). Here, in our example, there are three service types in total, Premium, Normal and FWA, the last two have access in only one partition (i.e., ser-prov = 𝔽). We use 𝜇 and 𝑖𝜇 to denote the service type and its corresponding slice indices respectively. The service types Premium, Normal and FWA are numbered as 𝜇 = 1, 2 and 3. Also, as slices Pre1, Norm1, Pre2 and FWA are numbered 1, 2, 3 and 4 (ref. Section 4.1), hence, for 𝜇 = 1, 𝑖𝜇 = {1, 3}; 𝜇 = 2, 𝑖𝜇 = {2} and 𝜇 = 3, 𝑖𝜇 = {4}. If any user of the 𝜇 -th service type waits to enter the network at some timestep 𝑗 , the variable ser-e𝜇,𝑗 becomes True. Moreover, users are allowed to enter the network only if the residual partition is not overused, i.e., 𝑟𝑝 -𝑜𝑣𝑟𝑗 = 𝔽. The constraint for updating the user-entry flag (𝑠𝑙 -𝑒𝑛) of the slices having access in only one partition, is as follows. 𝐿3,4 : ∧3𝜇=1 ∧𝑇𝑗=1 [ ( ser-prov𝜇 = 𝔽 ∧ rp-ovr𝑗 = 𝔽 ∧ ser-e𝜇,𝑗 = 𝕋 ) ⇒ ∧𝑖∈𝑖𝜇 ( sl-en𝑖,𝑗 = 𝕋 ) ]
Now, we discuss the uniform user allocation corresponding to service type 𝜇 = 1 or Premium service type, i.e., allocating users uniformly between the slices Pre1 (𝑠𝑙1 ) and Pre2 (𝑠𝑙3 ). At the 𝑗 -th timestep, if the flag 𝑠𝑒𝑟 -𝑒1,𝑗 is True (𝕋), indicating that a Premium type user waits to enter the network, then we need to decide in which of the two slices,
𝑠𝑙1 and 𝑠𝑙3 , we can asign the new user. The user-entry flag (sl-en) of a slice becomes True if a new user enters the slice 𝑠𝑙 (ref. Table 1), i.e., 𝑠𝑙 -𝑒𝑛𝑖,𝑗 = 𝕋, when a user is assigned to the 𝑖-th slice at the 𝑗 -th timestep. To determine the slice-index with the minimum user-count, we introduce the function Sl-Ind(.), that takes the slice’s user-count as input and returns the slice-index. At the (𝑗 -1)-th timestep, if 𝛽 is the slice-index having the minimum user-count between slices 𝑠𝑙1 and 𝑠𝑙3 , then the user is assigned to slice 𝑠𝑙𝛽 (i.e., 𝑠𝑙 -𝑒𝑛𝛽,𝑗 = 𝕋) and not to the other slice (i.e., ∧𝑖∈𝑖𝜇 −𝛽 sl-en𝑖𝑗 = 𝔽). 𝑇 𝐿3,5 : ∧𝑗=1 [ rp-ovr𝑗 = 𝔽 ∧ ser-e1,𝑗 = 𝕋 ⇒ ( 𝛽 = Sl-Ind (min (sl-usr1,𝑗 -1 , sl-usr3,𝑗 -1 ) ) ⇒ sl-en𝛽,𝑗 = 𝕋 ∧ ∧ sl-en𝑖𝑗 = 𝔽 ) ] 𝑖∈𝑖𝜇 −𝛽
For our running example of 2 partitions and 2 slices per partition, the entire formal model of the proposed 3-layered framework, FORSLICE, is obtained by considering the consolidated constraint given as follows.
C: ∧6𝑙1 =1 𝐿1, 𝑙1 ∧ ∧6𝑙2 =1 𝐿2, 𝑙2 ∧ ∧5𝑙3 =1 𝐿3, 𝑙3 Here, 𝐿1,1 − 𝐿1,6 are the constraints in Layer 1 (ref. Section 4.2), 𝐿2,1 − 𝐿2,6 are the constraints in Layer 2 (ref. Section 4.4) and 𝐿3,1 − 𝐿3,5 are the constraints in Layer 3 (ref. Section 4.6). If constraint C is satisfiable, then we conclude that the PRB-allocation generated simultaneously ensures the system properties, fairness and PRB-optimality while prioritizing the eMBB Premium service type.
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 19 Next, we present the constraint formulation in FORSLICE for any generic (𝒮, 𝒦, 𝒩) configuration of the hierarchical 3-layered network, i.e., a 5G network scenario which is much more holistic in terms of PRB-partitioning and slicing.
4.7 Generalized Constraints for any Service-Partition-Slice Configuration Here, we consider any number of service types, partitions and slices and also different combinations of slices per partition, abiding by the 5G-network protocols and design criteria. If there are total 𝒦 partitions and 𝑟𝑘 number of 𝒦
slices in the 𝑘 -th partition, 𝑘 = 1 to 𝒦, then the total number of slices is ∑𝑘=1 𝑟𝑘 = 𝒩. The slices correspond to various service types. In our running example discussed previously, a service type can have access in more than one partition. For example, eMBB Premium service type had slices Pre1 and Pre2 in Partitions 1 and 2 respectively. We assume that there are 𝒮 service types in total in the network and 𝑛𝜇 number of slices correspond to the 𝜇 -th 𝒮
service type, for 𝜇 = 1 to 𝒮. Therefore, 𝒩 = ∑𝜇=1 𝑛𝜇 . We hence obtain the service-partition-slice configuration as
(𝒮, 𝒦, 𝒩). The generalized version of the constraints discussed in Sections 4.2, 4.4 and 4.6 (with configuration (3, 2, 4)) are given below. Layer 1: All the constraints mentioned in Section 4.2 for Layer 1 remain the same except the outer And, mentioned as ∧4𝑖=1 in each of the six constraints (𝐿1,1 − 𝐿1,6 ), is now replaced by ∧𝒩 𝑖=1 . We denote the six modified constraints as ℒ1,𝑐 , where 𝑐 = 1 to 6. Layer 2: To present the generalized constraints for 𝐿2,1 − 𝐿2,6 of Layer 2 in a compact form, we introduce the symbols Λ𝑘,0,𝑗 , Λ𝑘,1,𝑗 and Λ𝑘,2,𝑗 , that represent the sets containing the slice indices in the 𝑘 -th partition opting for 𝜙𝑠 : no requirements (neither top-up-slice nor ramp-down-slice), TU: top-up-slice, and RD: ramp-down-slice actions, respectively, at the 𝑗 -th timestep. It may be the case that the slices in the 𝑘 -th partition either opt for a top-up-slice or a ramp-down-slice action (ref. constraints 𝐿2,2 − 𝐿2,5 in Section 4.4). Also, it may happen that a few of the slices in a partition require a top-up-slice action and a few require a ramp-down-slice action; appropriate intra-partition adjustments are made within the slices in such cases (ref. constraint 𝐿2,6 ). The PRB-shares of the partitions are accordingly adjusted (increased or decreased), based on the top-up partition or ramp-down partition actions. The maximum possible usage in the 𝑖-th slice between 𝑠𝑙 -𝑡 -𝑤𝑖𝑛 two successive time-windows, 𝑊̂ 𝑖 = ⌈ 𝑠𝑙 -𝑚 𝑖 ⌉, is allocated/de-allocated to/from every slice after top-up-slice/ramp𝑖 down-slice actions, as discussed in Section 4.4. Since, Λ𝑘,1,𝑗 and Λ𝑘,2,𝑗 are the sets of slice indices requiring top-up and ramp-down in 𝑘 -th partition respectively, hence, the total number of PRBs to be allocated to the slices in the partition after top-up-slice actions is 𝜂1 = ∑𝑢∈Λ𝑘,1,𝑗 𝑊̂ 𝑢 . Similarly, the total number of PRBs to be de-allocated from the slices after ramp-down-slice actions is, 𝜂2 = ∑𝑣∈Λ 𝑊̂ 𝑣 . 𝑘,2,𝑗
If 𝜂1 > 𝜂2 or 𝜂1 < 𝜂2 (former is the case of top-up-slice actions being dominant over ramp-down-slice actions and the latter indicates ramp-down-slice actions are dominant over top-up-slice actions in the 𝑘 -th partition), then the net amount, i.e., 𝑛𝑒𝑡 = 𝜂1 −𝜂2 or 𝑛𝑒𝑡 = 𝜂2 −𝜂1 is either allocated or de-allocated from the 𝑘 -th partition; also the PRB-shares of the slices are updated accordingly. Else if 𝜂1 = 𝜂2 , then with intra-partition adjustments, there is no need to allocate or de-allocate PRBs to/from the 𝑘 -th partition; only the PRB-shares of its slices are updated. The constraint explaining this is given below. 𝒦 𝑇 ℒ2 : ∧𝑘=1 ∧𝑗=1
[ ( 𝜂 = ∑ 𝑊̂ ∧ 𝜂 = ∑ 𝑊̂ ) ∧ { ( 𝜂 > 𝜂 ⇒ (net = 𝜂 − 𝜂 ) ∧ ( pt-shr = pt-shr + net ) ) 1
𝑢∈Λ𝑘,1,𝑗
𝑢
2
𝑣∈Λ𝑘,2,𝑗
𝑣
1
2
1
2
𝑘,𝑗
𝑘,𝑗 -1
∨ ( 𝜂2 > 𝜂1 ⇒ ( net = 𝜂2 − 𝜂1 ) ∧ ( pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗-1 − net ) ) ∨ ( 𝜂1 = 𝜂2 ⇒ ( pt-shr𝑘,𝑗 = pt-shr𝑘,𝑗-1 ) ) } ∧ ( ∧𝑥∈Λ𝑘,0,𝑗 (sl-resi𝑥,𝑗 = sl-resi𝑥,𝑗-1 ) ∧ (sl-shr𝑥,𝑗 = sl-shr𝑥,𝑗-1 ) ) ∧ ( ∧𝑢∈Λ𝑘,1,𝑗 (sl-resi𝑢,𝑗 = sl-resi𝑢,𝑗-1 + 𝑊̂ 𝑢 ) ∧ (sl-shr𝑢,𝑗 = sl-shr𝑢,𝑗-1 + 𝑊̂ 𝑢 ) )
20
D. Banerjee et al.
∧ ( ∧𝑣∈Λ𝑘,2,𝑗 (sl-resi𝑣,𝑗 = sl-resi𝑣,𝑗-1 − 𝑊̂ 𝑣 ) ∧ (sl-shr𝑣,𝑗 = sl-shr𝑣,𝑗-1 − 𝑊̂ 𝑣 ) ) ] Layer 3: First we formulate the constraint for PRB-share updation of the residual partition. Let 𝒫0,𝑗 , 𝒫1,𝑗 and 𝒫2,𝑗 be the sets containing the partition indices (1 to 𝒦) which generate 𝜙𝑝 : no change, A: top-up-partition and D: ramp-downpartition actions at the 𝑗 -th timestep respectively. Based on the combinations of these actions, the residual partition share is suitably adjusted. Hence, 𝜁1 = ∑𝑢∈𝒫1,𝑗 (𝑝𝑡 -𝑠ℎ𝑟𝑢,𝑗 − 𝑝𝑡 -𝑠ℎ𝑟𝑢,𝑗 -1 ) is the number of PRBs to be allocated to the partitions after top-up-
partition actions and 𝜁2 = ∑𝑣∈𝒫2,𝑗 (𝑝𝑡 -𝑠ℎ𝑟𝑣,𝑗 -1 − 𝑝𝑡 -𝑠ℎ𝑟𝑣,𝑗 ) be the number of PRBs to be de-allocated from the partitions after ramp-down-partition actions.
If 𝜁1 = 𝜁2 , then with inter-partition adjustments, the residual partition share remains the same as that in the previous timestep. Else, if 𝜁1 > 𝜁2 (top-up-partition actions are dominant over ramp-down-partition actions) or if 𝜁2 > 𝜁1 (ramp-down-partition actions are dominant over top-up-partition actions), then the PRB-share of the residual partition accordingly decreases or increases. The following constraint expresses the above idea.
[ (𝜁1 = ∑𝑢∈𝒫1,𝑗 (pt-shr𝑢,𝑗 − pt-shr𝑢,𝑗-1 ) ∧ 𝜁2 = ∑𝑣∈𝒫2,𝑗 (pt-shr𝑣,𝑗-1 − pt-shr𝑣,𝑗 )) ∧ [ ( 𝜁1 > 𝜁2 ⇒ rp-shr𝑗 = rp-shr𝑗 -1 − (𝜁1 − 𝜁2 ) ) ∨ ( 𝜁2 > 𝜁1 ⇒ rp-shr𝑗 = rp-shr𝑗 -1 + (𝜁2 − 𝜁1 ) ) ∨ ( 𝜁2 = 𝜁1 ⇒ rp-shr𝑗 = rp-shr𝑗 -1 ) ] ]
𝑇 ℒ3,1 : ∧𝑗=1
Next, we discuss the uniform user allocation constraint. Let 𝑛𝜇 be the number of slices corresponding to the 𝜇 -th service type, 𝜇 ≤ 1 ≤ 𝒮, i.e., 𝑛𝜇 = |𝑖𝜇 |. These variables are defined above the constraint 𝐿3,5 in Section 4.6. Conditions
𝑛𝜇 = 1 and 𝑛𝜇 > 1, indicate that the 𝜇 -th service has access in only one, and more than one partition respectively. The generalized constraint 𝐿3,5 is as follows. 𝑆 𝑇 ℒ3,2 : ∧𝜇=1 ∧𝑗=1 [ (rp-ovr𝑗 = 𝔽 ∧ ser-e𝜇,𝑗 = 𝕋 ) ⇒
𝑛 ( 𝛽 = Sl-Ind ( 1≤𝑥≤𝑛 𝑚𝑖𝑛 ( sl-usr𝑥,𝑗 -1 ) ) ⇒ sl-en𝛽,𝑗 = 𝕋 ∧ ∧ 𝑥=1 sl-en𝑥,𝑗 = 𝔽 ) ] 𝜇
𝜇
𝑥≠𝛽
The final constraint 𝒞 = ∧6𝑖=1 ℒ1,𝑖 ∧ ℒ2 ∧2𝑖=1 ℒ3,𝑖 , is provided to the SMT solver. An answer, SAT or satisfiable, proves that the PRB-allocation generated through the proposed model FORSLICE satisfies all the system properties while preserving the service level priorities.
4.8
Estimation of the Total Number of Constraints
Here, we obtain an upper bound on the total number of constraints formulated in all three layers. Layer 1: Layer 1 comprises of the slices and each slice is modeled with the set of constraints, ∧6𝑖=1 ℒ1,𝑖 . Hence, there are 6 × 𝑇 × 𝒩 many constraints in Layer 1 in total, on simulating till the timestep 𝑇 . Layer 2: In Layer 2, each of the 𝑟𝑘 slices in the 𝑘 -th partition can opt for exactly one of the following three types of actions at the 𝑗 -th timestep: no action (neither top-up nor ramp-down), top-up-slice, and ramp-down-slice. This leads to a total of 3𝑟𝑘 possible combinations at each timestep, each of which is modeled with a constraint. All such possible cases are mentioned in constraint ℒ2 . As the same argument holds at each timestep, the total number of constraints 𝒦
in Layer 2, up to timestep 𝑇 , is ∑𝑘=1 𝑇 × 3𝑟𝑘 .
Layer 3: For the residual partition share management, similar to the monitoring agents in the second layer, the central monitoring agent too needs to adhere to three type of actions — no action (PRB-shares in partitions remain
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 21 same), top-up-partition, and ramp-down-partition — to decide on the PRB-share of the residual partition. Consequently, the central monitoring agent deals with 3𝒦 combinations for 𝒦 many partitions in total. Moreover, the uniform user allocation to slices is aided by the determination of the minimum user-count amongst all the slices of the same service type. In order to calculate the minimum value and evaluate the value of 𝑠𝑙 -𝑒𝑛𝑖,𝑗 to True or False, 𝑛𝜇 comparisons and 𝑛𝜇 update equations (both checked through constraints) are performed at each timestep, for 𝑛𝜇 many slices corresponding to the 𝜇 -th service type. Following the above arguments, the total number of constraints executed in Layer 3, up to timestep 𝑇 is, 𝑇 × (3𝒦 + 𝒮 ∑𝜇=1 2 × 𝑛𝜇 ).
Taking into account the internal sub-constraints, we state that the total number of constraints in all the three layers 𝒦
𝒮
is of 𝑂(𝑇 × (6𝒩 + ∑𝑘=1 3𝑟𝑘 + 3𝒦 + ∑𝜇=1 2𝑛𝜇 )) = 𝑂(𝑓 (𝑇 , 𝒮, 𝒦, 𝒩)). This wraps up the entire formal modeling of FORSLICE and next we present a set of experiments to justify that the proposed framework efficiently ensures the system properties. 5 Experimental Evaluation In this section, we evaluate the proposed formal framework FORSLICE, based on the following four research questions. Q1. How effectively does FORSLICE maintain the system properties, fairness and PRB-optimality? Q2. How does the PRB-allocation in FORSLICE benefit best-effort services? Q3. How does increasing the number of timesteps affect the execution time of FORSLICE? Q4. How does FORSLICE compare with the baseline [15] in terms of system properties? Implementation: To address the above questions, we evaluate FORSLICE by considering various types of input configurations, specifically by varying the following input parameters. (1) Total number of service types (𝒮), (2) Total number of partitions (𝒦), (3) Total number of slices (𝒩), (4) Number of slices per partition Different (𝒮, 𝒦, 𝒩) configurations are created by varying the above parameters. For example, in the (3, 2, 4) configuration discussed in Section 3, we considered 3 service types with 2 partitions and 4 slices; Partitions 1 and 2 contains 2 slices each. Here, we account for three other types of configurations, viz., (3, 3, 7), (5, 3, 10) and (5, 4, 13), where either 𝒮 or 𝒦 is increased, thereby increasing the total number of slices, 𝒩. Note that an increase in the number of service types, 𝒮, contributes to a larger number of users in the network. This increases the number of slices per partition (thus the total number of slices 𝒩) to cater the users with differentiated quality of service depending on their needs. Moreover, 𝒩 automatically increases with an increase in the number of partitions (𝒦), since a single partition has at least one slice. Consider the (3, 3, 7) configuration. We fix the number of service types (𝒮) to 3 as in (3, 2, 4), and increase one more partition (from 2 to 3) and the total number of slices 𝒩 (from 4 to 7), to obtain 3 partitions with 7 slices. On the other hand for the (5, 3, 10) configuration, keeping the number of partitions (𝒦) fixed, we increase the number of service types 𝒮 (from 3 to 5) and the number of slices per partition, which in turn increases the total number of slices 𝒩 (from 7 to 10). Finally, for the (5, 4, 13) configuration, we keep the parameter 𝒮 fixed, as in (5, 3, 10), and increase both 𝒦 and 𝒩 to construct 4 partitions with 13 slices. Note that with an increase in the total number of services (𝒮), partitions (𝒦) and slices (𝒩), the number of users per partition also increases. Thus, while evaluating FORSLICE by considering multiple (𝒮, 𝒦, 𝒩) configurations, we simultaneously examine its effectiveness by varying the total user count.
22
D. Banerjee et al. The 5G service types considered in this work are: enhanced mobile broadband (eMBB) — eMBB Premium (Pre) and
eMBB Normal (Norm), fixed wireless access (FWA), ultra-reliable low-latency communications (URLLC) and massive machine-type communications (mMTC). We have chosen the standard service types from the 3GPP specification [2] for our experiments. Considering up to 13 slices at maximum for 5 service types is in accordance with the standard network protocol and design criteria followed for 5G telecommunication networks (Table 5.15.2.2-1 on Page 23 in [4] mentions that are 6 standardized service-slice types (SST), whereas, we test up to 13 slices so that it can handle future standard SSTs). The user distributions vary according to the service types; for example, in usual practice, eMBB services are often characterized by heavy-tailed distributions (such as lognormal), whereas FWA services typically follow a Poisson distribution, etc. Based on such user distributions, we construct the user inputs (arrival and leaving of users) to our formal model. We first generate random data following the stipulated distributions and then convert the generated probability density values (according to the probability density function or mass function) into binary flags (0/1), using thresholds. If the probability is above the given threshold for the 𝑖-th slice at the 𝑗 -th timestep, then we set the user entry flag slen𝑖,𝑗 = 1, else we set sl-en𝑖,𝑗 = 0 (ref. Table 1 for the definition of sl-en𝑖,𝑗 ). With the generated user data corresponding to a particular (𝒮, 𝒦, 𝒩) network configuration and the simulation time horizon given as input, we simulate FORSLICE (see the automated workflow in Figure 4) for a finite number of timesteps, to obtain the PRB-allocations of slices and partitions as outputs. The workflow provides a fully automated, end to end solution — processing the inputs to formulate all the three-layer constraints, invoking an SMT solver for verification, and finally generating PRB-allocations if the set of constraints are satisfiable. From the allocations generated as output, we can compute other parameters, such as, number of top-up-slice and ramp-down-slice actions (based on the number of times PRBs have been allocated/de-allocated to/from slices), residual partition share (the PRBs not allocated to the slices), etc. These parameters allow us to resolve the research questions stated previously. Experimental Setup: We have used the Z3 SMT solver [20] with Python API to formally model FORSLICE. The userdata generation, following various probability distribution functions, is implemented by integrating the ‘scipy.stats’ module in Python. All these experiments are carried out on a 64-bit Windows OS in a 2.10 GHz Intel Core-i5 machine, with 32 GB of RAM. The network simulations are performed by connecting user equipments (UEs) to a single base station (gNB) in the network simulator NS3-5Glena [1]. 5.1
Q1. Checking Fairness and PRB-Optimality
Here, we present two sets of experiments to demonstrate that FORSLICE ensures the system properties: fairness and PRB-optimality. 5.1.1
Residual Partition Share. First, we check the fairness by analyzing the PRB-share of the residual partition. Figure
5 shows how the final residual partition shares vary with the four (𝒮, 𝒦, 𝒩) configurations and for three different values (100, 200 and 300) of the total PRB count, when FORSLICE is simulated for 30 timesteps, e.g., for 30 min (with one timestep ℎ = 1 min). Each bar plot in the figure depicts the PRB-share of the residual partition in the final timestep (i.e., the 30-th timestep) for a particular (𝒮, 𝒦, 𝒩) configuration and a fixed total PRB count. To generate the data for each bar plot, we ran the FORSLICE simulation 30 times generating different instances of user data (sl-en𝑖,𝑗 and sl-lv 𝑖,𝑗 ) in each trial. Specifically, our evaluation utilized a large volume of user data instances.
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 23 The corresponding confidence interval, obtained considering 30 runs of the simulation for a single case, is also marked in each bar plot. The (5, 4, 13) configuration exhibits a bit of anomaly, with respect to the total PRB count. There are 4 partitions and 13 slices in total for this configuration, and due to the uniform allocation of users to the partitions by the central monitoring agent (ref. ℒ3,2 , generalized constraint for 𝐿3,5 ), users are almost equally spread into the four partitions, if they have provisions in more than one partition. Thus, 100 PRBs, is too low to be allocated to the users among 13 slices. Hence, for this configuration, the results are shown only for the cases with total PRB as 200 or 300. For the rest of the three configurations, the results for all three cases of 100, 200 and 300 total PRBs are shown in Figure 5. It is clearly evident from the figure that with an increase is greater (due to the larger number of users assigned to the slices) and therefore the PRB-share of the residual partition gradually drops. Furthermore, for all four configurations and for all total PRB counts, the PRB-share of the residual partition is at least 50% of the total PRBs, which implies that the residual partition is not yet overused. This
Residual Partition Share (%)
in the number of slices and partitions, the PRB utilization
is specifically achieved due of the design of the following
300 PRB
40
20
1
2
3
4
( 3, 2, 4 )
( 3, 3, 7 )
( 5, 3, 10 )
( 5, 4, 13 )
Service-Partition-Slice Configurations
justments to manage the residual partition PRB-share (ref. constraint ℒ3,1 in Section 4.7), and ii) uniform allocation of
200 PRB
60
0
constraints in Layer 3 of our model: i) inter-partition ad-
100 PRB
80
Fig. 5. The final residual partition share for different PRB
users within partitions (ref. constraint ℒ3,2 in Section 4.7). counts in four (𝒮, 𝒦, 𝒩) configurations, for 30 timesteps These actions reduce clustering of users in one partition and prevent continuous overuse of the residual partition. Therefore, the PRB-share of the residual partition (denoted by the variable rp-shr 𝑗 at the 𝑗 -th timestep, ref. Table 3) does not get overused. Consequently, the boolean variable rp-ovr 𝑗 (that becomes True in case of a residual partitionoveruse scenario, ref. Table 1) remains False (𝔽) at the 30-th timestep. This implies that a top-up signal (sl-top) can be generated in a slice whenever there is PRB-requirement from the user end (ref. constraint 𝐿1,4 ). Based on the formal modeling of FORSLICE, extra PRBs are allocated to slices upon the generation of top-up signals (ref. constraints 𝐿2,2 , 𝐿2,4 and 𝐿2,6 ), ensuring fairness to each service type, as per Definition 2.1.
5.1.2 Top-up-slice and Ramp-down-slice Actions. We now demonstrate that FORSLICE strikes a balance between the total number of top-up-slice and ramp-down-slice actions, to ensure fairness and PRB-optimality simultaneously. Topup in a slice is required to guarantee fairness to the users of the slice corresponding to a particular service type, whereas ramp-down in a slice is necessary to reduce the extra and unused PRBs from a slice, minimizing the PRB-usage. The proposed model aims to reduce the overall dynamic actions: top-up-slice and ramp-down-slice actions, while ensuring fairness and PRB-optimality. The number of top-up-slice and ramp-down-slice actions in a duration of 30 timesteps, for a total PRB count of 200, is exemplified in Table 4. We observe that when both partitions and slices are increased, the number of top-up-slice actions also increases to provide the users with the desired amount of PRBs (⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉ many PRBs during one time interval) and thereby 𝑚 guarantee fairness. However, interestingly the rate of increase is not that high. For example, corresponding to the
24
D. Banerjee et al. (𝒮, 𝒦, 𝒩)
# Top-Up-
# Ramp-Down
Configuration
Slice Actions
Slice Actions
1
(3, 2, 4)
6
0
2
(3, 3, 7)
7
0
3
(5, 3, 10)
6
3
4
(5, 4, 13)
10
0
Row No.
Table 4. Total number of top-up-slice and ramp-down-slice actions for 200 PRBs
(3, 2, 4) configuration, there are 6 top-up-slice actions in 4 slices after simulating for 30 timesteps; whereas there are just 7 top-up-slice actions in a larger number of slices (7 slices) for the (3, 3, 7) configuration (Rows 1-2). The primary reason behind this is as follows. A top-up-slice action allocates ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉ many extra PRBs (the maximum 𝑚 usage amount) to a slice 𝑠𝑙 after a top-up, such that there are sufficiently many PRBs till the next time window (according to Inference 5). Hence, within a time-interval, there is no need for a top-up in a slice; the action is commenced only if it is truly essential to allocate extra PRBs further (i.e., when the residual PRB in a slice, sl-resi𝑖,𝑗 , is less than the amount, ⌈ 𝑠𝑙 -𝑠𝑙𝑡 --𝑤𝑖𝑛 ⌉, as per constraint 𝐿1,4 ). 𝑚 Furthermore, with an increase in both the number of partitions and slices, the users are uniformly allocated within the partitions. The PRBs are thus uniformly utilized by the users and do not remain unused in a particular slice due to overuse in another. Therefore, it is not required to evoke ramp-down-slice actions often to de-allocate the excess unused PRBs. However, keeping the number of partitions fixed, if only the number of slices is increased, then the clustering of users becomes larger in one partition, resulting in its overuse and a low PRB usage in another. This increases the chances of a ramp-down-slice action in the slice with a larger number of unused PRBs. The unused PRBs can be then ramped down and offered to another slice which is in requirement of extra PRBs (ref. constraint 𝐿2,6 in Layer 2). Such a scenario is reported in Rows 2-3; where for the same set-up of 3 partitions, the number of slices increases from 7 to 10, thereby escalating the ramp-down slice actions in the latter case. Nevertheless, this simultaneously minimizes the unused PRBs in slices, ensuring PRB-optimality (according to Inference 5 and 7). In summary, FORSLICE preserves the system properties, fairness and PRB-optimality, however, it tries to evoke the top-up-slice and ramp-down-slice actions as less as possible to avoid unnecessary allocations and de-allocations at the runtime. 5.2
Q2. Benefiting Best-Effort Services
The PRB-allocation approach in this work also aims to cater the best-effort services (services having no specific QoS requirements like eMBB, FWA), apart from ensuring fairness and PRB-optimality while prioritizing the eMBB Premium service type. The following two strategies in FORSLICE specifically make provision for the best-effort services that access the residual partition. i) A top-up signal can be generated in a slice only when the residual partition is not overused, i.e., when it has more than 50% of the total PRBs (ref. constraint 𝐿1,4 in Layer 1). If overused, we avoid a top-up-slice action, unless PRBs are re-allocated to the residual partition after some time. ii) On having excess unused PRBs in a slice for a long duration, the unused amount is ramped-down from the partition (corresponding to that slice) and re-allocated to the residual partition (ref. constraint 𝐿1,5 in Layer 1 and constraint 𝐿3,3 in Layer 3).
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 25 iii) The inter-partition adjustments in Layer 3 often lead to scenarios in which PRBs need not to be de-allocated from the residual partition after top-up-slice actions (ref. constraint 𝐿3,1 in Layer 3). We now discuss experimental results illustrating how best-effort services gain from the PRB-share management of the residual partition, which is particularly achieved due to the aforementioned strategies. We observe in Figure 5 that the final residual partition share is much greater than 50% of the total number of PRBs, in all cases. It is illustrated in Section 5.1.1 that such scenarios ensure fairness to every service type, by providing the facility for a top-up-slice action in times of PRB-requirement. Thus, the proposed model FORSLICE allocates PRB in such a manner, which apart from guaranteeing fairness, also allows for a sufficient amount of PRBs (50% of the total amount) to be utilized by multiple best-effort services. Additionally, the illustration and the results provided in Section 5.1.2 indicate that the rate of increase in the number of top-up-slice actions is quite low, even with increasing slices and partitions. Moreover, ramp-down-slice actions are invoked to reduce unused PRBs when there is an overuse in one partition and PRBs remain relatively unutilized in another. Both these factors prevent the residual partition from getting overused, highlighting that the PRB-allocations/deallocations in FORSLICE ensure PRB-optimality and simultaneously accounts for the residual partition to have 50% of the total PRBs. 5.3 Q3. Execution Time Here, we explain how the execution time of FORSLICE varies with the number of timesteps. For this experiment, we consider three input combinations: 30, 50 and 70 timesteps (e.g., 30 min, 50 min and 70 min), respectively, to observe the rate of increase in the execution time with higher values of timesteps. For all four (𝒮, 𝒦, 𝒩) configurations and for different values of timesteps, the respective minimum and average verification times (averaged over 3 runs) are shown in Table 5. (𝒮, 𝒦, 𝒩)
( 3, 2, 4 )
( 3, 3, 7 )
Timesteps
30
50
70
30
50
70
Min Time (s)
3.50
32.97
157.31
23.67
41.14
366.65
Avg Time (s)
12.49
94.49
439.20
32.66
100.57
417.99
70
30
(𝒮, 𝒦, 𝒩)
( 5, 3, 10)
(5, 4, 13)
Timesteps
30
50
Min Time (s)
74.688
183.05
457.15
Avg Time (s)
133.63
319.88
1195.17
50
70
116.61
977.15
4145.75
216.90
1439.53
5037.29
Table 5. Execution time with varying timesteps
Through our experiments, we observe that the execution time increases with increasing timesteps, as well as with an increase in the number of slices and partitions. For a smaller number of slices, e.g., for 4 slices, the execution time taken is mostly within 12 s-7 min, whereas, for 7 slices, it is approximately around 7 min, up to 70 timesteps. For 10 slices, the execution time is less than 5.5 min up to 50 timesteps; it increases to 20 min in average for higher timesteps. Finally, for 4 partitions and 13 slices, the time varies between 3.5 min-24 min up to 50 timesteps, and increases quite a bit, nearly 1.4 h, for 70 timesteps. Therefore, in almost all cases, FORSLICE can be executed within a reasonable time frame; e.g., within half an hour. We consider the user arrival data following the user distributions for specific service types, compliant with the 5G telecommunication network protocols. Also, the number of slices is considered following real practice, 8 − 13 in
26
D. Banerjee et al.
general. Since our modeling adheres to such standard design criteria and yields reasonable execution times for PRBallocation over a given simulation time range, we are confident that FORSLICE is practically viable for deployment in real applications. 5.4
Q4. Comparison with Baseline
To our knowledge, the only existing work that considers similar PRB-partitioning and RAN-slicing scenarios, accounting for fairness and prioritizing eMBB Premium service, is [15]. Their proposed method ‘Convergence’ employs an AI planning agent to solve the PRB-allocation problem. However, the method is limited to the PRB-allocation solution only for a single case study: 3 service types, 2 partitions and 2 slices per partition (Pre1, Norm1 in Partition 1 and Pre2, FWA1 in Partition 2). In contrast, the proposed formal framework, FORSLICE, 20
allocations for any configuration of services, partitions
18
and slices. Moreover, our work addresses residual-partition
16
share management in order to serve the best-effort services, which is not accounted for in [15]. To demonstrate the efficiency of FORSLICE, we compare
PRB-share (%)
is generic and automated, and successfully computes PRB-
14 12 10
the PRB-share percentage in eMBB Premium slices, with
6
the AI-planning based solution method, Convergence. Since
4
both the methods prioritize the eMBB Premium service type, we consider the metric, PRB-share in eMBB Premium slices, to highlight how FORSLICE simultaneously ensures fairness and PRB-optimality, with a priority to the eMBB
Convergence: Pre1
8
FORSLICE:
Pre1
Convergence: Pre2 FORSLICE:
Pre2
2 0
5
10
15
20
25
30
Timesteps
Fig. 6. Comparing % of PRB-share in eMBB Premium slices with Convergence
Premium service type, in contrast to Convergence. For this experiment, we consider the (3, 2, 4) configuration, i.e., 2 partitions and 2 slices per partition (Pre1, Norm1 in Partition 1 and Pre2, FWA1 in Partition 2), since this is the only configuration considered in [15]. Finally, we simulate both models for 30 timesteps. Starting with the same initial PRB-share, it is clear from Figure 6 that at all timesteps, the percentage of the PRBallocations to any of the slices, Pre1 or Pre2, in Convergence, is greater than that in FORSLICE. Although this prioritizes eMBB Premium serivce type and guarantees fairness in [15], PRBs are over-provisioned to the slices in their case (at least by 44.45% as compared to ours). Rather, we ensure fairness with a much lower percentage of allocated PRBs, as we minimize the allocated but unused PRBs in the slices. This comparison thus highlights the PRB-optimality in FORSLICE (Inferences 5, 7). Moreover, the residual partition PRB-share is larger in our case (as allocations to slices are lesser), thereby benefiting the best-effort services. 6 A Case Study: Network Simulation Here, we consider a practical example of Ericsson’s PRB-partitioning in Saltlake Kolkata, to discuss the network performance achieved in FORSLICE. There is a diverse demand for services in that region, like eMBB (demanding a large share of PRBs during peak evening hours for high throughput, especially in the office areas), FWA (having PRB requirements to ensure a minimum throughput), etc. To provide guaranteed SLAs and traffic isolation for different services running over the same physical infrastructure, efficient PRB-allocations is a necessity.
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 27
Central monitoring agent
Layer 3
Residual partition
Layer 2
Layer 1
Partition 1
Partition 2
Partition 3
Monitoring agent 1
Monitoring agent 2
Monitoring agent 3
Pre1
Norm1
Pre 2
Norm2
FWA1
Pre3
FWA2
Slices
a RAN slicing scenario
b 3-layered FORSLICE framework
Fig. 7. Network configuration (3, 3, 7): service types eMBB Premium, Normal and fixed wireless traffic; slices Pre1 and Norm1 in Partition 1; Pre2, Norm2 and FWA1 in Partition 2; Pre3 and FWA2 in Partition 3
Based on the user categories and resource demands, we have considered 3 partitions with the slice types as eMBB Premium, eMBB Normal and FWA. Specifically, we obtain the (3, 3, 7) network configuration: 3 service types, 3 partitions, and 7 slices. The RAN-slicing and PRB-partitioning scenario for this configuration is shown in Figure 7a, where Partition 1 has two slices: Pre1 and Norm1; Partition 2 has three slices: Pre2, Norm2 and FWA1; and Partition 3 has two slices: Pre3 and FWA2. The unallocated PRBs form the residual partition. The proposed 3-layered framework, FORSLICE, for such a hierarchical network structure is also depicted in Figure 7b. In this case study, eMBB Premium slices — which have higher priority — are present across all partitions, and every service type has access to more than one partition. We can observe that there is a differentiated quality of service requirements (varied 5QIs in the figure). Fairness in resource allocation implies that each service type receives its required share of PRBs and achieves the desired throughput levels, with a priority to the eMBB Premium service type. Now, we consider a network simulation for the
Throughput ( Mbps )
35 (3, 3, 7) configuration, to demonstrate the network perOffered Throughput Obtained Throughput 30 formance of FORSLICE, measured in terms of the aver25 age throughput per slice over all the timesteps. Specifi20 cally, we show that the throughput achieved by the PRB15 allocations and de-allocations in FORSLICE is almost sim10 ilar to the throughput observed in the actual network 5 simulation, indicating that FORSLICE maintains the de0 sired network performance. Pre1 Norm1 Pre2 Norm2 FWA1 Pre3 FWA2 Partition 2 Partition 3 Partition 1 We simulate the (3, 3, 7) configuration for 30 timesteps in the network simulator NS3-5Glena [1]. At each Fig. 8. Throughput: offered (FORSLICE) vs obtained (NS3-5Glena) timestep, we associate 1 to 36 UEs (based on the usercount in FORSLICE) with the slices. All the UEs are connected to a single 5G base station (gNB) in a clear Line-of-Sight (LoS) path through an isotropic antenna model [1]. Each service type follows a full buffer UDP traffic model [21].
28
D. Banerjee et al.
Furthermore, we consider the rest of the simulation parameters as the default setup. Specifically, the telecommunication network parameters: central frequency, bandwidth, transmission power, modulation scheme, numerology, and component carrier values are set up at 7GHz, 100MHz, 47dBm, 256QAM, 0, 1, respectively. We use the PRB-allocation outcome from the FORSLICE model to calculate the offered throughput. The actual network simulation in NS3-5Glena provides the obtained throughput for each slice. Figure 8 shows that both the offered and obtained throughput depict nearly similar behaviors for all slices. Therefore, we conclude that the allocated PRB-share in each slice attains the throughput as per the expectation (see Eq. (2) and Inference 4 for the relationship between PRBusage and throughput requirements). Moreover, the offered and the obtained throughput for Premium service types is always greater than that of the Normal ones, thereby prioritizing the eMBB Premium service type (as observed in Inference 3). 7 Related Work To the best of our knowledge, formal methods have not been applied in the RAN slicing domain in any prior research. Thereby, we separately explore the existing methods in two directions: PRB-allocation in RAN and formal methods in telecommunication. PRB-Allocation in RAN: Resource allocation in network slices is well-studied in various contexts [15, 19, 22, 24]. The work in [19] uses network slicing to study service-aware baseband resource allocation and virtual network function activation in open-RAN systems. This work deals with the three service types eMBB, URLLC and mMTC, and applies Lagrangian function and Karush-Kuhn-Tucker conditions to obtain optimal PRB-allocation in open-RAN systems. The work in [24] considers the media access control layer scheduling perspective; analyzes the multiplexing of eMBB and URLLC traffic in 5G downlink transmission. The resource allocation problem, considered for eMBB and URLLC network slices, is formulated as an ILP, such that the original eMBB users’ aggregate utility is maximized while guaranteeing the QoS of URLLC users. The method proposed in [22] also accounts for eMBB and URLLC service types, but focuses on joint scheduling of transmit power and PRBs for remote radio heads in the 5G cloud RAN systems. The resource-allocation problem is formulated as a mixed-integer non-linear program and a penalized successive convex approximation determines a suboptimal solution in polynomial time. The only work that considers resource allocation to RAN slices while adopting the similar PRB-partitioning approach as ours, is [15]. An AI-planning agent is employed to solve the PRB-allocation problem in [15], accounting for fairness and prioritizing eMBB Premium service. However, their method is limited to a particular case study, whereas our proposed framework is generic and computes PRB-allocation for any configuration of the 3-layered network. Furthermore, the experimental comparisons show that the PRB-allocation in FORSLICE exhibits enhanced optimality and also caters the best-effort services, in contrast to [15]. Formal Methods in Telecommunication Networks: In the recent past, formal methods have been used in moderation in the networking area [5, 13, 14, 17, 18]. The authors in [14] address formal modeling and verification of call admission control strategy (CAC), specifically used for voice communication. Probabilistic model checking and continuous-time Markov Chains model is used to describe the CAC schema. The work in [17] formally verifies an existing 5G service orchestration solution (i.e., coordination of network resources) and checks if the solution meets the service-level agreements over various dynamic behaviors, like, dynamic network load and link utilization. Formal verification is used on a security protocol named, EAP-AKA (Extensible Authentication Protocol - Authenticated Key Agreement) in [5] to guarantee secure transmission of user data. It uses a tool named Pro-Verif, to evaluate the extent to which the attacker can intrude on the communication path. Although formal methods explore on different aspects of
FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services 29 network problems, it is limited to higher layer resource management. Moreover, the joint exploration on the resource allocation in RAN and formal methodology is still an open area of research. 8 Conclusion In 5G network slicing, differentiated quality of service (QoS) is provided to various service types having multiple priorities. Hence, to achieve RAN slicing, it is crucial to develop a dependable design strategy for resource allocation to RAN slices, i.e., the system properties like — ensuring appropriate provision of the desired resources to a higher priority service type, while guaranteeing fairness to all other service types and preserving resource-optimality — must always be satisfied to uphold network performance standards. The basic unit of radio resource is PRB, and the objective of this work is to efficiently allocate PRBs to RAN slices corresponding to multiple service types. To ensure the correctness of the solution to the PRB-allocation problem, we formally model the problem as a 3-layered framework, FORSLICE and we employ formal verification to verify the following system properties: maintenance of a particular range of throughput for Premium users (prioritizing Premium customers), guaranteeing a minimum share of PRBs and throughput to each service (guaranteeing fairness) and minimization of the allocated but unused PRBs (PRB-optimality). To the best of our knowledge, this is the first work leveraging formal verification in solving the PRB-allocation problem in multipriority multi-services scenarios. We synthesize an automated formal framework and substantiate the efficiency and applicability of the proposed framework with a handful of experiments. Formal modeling and verification involving a broader range of KPIs offers a compelling avenue for future research. Acknowledgments This work was funded by Ericsson Research India. References [1] [n. d.]. Open-source 5G new radio (NR) network simulator. https://5g-lena.cttc.es/. [2] 3GPP. 2022. System architecture for the 5G system (5GS) (Release 17). In ETSI TS 23.501 V17.5.0 (2022-07). [3] 3GPP. 2024. 3rd Generation Partnership Project; Technical specification group radio access network; NR; User equipment (UE) radio access capabilities (Release 18). In TS 38.306 V18.2.0 (2024-06). [4] 3GPP. 2024. System architecture for the 5G System (5GS) (Release 18). In TS 23.501 V18.5.0 (2024-05). [5] Megha Ajit, Sriram Sankaran, and Kurunandan Jain. 2021. Formal verification of 5G EAP-AKA protocol. In Proc. International Telecommunication Networks and Applications Conference. 140–146. [6] Sihem Bakri, Pantelis A Frangoudis, and Adlen Ksentini. 2019. Dynamic slicing of RAN resources for heterogeneous coexisting 5G services. In Proc. Global Communications Conference. 1–6. [7] Debarpita Banerjee, Parasara Sridhar Duggirala, Bineet Ghosh, and Sumana Ghosh. 2025. A Formal approach towards safe and stable schedule synthesis in weakly hard control systems. ACM Transactions on Embedded Computing Systems (TECS) 24, 5s (2025). [8] Edmund M. Clarke, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model Checking. MIT Press. [9] Ericsson. 2020. 5G RAN slicing. https://www.ericsson.com/4addb2/assets/local/networks-slicing/docs/ericsson-5g-ran-slicing.pdf. [10] Devleena Ghosh, Sumana Ghosh, Raj Kumar Gajavelly, and Ansuman Banerjee. 2023. Harnessing multiple BMC engines together for efficient formal verification. In Proc. Formal Methods and Models for System Design. 71–81. [11] Sumana Ghosh, Soumyajit Dey, and Pallab Dasgupta. 2019. Performance and energy aware robust specification of control execution patterns under dropped samples. IET Computers & Digital Techniques (2019). [12] Sumana Ghosh, Soumyajit Dey, and Pallab Dasgupta. 2020. Pattern guided integrated scheduling and routing in multi-hop control networks. ACM Transactions on Embedded Computing Systems 19, 2 (2020), 1–28. [13] Fengchen Gong et al. 2023. Towards integrating formal methods into ML-based systems for networking. In Proc. ACM Workshop on Hot Topics in Networks. 48–55. [14] Maroua Idi, Sana Younès, and Riadh Robbana. 2022. Performance evaluation of call admission control strategy in cloud radio access network using formal methods. In Proc. International Conference on Software Technologies. 630–640.
30
D. Banerjee et al.
[15] Ajay Kattepur et al. 2024. Convergence: Cognitive intent driven 5G radio access network slice assurance. In Proc. Wireless Communications and Networking Conference. 01–06. [16] Moez Krichen. 2023. A survey on formal verification and validation techniques for internet of things. Applied Sciences 13, 14 (2023), 8122. [17] A Kunnappilly, P Backeman, and C Seceleanu. 2021. From UML modeling to UPPAAL model checking of 5G dynamic service orchestration. In Proc. Engineering of Computer Based Systems. 1–10. [18] Sergey Litvinyuk, Pavel Pilyugin, and Andrey Petukhov. 2024. Formal methods for building network-level information security policies . In Proc. Modern Computer Network Technologies. 1–5. [19] Mojdeh Karbalaee Motalleb, Vahid Shah-Mansouri, Saeedeh Parsaeefard, and Onel Luis Alcaraz López. 2022. Resource allocation in an open RAN system using network slicing. IEEE Transactions on Network and Service Management 20, 1 (2022), 471–485. [20] Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An efficient SMT solver. In Proc. Tools and Algorithms for the Construction and Analysis of Systems. Springer, 337–340. [21] L. O. Ostrowsky, N. L. S. da Fonseca, and C. A. V. Melo. 2007. A Traffic Model for UDP Flows. In Proc. International Conference on Communications. 217–222. [22] Mehdi Setayesh, Shahab Bahrami, and Vincent WS Wong. 2020. Joint PRB and power allocation for slicing eMBB and URLLC services in 5G C-RAN. In Proc. Global Communications Conference. 1–6. [23] Alireza Souri, Nima Jafari Navimipour, and Amir Masoud Rahmani. 2018. Formal verification approaches and standards in the cloud computing: a comprehensive and systematic review. Computer Standards & Interfaces 58 (2018), 1–22. [24] Hao Yin, Lyutianyang Zhang, and Sumit Roy. 2020. Multiplexing URLLC traffic within eMBB services in 5G NR: Fair scheduling. IEEE Transactions on Communications 69, 2 (2020), 1080–1093.