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

被引:7
作者
Yang, Ru [1 ]
Ding, Zhijun [2 ]
Jiang, Changjun [2 ]
Zhou, MengChu [3 ,4 ,5 ]
机构
[1] Shanghai Normal Univ, Dept Comp Sci & Technol, Shanghai 200234, Peoples R China
[2] Tongji Univ, Dept Comp Sci & Technol, Key Lab Embedded Syst & Serv Comp, Minist Educ, Shanghai 201804, Peoples R China
[3] Macau Univ Sci & Technol, Macao Inst Syst Engn, Macau 999078, Peoples R China
[4] Macau Univ Sci & Technol, Collaborat Lab Intelligent Sci & Syst, Macau 999078, Peoples R China
[5] New Jersey Inst Technol, Dept Elect & Comp Engn, Newark, NJ 07102 USA
基金
中国国家自然科学基金;
关键词
Analytical models; Virtual private networks; Interactive systems; Petri nets; Data models; Task analysis; Mobile handsets; Mobile interactive system; property analysis; formal model; discrete event system; SECURITY;
D O I
10.1109/TASE.2022.3206999
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
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.
引用
收藏
页码:2479 / 2491
页数:13
相关论文
共 48 条
[1]  
Captarencu OO, 2012, LECT NOTES BUS INF P, V112, P486
[2]  
Chang L., 2008, P WORKSH PETR NETS D, P132
[3]   Modeling and performance evaluation of supply chains using batch deterministic and stochastic Petri nets [J].
Chen, HX ;
Amodeo, L ;
Chu, F ;
Labadi, K .
IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2005, 2 (02) :132-144
[4]   Automatic Composition of Semantic Web Services Based on Fuzzy Predicate Petri Nets [J].
Cheng, Jiujun ;
Liu, Cong ;
Zhou, MengChu ;
Zeng, Qingtian ;
Yla-Jaaski, Antti .
IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2015, 12 (02) :680-689
[5]  
Cristini F., 2012, LECT NOTES COMPUT SC, P348, DOI DOI 10.1007/978-3-642-31131-4
[6]   Mobility-Aware Service Composition in Mobile Communities [J].
Deng, Shuiguang ;
Huang, Longtao ;
Taheri, Javid ;
Yin, Jianwei ;
Zhou, MengChu ;
Zomaya, Albert Y. .
IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2017, 47 (03) :555-568
[7]   Variable Petri Nets for Mobility [J].
Ding, Zhijun ;
Yang, Ru ;
Cui, Puwen ;
Zhou, MengChu ;
Jiang, Changjun .
IEEE TRANSACTIONS ON SYSTEMS MAN CYBERNETICS-SYSTEMS, 2022, 52 (08) :4784-4797
[8]   Modeling and Analysis for Mobile Computing Systems Based on Petri Nets: A Survey [J].
Ding, Zhijun ;
Yang, Ru .
IEEE ACCESS, 2018, 6 :68038-68056
[9]   Structural Place Invariants for Analyzing the Behavioral Properties of Nested Petri Nets [J].
Dworzanski, Leonid W. ;
Lomazova, Irina A. .
APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY, PETRI NETS 2016, 2016, 9698 :325-344
[10]  
Ek S., 2021, 2021 IEEE INT C PERV, P1, DOI [DOI 10.1109/PERCOM50583.2021.9439129, 10.1109/percom50583.2021.9439129]