Modeling and Analysis of Three Properties of Mobile Interactive Systems Based on Variable Petri Nets

TL;DR

This paper presents a novel Petri net-based modeling approach to analyze key properties like connectivity, soundness, and data validity in mobile interactive systems, addressing challenges posed by mobility and disconnections.

Contribution

It introduces a VPN-based modeling and analysis method for critical properties of mobile systems, demonstrated through a practical mobile payment case study.

Findings

Effective analysis of system connectivity, soundness, and data validity.

Successful application to a mobile payment system case study.

Validation of the proposed VPN-based modeling approach.

Abstract

Due to the mobility and frequent disconnections, the correctness of mobile interaction systems, such as mobile robot systems and mobile payment systems, are often difficult to analyze. This paper introduces three critical properties of systems, called system connectivity, interaction soundness and data validity, and presents a related modeling and analysis method, based on a kind of Petri nets called VPN. For a given system, a model including component nets and interaction structure nets is constructed by using VPNs. The component net describes the internal process of each component, while the interaction structure net reflects the dynamic interaction between components. Based on this model, three properties are defined and analyzed. The case study of a practical mobile payment system shows the effectiveness of the proposed method.