通过形式化验证实现 O-RAN 能源效率与服务可用性
网络与互联网体系结构
2025-04-22 v1
摘要
随着 Open Radio Access Networks（O-RAN）的不断扩张，AI 驱动的应用（xApps）正越来越多地被部署以增强网络管理。然而，在开发 xApps 而不进行形式化验证风险引入逻辑不一致，尤其是在能源效率和服务可用性之间进行权衡。本文我们认为，在开发之前，对 xApp 模型进行形式分析是 O-RAN 设计过程中的关键早期步骤。使用 PRISM 模型检查器，我们展示了我们的结果为在能源效率和服务可用性之间提供现实感知的阈值提供了见解。尽管我们的模型被简化，但发现 AI 信息化决策可实现更有效的细胞切换策略。我们将形式化验证定位为未来 xApp 开发的必不可少的实践，避免现实应用中的谬误，确保网络高效运行。
关键词
引用
@article{arxiv.2411.03943,
title = {Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification},
author = {Roberto Metere and Kangfeng Ye and Yue Gu and Zhi Zhang and Dalal Alrajeh and Michele Sevegnani and Poonam Yadav},
journal= {arXiv preprint arXiv:2411.03943},
year = {2025}
}
备注
22 pages, 9 figures, 2 tables