Formal Description And Verification Of Mobility Management In Mobile Communication

With the development of digital communication, computer and network technology, mobile communications with its own convenient characteristics shows a momentum for the development in full swing. The purpose of mobile communications is to achieve communication at any time, any place and among any two mobile devices. Compared to the fixed communications systems, its significantly point is: the mobile station's location is constantly changing. This makes mobility management a focal point.Mobility management is achieved through two-tier database structure in location management. All the mobile stations' location information are stored in the two-tier database. With the changing location of mobile stations, the location information in corresponding database must be constantly updated in order to deal with these requests such as calls, data transmissions and so on. The follow-up process originated in the location change of the mobile station is relevant with it's state. If it's moving in attached state, just need perform a location update process in time. And if it's moving in a call state, a handover process is a must to ensure that the call is not interrupted. Then a new location update process is to be performed after the call is end.In this paper, we make a study of the mobility management in mobile communication systems. Using Pi-calculus, we describe the two-tier database schema in GSM. So we get our simplified model. Two important properties which all the mobile communication system must satisfy, mobile station's mobility and system's irrelevance of move, are proposed and given formal description. Then we verify manually that our model satisfies these two properties. So the model is correct. Finally, for further testing the correctness of our model, we use the model checking tools to check the grammar and deadlocks of our description.