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.

翻译：随着开放式无线接入网络（O-RAN）的持续扩展，基于人工智能的应用（xApps）正日益广泛地部署以增强网络管理。然而，未经形式化验证而开发xApps可能引入逻辑不一致性，尤其在平衡能效与服务可用性方面。本文主张，在xApps开发之前，对其模型进行形式化分析应成为O-RAN设计流程中至关重要的早期步骤。通过使用PRISM模型检测器，我们展示了研究结果如何为能效与服务可用性之间的阈值提供现实性见解。尽管我们的模型经过简化，但研究结果凸显了基于人工智能的决策如何能够实现更有效的小区切换策略。我们将形式化验证定位为未来xApp开发中必不可少的一环，旨在避免实际应用中的逻辑谬误，并确保网络高效运行。