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

TL;DR

This paper emphasizes the importance of formal verification in developing AI-driven xApps for O-RAN to ensure energy efficiency and service availability, using the PRISM model checker for analysis.

Contribution

It introduces a formal verification approach for xApps in O-RAN, demonstrating how model checking can inform better cell-switching policies and network management.

Findings

Formal analysis provides realistic thresholds for energy and service trade-offs.

Model checking helps identify logical inconsistencies in xApp design.

AI-informed policies can improve network efficiency.

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.