Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra

Dmitry A. Zaitsev; Tatiana R. Shmeleva; Jan Friso Groote

doi:10.1109/JAS.2019.1911486

Volume 6 Issue 3

May 2019

IEEE/CAA Journal of Automatica Sinica

JCR Impact Factor: 15.3, Top 1 (SCI Q1)

CiteScore: 23.5, Top 2% (Q1)
Google Scholar h5-index: 77， TOP 5

Turn off MathJax

Article Contents

Article Navigation > IEEE/CAA Journal of Automatica Sinica > 2019 > 6(3): 733-742

Dmitry A. Zaitsev, Tatiana R. Shmeleva and Jan Friso Groote, "Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra," IEEE/CAA J. Autom. Sinica, vol. 6, no. 3, pp. 733-742, May 2019. doi: 10.1109/JAS.2019.1911486

Citation:

Dmitry A. Zaitsev, Tatiana R. Shmeleva and Jan Friso Groote, "Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra," IEEE/CAA J. Autom. Sinica, vol. 6, no. 3, pp. 733-742, May 2019. doi: 10.1109/JAS.2019.1911486

Citation:

PDF( 4505 KB)

Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra

doi: 10.1109/JAS.2019.1911486

1.
Vistula University, Warsaw 02-787, Poland
2.
A.S. Popov Odessa National Academy of Telecommunications, Odessa 65023, Ukrain
3.
Eindhoven University of Technology, PO Box 513, 5600 MB Eindhoven, The Netherlands

Funds: This work was supported in part by NATO(ICS.NUKR.CLG982689)

More Information

Author Bio:
Dmitry A. Zaitsev (M'10-SM'11) received an Eng. degree in applied mathematics from Donetsk Polytechnic Institute, Donetsk, Ukraine, in 1986, a Ph.D. degree in automated control from the Kiev Institute of Cybernetics, Kiev, Ukraine in 1991, and a Dr.Sc. degree in telecommunications from the Odessa National Academy of Telecommunications, Odessa, Ukraine, in 2006
He is a Professor of Computer Engineering at the International Humanitarian University, Odessa, Ukraine since 2009 and also a Professor of Computer Science at Vistula University, Warsaw, Poland since 2014. He developed the analysis of infinite Petri nets with regular structure, the decomposition of Petri nets in clans, and a method of synthesis of fuzzy logic functions given by tables. His current research interests include Petri net theory and its application in networking, production control, and computing. Recently he has been a co-director in Austria-Ukraine, China-Ukraine, and Slovakia-Ukraine research projects. He developed small universal Petri nets, the analysis of infinite Petri nets with a regular structure, the decomposition of Petri nets in clans, and the method of synthesis of fuzzy logic function given by tables. He designed the Opera-Topaz system for production control, models of protocols and networking technologies such as TCP, BGP, IOTP, MPLS, Bluetooth and PBB. Finally, he provided an implementation of the networking protocols E6 for the Linux kernel. He is a Senior Member of ACM. (e-mail: daze@acm.org)

Tatiana R. Shmeleva received an Eng. degree in applied mathematics from the Moscow Railroad Engineering Institute in 1990, a Ph.D. degree in telecommunications from the Odessa National Academy of Telecommunications, Ukraine, in 2008, and an associate professor diploma of the Switching Systems department from the Odessa National Academy of Telecommunications, Ukraine, in 2011. T. R. Shmeleva is the author of more than 80 papers and chapters published in journals, books, and conference proceedings. Her research interest is Petri net theory and its application in networking, especially in verifications of protocols, and performance evaluation. She developed an analysis of infinite Petri nets with regular structure and reenterable colored Petri net models of networks. Since 2005, she has been with the A.S. Popov Odessa National Academy of Telecommunications, where she is currently an Associate Professor in the Switching Systems Department. Tatiana is a member of SIAM. (e-mail:t.shmeleva@onat.edu.ua)

Jan Friso Groote is a Dutch computer scientist. Groote studied computer science at Twente University obtaining his master's degree in 1988 under supervision of prof. Ed Brinksma. He obtained his PhD thesis in 1991 under Prof. Jan Bergstra and Prof. Jos Baeten at the University of Amsterdam, while working at the Centre for Mathematics and Computer Science in Amsterdam. He contributed to structural operational semantics and verification technology. His particular contributions include the tyft/tyxt format for operational rules, the first algorithm to determine branching bisimulation and the cones and foci method to prove correctness of protocols and distributed algorithms. He is the founding father of the process modelling language and analysis tool sets muCRL and mCRL2. His current interest lies in the improvement of the quality of software by modeling via domain specific languages of which the quality is guaranteed using automatic verification. Since 1998 he has worked as a Full Professor in verification technology at Eindhoven University of Technology. He is a member of the ACM. (e-mail: j.f.groote@tue.nl)
Corresponding author: Dmitry A. Zaitsev, email: daze@acm.org
Received Date: 2018-11-08
Revised Date: 2019-01-13
Accepted Date: 2019-01-20

