QoS Protocol Verification using Petri-Net for Seamless Mobility in a Ubiquitous Environment: A Case Study

Ubiquitous computing is a worthy environment for autonomic/pervasive computing between users and devices or between devices and devices. To realize ubiquitous computing, supporting seamless mobility ensures continuous services during inter-networking movement without meddling users. For seamless mobility in a heterogeneous networking environment, an adequate service/network configuration is necessary in accordance with the given environment. We developed the middleware, assisting to decrease human effort for application implementation and to guarantee interoperability for effective sustaining. A protocol of QoS (quality of service) NSLP (NSIS Signaling Layer Protocol) with advance resource reservation is modeled during the development process; furthermore, the protocol verification prior to be implemented ensures the correctness of the protocol and additionally reduces risks from ambiguous designs. In this paper, we present the case-study of QoS protocol verification utilizing Petri-Net as one of well-known methods; for seamless mobility, the verified QoS protocol can guarantee service quality and effective use of resources.