Formal Approaches to SMS Service Based on Pi Calculus

With the rapid evolution of mobile communication technology, the short message service (SMS) is the most important and essential operating business. The Pi calculus is a process algebra that describes the concurrent, dynamic and mobile systems. This paper depicts the behaviors of SMS service based on Pi calculus, including the formal description of fixed and mobile area. The formal model for SMS service is introduced and the storage-transmit mechanisms are discussed. The mobility features are represented with Pi calculus that the mobile process is controlled by switching the channel and the moving user still accurately receives any message. The formalizations can be used as a basis for future research on other mobile computing or wireless communication.