Formal specification and verification of protocol-based handover in a mobile process

Author

Cong Vinh, Phan

Author_Institution

Dept. of Inf. Technol., Vietnam Posts & Telecommun. Inst. of Technol., Viet Nam

fYear

2001

fDate

2001

Firstpage

354

Lastpage

358

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/ICATM.2001.932117

Filename

932117