This repository contains PRISM models used to analyse QoS (energy efficiency and service availability) in O-RAN xApps.
The DataMod24 folder contains the model and property files presented in our DataMod24 paper: "Formal Verification as a Key Enabler for Energy Efficiency and Service Availability in Open Radio Access Network (O-RAN)".
ue_dynamics_9_3_cnf1.prism: models 9 UEs and 3 RCs using the cnf1 configuration. Simply change the value of constants in the model for other configurations.ue_dynamics.props: the property file