Guardado en:
| Autores principales: | , , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2411.03943 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917990249791488 |
|---|---|
| author | Metere, Roberto Ye, Kangfeng Gu, Yue Zhang, Zhi Alrajeh, Dalal Sevegnani, Michele Yadav, Poonam |
| author_facet | Metere, Roberto Ye, Kangfeng Gu, Yue Zhang, Zhi Alrajeh, Dalal Sevegnani, Michele Yadav, Poonam |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_03943 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification Metere, Roberto Ye, Kangfeng Gu, Yue Zhang, Zhi Alrajeh, Dalal Sevegnani, Michele Yadav, Poonam Networking and Internet Architecture 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. |
| title | Towards Achieving Energy Efficiency and Service Availability in O-RAN via Formal Verification |
| topic | Networking and Internet Architecture |
| url | https://arxiv.org/abs/2411.03943 |