Abstract

Abstract

A model of a hypertorus communication grid has been constructed in the form of an infinite Petri net. A grid cell represents either a packet switching device or a bioplast cell. A parametric expression is obtained to allow a finite specification of an infinite Petri net. To prove properties of an ideal communication protocol, we derive an infinite Diophantine system of equations from it, which is subsequently solved. Then we present the programs htgen and ht-mcrl2-gen, developed in the C language, which generate Petri net and process algebra models of a hypertorus with a given number of dimensions and grid size. These are the inputs for the respective modeling tools Tina and mCRL2, which provide model visualization, step simulation, state space generation and reduction, and structural analysis techniques. Benchmarks to compare the two approaches are obtained. An ad-hoc induction-like technique on invariants, obtained for a series of generated models, allows the calculation of a solution of the Diophantine system in a parametric form. It is proven that the basic solutions of the infinite system have been found and that the infinite Petri net is bounded and conservative. Some remarks regarding liveness and liveness enforcing techniques are also presented.
- Computing grid,
- conservativeness,
- deadlock,
- hypertorus,
- infinite Petri nets,
- process algebra,
- systems biology

FullText(HTML)

References(31)

References

[1]	D. A. Zaitsev, I. D. Zaitsev, and T. R. Shmeleva, "Infinite petri nets: part 1, modeling square grid structures, " Complex Systems, vol. 26, no. 2, pp. 157-195, 2017. doi: 10.25088/ComplexSystems
[2]	D. A. Zaitsev, I. D. Zaitsev and T. R. Shmeleva, "Infinite petri nets: part 2, modeling square grid structures, " Complex Systems, vol. 26, no. 4, pp. 341-371, 2017. doi: 10.25088/ComplexSystems
[3]	D. A. Zaitsev and T. R. Shmeleva, "Verification of hypercube communication structures via parametric Petri nets, " Cybernetics and Systems Analysis, vol. 46, no. 1, pp. 105-114, 2010. doi: 10.1007/s10559-010-9189-y
[4]	D. A. Zaitsev, "Verification of computing grids with special edge conditions by infinite petri nets, " Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 403-412, 2013. doi: 10.3103/S0146411613070262
[5]	T. R. Shmeleva, D. A. Zaitsev, and I. D. Zaitsev, "Verification of square communication grid protocols via infinite Petri nets, " in Proc. of MESM 10th Middle Eastern Simulation Multiconference, 2009, 53-59.
[6]	S. Cheng, W. Zhong, and K. E. Isaacs, and K. Mueller, "Visualizing the topology and data traffic of multi-dimensional torus interconnect networks, " IEEE Access, 2018.
[7]	N. P. Preve (Ed.), Grid Computing: Towards a Global Interconnected Infrastructure, Springer, 2011.
[8]	D. Gilbert, M. Heiner, F. Liu, and N. Saunders, "Colouring space - a coloured framework for spatial modelling in systems biology, " in Proc. Conf. Petri Nets, Milano, Springer, LNCS, vol. 7927, pp. 230-249, June 2013.
[9]	K. Miyamoto, Plasma Physics and Controlled Nuclear Fusion. Springer, 2005.
[10]	L. V. Belevtsov and A. A. Kostikov, "Influence of grain properties on the Abrikosov vortices interaction with Josephson junction, " Journal of Low Temperature Physics, vol. 139, no. 1, pp. 11-19, 2005. http://www.wanfangdata.com.cn/details/detail.do?_type=perio&id=9a05b5a41cf3fd4db3a66eec0fa213d3
[11]	B. Berthomieu, O.-P. Ribet, and F. Vernadat, "The tool TINA-construction of abstract state space for Petri nets and time Petri nets, " Int. J. Prod. Res., vol. 42, no. 14, pp. 2741-2756, 2004. doi: 10.1080/00207540412331312688
[12]	B. Berthomieu et al., "Tina: Time Petri Net Analyser, " LAAS, 2019 [Online]. Available: http:/projects.laas/fr/tina
[13]	D. A. Zaitsev, "Software of Dmitry Zaitsev, " GitHub, 2019 [Online]. Available: https://github.com/dazeorgacm/
[14]	J. F. Groote and M. R. Mousavi. Modeling and Analysis of Communicating Systems. The MIT Press, 2014.
[15]	J. F. Groote et al, "mCRL2: Analysing System Behaviour, " TU/e, 2019.[Online]. Available: https://www.mcrl2.org/
[16]	T. A. N. Engels, J. F. Groote, M. J. van Weerdenburg, and T. A. C. Willemse, "Search algorithms for automated validation, " Journal of Logic and Algebraic Programming, vol. 78, no. 4, pp. 274-287, 2009. doi: 10.1016/j.jlap.2008.11.003
[17]	D. A. Zaitsev, "A generalized neighborhood for cellular automata, " Theoretical Computer Science, vol. 666, pp. 21-35, March 2017.
[18]	G. Berthelot and R. Terrat, "Petri nets theory for the correctness of protocols, " IEEE Trans. on Communications, vol. 30, no. 12, pp. 2497-2505, 1982. doi: 10.1109/TCOM.1982.1095452
[19]	M. Diaz, "Modelling and analysis of communication and cooperation protocols using petri net based model, " Computer Networks, no. 6. pp. 419-441, 1982.
[20]	T. Murata, "Petri Nets: Properties, Analysis and Applications, " Proc. of the IEEE, vol. 77, no. 4, pp. 541-580, 1989. doi: 10.1109/5.24143
[21]	Z. W. Li and M. C. Zhou, Deadlock Resolution in Automated Manufacturing Systems, Springer, 2010.
[22]	D. A. Zaitsev, "Decomposition of petri nets, " Cybernetics and Systems Analysis, vol. 40, no. 5, pp. 739-746, 2004. doi: 10.1007/s10559-005-0012-0
[23]	J. Ye, M. C. Zhou, Z. Li, and A. Al-Ahmari, "Structural Decomposition and Decentralized Control of Petri Nets, " IEEE Transactions on Systems, Man, and Cybernetics: Systems, pp. 1-10, DOI: 10.1109/TSMC.2017.2703950,July2017.
[24]	D. A. Zaitsev and A. I. Sleptsov, "State Equations and Equivalent Transformation for Timed Petri Nets, " Cybernetics and Systems Analysis, vol. 33, no. 5, pp. 659-672, 1997. doi: 10.1007/BF02667189
[25]	J. Luo, H. Ni, W. Wu, S. Wang, and M. C. Zhou, "Simultaneous reduction of petri nets and linear constraints for efficient supervisor synthesis, " IEEE Trans. on Automatic Control, vol. 60, no. 1, pp. 88-103, Jan. 2015.
[26]	N. Wu, M. C. Zhou, and G. Hu, "Petri net modeling and one-step look-ahead maximally permissive deadlock control of automated manufacturing systems, " ACM Transactions on Embedded Computing Systems, vol. 12, no. 1, pp. 10: 1-10: 23, Jan. 2013.
[27]	H. Liu, K. Xing, W. Wu, M. C. Zhou, and H. Zou, "Deadlock prevention for flexible manufacturing systems via controllable siphon basis of petri nets, " IEEE Trans. Systems, Man, and Cybernetics: Systems, vol. 45, no. 3, pp. 519-529, Mar. 2015.
[28]	D. You, S. Wang, and M. C. Zhou, "Synthesis of monitor-based liveness-enforcing supervisors for S3PR with $xi $-resources, " IEEE Trans. Systems, Man, and Cybernetics: Systems, vol. 45, no. 6, pp. 967-975, June 2015.
[29]	H. Chen, N. Wu, and M. C. Zhou, "A novel method for deadlock prevention of AMS by using resource-oriented petri nets, " Information Sciences, vol. 363, pp. 178-189, Oct. 2016.
[30]	D. A. Zaitsev, T. R. Shmeleva, W. Retschitzegger, and B. Proll, "Security of grid structures under disguised traffic attacks, " Cluster Computing, vol. 19, no. 3, pp. 1183-1200, 2016. doi: 10.1007/s10586-016-0582-9
[31]	F. Kordon et al., "Model Checking Contest, " Sorbonne, 2019 [Online]. Available: https://mcc.lip6.fr

Supplements(0)

Cited By

Proportional views

Proportional views

通讯作者: 陈斌, bchen63@163.com

1.
沈阳化工大学材料科学与工程学院沈阳 110142

Figures(8) / Tables(2)

Get Citation

PDF

XML

Article Metrics

Article views (1525) PDF downloads(45)

Verification of Hypertorus Communication Grids by Infinite Petri Nets and Process Algebra

doi: 10.1109/JAS.2019.1911486

Abstract

References

Proportional views

Catalog

通讯作者: 陈斌, bchen63@163.com

Article Metrics

Export File

Citation

Format

Content