An Approach for Modeling and Analyzing Code Mobility

Code mobility provides a flexible paradigm for building high performance mobile computing systems. Because code mobility can cause dynamic configuration of system structures in mobile computing systems, assuring design quality of the system is challenge. Formal specification and analysis provide a rigorous way to ensure system requirements are correctly designed. In this paper, we first introduce the formalism developed based on high level Petri nets and a communication channel mechanism for modeling mobile computing systems specifically code mobility. The formalism has the expressive capacity to naturally model mobile computing systems, and easily define mobility and mobile communication properties in the system. Then we model three representative styles of code mobility in mobile computing systems using the formalism. The formal models developed in this paper provide a solid foundation for formal analysis of code mobility. The formal analysis approach used for analyzing the code mobility models is illustrated via model checking the code mobility models using symbolic model checking tool NuSMV. Through successfully modeling and model checking the code mobility, the paper demonstrates that formal specification and modeling checking provide an effective and efficient way to ensure the design quality of mobile computing systems.