VERIFICATION OF THE TRIANGULAR COMMUNICATION GRIDS PROTOCOLS BY INFINITE PETRI NETS

Authors

  • T. R. Shmeleva A. S. Popov National Academy of Telecommunications, Odessa, Ukraine

DOI:

https://doi.org/10.15588/1607-3274-2018-4-3

Keywords:

computing grids, triangular communication structure, infinite Petri net, parametric specification, linear invariant, verification of protocols.

Abstract

Context. Computing and communication grids are a powerful means of increasing the performance and quality of service of modern networks. In two-dimensional grids the basic cell forms are a triangle, a square, and a hexagon. Triangular grids are used in
solving boundary value problems with triangular finite elements, in broadcasting systems and in television. The simplest and most efficient implementations of grids can possess hidden defects and vulnerabilities in terms of secure information exchange. Thus, the
verification of grids is an urgent task.
Objective. The goal of the paper is to construct the models of triangular communication grids in the form of infinite Petri nets and to investigate their properties for proving the protocols (verification) correctness.
Method. Research methods are based on the basics of graph theory, linear algebra, the theoretical foundations of Petri nets, mathematical modeling and simulation.                  Results. A parametric description of the triangular communication grid on the plane, in a direct and a dual form, is constructed. The switching node implements full-duplex transmission and buffering of packets with a limited capacity of the internal buffer. Analytic expressions are obtained for estimating the number of model components. Solving infinite systems of linear equations in parametric form allowed us to prove the invariance of a model of arbitrary size. Invariance is one of the basic properties of the ideal protocol model which determines the safety of the network. The practical significance of the results obtained lies in the construction of safe grid schemes for further software and hardware implementation, which is officially confirmed by the inclusion of triangular grid models in the archive of Petri net models of the University Paris 6 Informatics Laboratory.                                                                                            Conclusions. For the first time, a mathematical model of triangular communication grids with a regular structure and an arbitrary size in the form of infinite Petri nets was constructed for verification of information transmit protocols in grids. The application of the technique for verification of triangular communication structures allows the further development of the infinite Petri nets theory for constructing and investigating models of arbitrary grids with a regular structure.

References

Katunin G. P., Mamchev G. V., Nosov V. I., Shuvalov V.P.

Telekommunikatsionnyye sistemy i seti : Uchebnoye posobiye.

V 3-kh tomakh. Pod red. professora V. P. Shuvalova.

Moscow, Goryachaya liniya. Telekom. Vol. 2: Radiosvyaz’,

radioveshchaniye, televideniye; 4-ye izdaniye, pererabotannoye

i dopolnennoye, 2017, 564 p. ISBN 978-5-9912-0494-1

Zaitsev D. A. Clans of Petri Nets: Verification of protocols

and performance evaluation of networks, LAP LAMBERT

Academic Publishing, 2013, 292 p. ISBN-13: 978-3-659-

-7

Grid and Cloud Computing: Concepts, Methodologies,

Tools and Applications (4 Vol.), Information Resources

Management Association (USA), IGI-Global, 2012,

p. DOI: 10.4018/978-1-4666-0879-5

Lokshin M. G., Shur A. A., Kokorev A. V., Krasnoshchekov

R. A. Seti televizionnogo i zvukovogo OVCH CHM

veshchaniya. Moscow, Radio i svyaz’, 1988, 144 p.

Zaitsev D. A., Zaitsev I. D., Shmeleva T. R. Infinite Petri

Nets: Part 2, Modeling Triangular, Hexagonal, Hypercube

and Hypertorus Structures, Complex Systems, 2017,

Vol. 26, No. 4, pp. 341–371. DOI:

25088/ComplexSystems.26.4.341

Galkin V. A. Tsifrovaya mobil’naya radiosvyaz’: ucheb.

posob. dlya vuzov: [2-ye izd., pererab. i dop.]. Moscow,

Goryachaya liniya – Telekom, 2012, 592 p.

Zaitsev D. A., Zaitsev I. D., Shmeleva T. R. Infinite Petri

Nets: Part 1, Modeling Square Grid Structures, Complex

Systems, 2017, Vol. 26, No. 2, pp. 157-195. DOI:

25088/ComplexSystems.26.2.157

Zaitsev D.A. Verification of Computing Grids with Special

Edge Conditions by Infinite Petri Nets, Automatic

Control and Computer Sciences, 2013, Vol. 47, Issue 7, pp.

-412. DOI: 10.3103/S0146411613070262

Murata T. Petri Nets: Properties, Analysis and Applications,

Proceedings of the IEEE, 1989, Vol. 77, Issue 4, pp.

–580. DOI: 10.1109/5.24143

Berthomieu B., Ribet P.-O. and Vernadat F. The Tool

TINA: Construction of Abstract State Spaces for Petri Nets

and Time Petri Nets, International Journal of Production

Research, 2004, Vol. 42, No. 14, pp. 2741–2756. DOI: 10.

/00207540412331312688

Zaitsev D. A., Zaitsev I. D., Shmeleva T. R. Infinite Petri

Nets: Part 2, Modeling Triangular, Hexagonal, Hypercube

and Hypertorus Structures, Complex Systems, 2017,

Vol. 26, No. 4, pp. 341–371. DOI:

25088/ComplexSystems.26.4.341

Shmeleva T. R. Programmnyy generator modeley Petri

treugol’nykh kommunikatsionnykh reshetok, Sbornik

nauchnykh trudov ONAS im. A.S. Popova, 2016, No. 1,

pp. 82–89.

Shmeleva T. TriangularGrid. Models for the MCC’2016.

Model Checking Contest @ Petri Nets 2016, 6th edition.

Torun, Poland, June 21, 2016

How to Cite

Shmeleva, T. R. (2019). VERIFICATION OF THE TRIANGULAR COMMUNICATION GRIDS PROTOCOLS BY INFINITE PETRI NETS. Radio Electronics, Computer Science, Control, (4). https://doi.org/10.15588/1607-3274-2018-4-3

Issue

Section

Radio electronics and telecommunications