Formal dependability analysis of fault tolerant Virtual Machine allocation strategies in Cloud Radio Access Network

Cloud Radio Access Network (C-RAN) has been proposed as a fifth generation (5G) cellular network that is designed to physically separate the Baseband Units (BBUs) from the Remote Radio Heads (RRHs). The BBUs are placed in the BBU pool/hotel, while the RRHs are located in the cells. This separation enables sharing baseband processing resources among RRHs by generating Virtual Machines (VMs) in the BBU pool, leading to radio coordination and energy saving opportunities. Nevertheless, the failure of a BBU can affect several RRHs, causing outages in the radio network. Therefore, designing a reliable and resilient C-RAN is essential to provide high availability and service continuity in case of BBU failure. This paper deals with using formal verification techniques to analyze the performance and the dependability of C-RAN architecture. We propose fault tolerant VM allocation strategies that can handle BBU failures, thus improving the system's overall reliability. Based on redundancy techniques, these strategies ensure call recovery through migration to functional BBUs in the case of a BBU failure. In order to evaluate the mutual impact of performance measures on the system's dependability, we develop performability (combination of performance and dependability) Markov Reward Models (MRMs) for the proposed strategies. We use Probabilistic Model Checking (PMC) to check the performability requirements written with Continuous Stochastic Reward Logic (CSRL). The proposed models are implemented and checked using the PRISM model checker, which supports solving MRMs and checking CSRL properties.