TY - JOUR
T1 - Detecting problematic control-plane protocol interactions in mobile networks
AU - Tu, Guan Hua
AU - Li, Yuanjie
AU - Peng, Chunyi
AU - Li, Chi-Yu
AU - Lu, Songwu
N1 - Publisher Copyright:
© 1993-2012 IEEE.
PY - 2016/4
Y1 - 2016/4
N2 - The control-plane protocols in 3G/4G mobile networks communicate with each other, and provide a rich set of control functions, such as radio resource control, mobility support, connectivity management, to name a few. Despite their significance, the problem of verifying protocol correctness remains largely unaddressed. In this paper, we examine control-plane protocol interactions in mobile networks. We propose CNetVerifier, a two-phase signaling diagnosis tool to detect problematic interactions in both design and practice. CNetVerifier first performs protocol screening based on 3GPP standards via domain-specific model checking, and then conducts phone-based empirical validation in operational 3G/4G networks. With CNetVerifier, we have uncovered seven types of troublesome interactions, along three dimensions of cross (protocol) layers, cross (circuit-switched and packet-switched) domains, and cross (3G and 4G) systems. Some are caused by necessary yet problematic cooperation (i.e., protocol interactions are needed but they misbehave), whereas others are due to independent yet unnecessary coupled operations (i.e., protocols interactions are not required but actually coupled). These instances span both design defects in 3GPP standards and operational slips by carriers and vendors. They all result in performance penalties or functional incorrectness. We deduce root causes, present empirical results, propose solutions, and summarize learned lessons.
AB - The control-plane protocols in 3G/4G mobile networks communicate with each other, and provide a rich set of control functions, such as radio resource control, mobility support, connectivity management, to name a few. Despite their significance, the problem of verifying protocol correctness remains largely unaddressed. In this paper, we examine control-plane protocol interactions in mobile networks. We propose CNetVerifier, a two-phase signaling diagnosis tool to detect problematic interactions in both design and practice. CNetVerifier first performs protocol screening based on 3GPP standards via domain-specific model checking, and then conducts phone-based empirical validation in operational 3G/4G networks. With CNetVerifier, we have uncovered seven types of troublesome interactions, along three dimensions of cross (protocol) layers, cross (circuit-switched and packet-switched) domains, and cross (3G and 4G) systems. Some are caused by necessary yet problematic cooperation (i.e., protocol interactions are needed but they misbehave), whereas others are due to independent yet unnecessary coupled operations (i.e., protocols interactions are not required but actually coupled). These instances span both design defects in 3GPP standards and operational slips by carriers and vendors. They all result in performance penalties or functional incorrectness. We deduce root causes, present empirical results, propose solutions, and summarize learned lessons.
KW - Control-plane
KW - mobile networks
KW - protocol verification
UR - http://www.scopus.com/inward/record.url?scp=84925060942&partnerID=8YFLogxK
U2 - 10.1109/TNET.2015.2404336
DO - 10.1109/TNET.2015.2404336
M3 - Article
AN - SCOPUS:84925060942
SN - 1063-6692
VL - 24
SP - 1209
EP - 1222
JO - IEEE/ACM Transactions on Networking
JF - IEEE/ACM Transactions on Networking
IS - 2
M1 - 7060732
ER -