Modeling and Analysis for Mobile Computing Systems Based on Petri Nets: A Survey

Mobile computing systems have generated many concerns. Numerous studies have been performed to model and analyze these systems. This paper focuses on the existing modeling and corresponding analyses methods for mobile computing systems based on formal methods, particularly Petri nets. First, this paper refines the characteristics of mobile computing systems into the three dimensions of concurrency, interaction, and mobility and presents several existing formal methods for each dimension. Second, the existing methods for mobile computing systems based on Petri nets are investigated and divided into two categories: models with fixed structures and models with variable structures. To reflect the mobility and dynamic interactions in systems, the former introduces the hierarchy and some special labels, whereas the latter introduces the dynamic structure (concept) to Petri nets. A model of each method is constructed for a single example system, and a detailed discussion and comparison of all discussed methods are provided in terms of their capabilities and related analysis techniques. Finally, ideas are introduced for future directions of modeling and analysis research of mobile computing systems based on Petri nets. This paper provides a comprehensive review of models and analysis techniques for mobile computing systems based on formal methods, especially Petri nets.