Exploring Dependability of Cellular Access Networks Through Formal Methods

Overview & Synopsis

Cellular access networks are essential for modern communication, evolving through successive generations to meet the increasing performance demands. As these networks become more complex, ensuring reliable and uninterrupted operation is a significant challenge, making dependability a fundamental requirement. To address these challenges, various fault-tolerance techniques have been developed to improve system availability and resilience, enabling service continuity even in the case of failure events. Formal methods provide mathematically rigorous techniques for modeling, analyzing, and verifying the dependability of cellular systems. This paper presents a comprehensive survey of formal method applications in dependability analysis for cellular access networks, classifying existing approaches by network generation, modeling framework, and fault-tolerance strategy. Finally, we highlight several open security-related issues that remain open in current cellular access networks, and that guide our ongoing research.