Title :
Formal specification and verification of protocol-based handover in a mobile process
Author_Institution :
Dept. of Inf. Technol., Vietnam Posts & Telecommun. Inst. of Technol., Viet Nam
Abstract :
In a current mobile computing system or future UMTS (universal mobile telecommunications system) environment, some nodes change locations, and are therefore connected to different other nodes at different points in time; cooperation between neighbouring nodes can be described in a way similar to the handover process based on communication protocols. We investigate how to specify a semantic model of protocol-based handover. We specify formally the protocol-based handover using RAISE specification language (RSL), and the RSL specifications are verified by the type checker of the RSL toolset. Finally, we simulate and verify the handover process using XSpin as a model checker for our specifications
Keywords :
asynchronous transfer mode; cellular radio; complete computer programs; formal specification; formal verification; mobile computing; protocols; specification languages; telecommunication computing; ATM-based mobile network; RAISE specification language; UMTS environment; XSpin; communication protocols; formal specification; formal verification; handover process; mobile computing system; mobile process; model checker; protocol-based handover; type checker; universal mobile telecommunications system; 3G mobile communication; Base stations; Electronic mail; Formal specifications; Information technology; Mobile computing; Protocols; Resumes; Specification languages; Telecommunication computing;
Conference_Titel :
ATM (ICATM 2001) and High Speed Intelligent Internet Symposium, 2001. Joint 4th IEEE International Conference on
Conference_Location :
Seoul
Print_ISBN :
0-7803-7093-7
DOI :
10.1109/ICATM.2001.932117
