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

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 servic...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-11
Main Authors: Metere, Roberto, Ye, Kangfeng, Gu, Yue, Zhang, Zhi, Dalal Alrajeh, Sevegnani, Michele, Yadav, Poonam
Format: Article
Language:English
Subjects:
Availability
Verification
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422