Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification

Roberto Metere, Kangfeng Ye, Yue Gu, Zhi Zhang, Dalal Alrajeh, Michele Sevegnani, Poonam Yadav

TL;DR

This work addresses the risk of deploying AI-driven xApps in O-RAN without formal verification, focusing on balancing energy efficiency and service availability. It advocates incorporating formal verification early in xApp design and demonstrates this with PRISM-based probabilistic model checking of a dynamic UE management scenario, modelling RCs and UEs as CTMCs and evaluating energy and QoS through CSL properties and rewards. Key findings show that RC capacity and redundancy critically determine energy use and service availability, with configurations enabling standby modes reducing energy while maintaining acceptable QoS, and overly constrained capacity leading to degraded accessibility. The practical impact is approving a formal-verification-first workflow to guide realistic, energy-efficient, and reliable O-RAN deployment, and outlining future work to incorporate mobility, RSRP dynamics, and scalability enhancements for real-world testbeds.

Abstract

As Open Radio Access Networks (O-RAN) continue to expand, AI-driven applications (xApps) are increasingly being deployed enhance network management. However, developing xApps without formal verification risks introducing logical inconsistencies, particularly in balancing energy efficiency and service availability. In this paper, we argue that prior to their development, the formal analysis of xApp models should be a critical early step in the O-RAN design process. Using the PRISM model checker, we demonstrate how our results provide realistic insights into the thresholds between energy efficiency and service availability. While our models are simplified, the findings highlight how AI-informed decisions can enable more effective cell-switching policies. We position formal verification as an essential practice for future xApp development, avoiding fallacies in real-world applications and ensuring networks operate efficiently.

Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification

TL;DR

This work addresses the risk of deploying AI-driven xApps in O-RAN without formal verification, focusing on balancing energy efficiency and service availability. It advocates incorporating formal verification early in xApp design and demonstrates this with PRISM-based probabilistic model checking of a dynamic UE management scenario, modelling RCs and UEs as CTMCs and evaluating energy and QoS through CSL properties and rewards. Key findings show that RC capacity and redundancy critically determine energy use and service availability, with configurations enabling standby modes reducing energy while maintaining acceptable QoS, and overly constrained capacity leading to degraded accessibility. The practical impact is approving a formal-verification-first workflow to guide realistic, energy-efficient, and reliable O-RAN deployment, and outlining future work to incorporate mobility, RSRP dynamics, and scalability enhancements for real-world testbeds.

Abstract

As Open Radio Access Networks (O-RAN) continue to expand, AI-driven applications (xApps) are increasingly being deployed enhance network management. However, developing xApps without formal verification risks introducing logical inconsistencies, particularly in balancing energy efficiency and service availability. In this paper, we argue that prior to their development, the formal analysis of xApp models should be a critical early step in the O-RAN design process. Using the PRISM model checker, we demonstrate how our results provide realistic insights into the thresholds between energy efficiency and service availability. While our models are simplified, the findings highlight how AI-informed decisions can enable more effective cell-switching policies. We position formal verification as an essential practice for future xApp development, avoiding fallacies in real-world applications and ensuring networks operate efficiently.

Paper Structure

This paper contains 15 sections, 3 equations, 9 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Overview of O-RAN
  4. Formal Methods and PRISM
  5. Probabilistic Model Checking
  6. Dynamic Client Management
  7. Modelling Considerations
  8. Formal Model and Analysis
  9. PRISM Model Description
  10. Verification and Evaluation
  11. Configurations.
  12. Power consumption.
  13. Service availability.
  14. Discussions
  15. Conclusion

Figures (9)

  • Figure 1: O-RAN Architecture
  • Figure 2: A scenario with 3 RCs and 9 UEs where their locations are all fixed. The diagram shows one possible connection where all the RCs are on.
  • Figure 3: PRISM module connections and behaviours.
  • Figure 4: The modelling of an RC in PRISM and the snippet for other two RCs are omitted.
  • Figure 5: The modelling of a UE in PRISM and the snippet for other UEs are omitted.
  • ...and 4 more figures