Formal Modelling and Analysis of the O-RAN O2 Interface in Alloy: Implications for NTN Deployment (to appear)

Abstract

Open Radio Access Networks (O-RAN) aims to transition telecommunication networks from vendor-specific hardware to open, virtualised control architectures. As interest grows in deploying O-RAN in non-terrestrial networks (NTNs), understanding the robustness of its protocol specifications becomes critical.

This paper reports on the formal modelling of the stable O2 O-RAN interface specification using the Alloy modelling language. We encode ten representative operational scenarios from the O2 specification and formalise safety and liveness properties relevant to deployment constraints. Bounded model checking reveals several classes of specification weaknesses, including underconstrained pre/post conditions, ambiguous sequencing of protocol steps, and conflicting simultaneous triggers that permit inconsistent system states or violate intended progress conditions.