Control-Plane Protocol Interactions in Mobile Networks

摘要: The 3G/4G mobile network is a wireless infrastructure that offers universal coverage and ubiquitous data voice services. It large-scale, global system on par with the Internet. In recent years, demand for access grows exponentially. traffic volume projected to increase three times by 2018, according CISCO estimate. will be further accelerated increasing popularity of smartphones, tablets, wearable devices. However, its control-plane design much more complex many utility functions (e.g., mobility support, radio resource control, device-level security) than Internet counterpart. They communicate one another along dimensions cross layers, (circuit-switched packet-switched) domains, (3G 4G) systems. Despite their significance, correctness verification protocols remains largely unexplored. this dissertation, we examine protocol interactions in networks. We propose CNetVerifier, two-phase signaling diagnosis tool detect problematic both practice. CNetVerifier first performs screening based 3GPP standards via domain-specific model checking, then conducts phone-based empirical validation operational With have uncovered six types troublesome interactions, Such issues span defects slips carriers. Some are caused necessary yet cooperation (i.e., needed but they misbehave), whereas others due independent unnecessary coupled operations not required actually coupled). all result performance penalties or functional incorrectness.We quantify real world impact from end-user’s perspective. conduct two studies essential services users: user Specifically, focus whether improper support) affect accounting (management-plane) roaming users’ negative impacts There lessons learnt our work. First, current networks does honor layering structure which has been strictly examined community well recognize differences domains almost observed anywhere Coupling inter-layer actions leads longer call setup time packet delivery latency usual; CS PS at shared state (RRC) may deprive 4G connectivity; Inconsistent regulations context different systems get users into “out-of-service” tens seconds. Second, management-plane usage accounting) do cooperate each other coordinated manner. For example, suspended while an inter-system handoff 3G→4G) triggered mobility. devices cannot receive any packets until procedure finished (caused hardware limitation, e.g., single radio). still pay lost during procedure. Third, diversity demands service (or even most important service) always granted higher serving priority service. discover not-well-justified principle serious up 83.4% throughput slumps applications aborted) missed incoming call)