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

VERIFICATION OF THE TRIANGULAR COMMUNICATION GRIDS PROTOCOLS BY INFINITE PETRI NETS

T. R. Shmeleva

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.


Keywords


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

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


GOST Style Citations


1. Телекоммуникационные системы и сети: Учебное по-
собие. В 3-х томах / [Под ред. профессора В. П. Шува-
лова]. – М. : Горячая линия – Телеком. – Т. 2: Радио-
связь, радиовещание, телевидение / [Катунин Г. П.,
Мамчев Г. В., Носов В. И., Шувалов В. П.]; 4-е издание,
переработанное и дополненное, 2017. – 564 с. ISBN
978-5-9912-0494-1
2. Zaitsev D. A. Clans of Petri Nets: Verification of protocols
and performance evaluation of networks / D. A. Zaitsev. –
LAP LAMBERT Academic Publishing, 2013. – 292 p.
ISBN-13: 978-3-659-42228-7
3. Grid and Cloud Computing: Concepts, Methodologies,
Tools and Applications / [Information Resources Management
Association (USA)]. – IGI-Global, 2012. – 2134 p.
DOI: 10.4018/978-1-4666-0879-5
4. Сети телевизионного и звукового ОВЧ ЧМ вещания /
[М. Г. Локшин, А. А. Шур, А. В. Кокорев, Р. А. Крас-
нощеков]. – М : Радио и связь, 1988. – 144 с.
5. Zaitsev D. A. Infinite Petri Nets: Infinite Petri Nets: Part 2,
Modeling Triangular, Hexagonal, Hypercube and Hypertorus
Structures / D. A. Zaitsev, I. D. Zaitsev, T. R. Shmeleva
// Complex Systems. – 2017. – Vol. 26, № 4. – P. 341–371.
DOI: 10.25088/ComplexSystems. 26.4.341
6. Галкин В. А. Цифровая мобильная радиосвязь: учеб.
пособ. для вузов / В. А. Галкин: [2-е изд., перераб. и
доп.]. – М. : Горячая линия – Телеком, 2012. – 592 с.

7. Zaitsev D. A. Infinite Petri Nets: Part 1, Modeling Square
Grid Structures / D. A. Zaitsev, I. D. Zaitsev, T. R. Shmeleva
// Complex Systems. – 2017. – Vol. 26, № 2. – P. 157–
195. DOI: 10.25088/ComplexSystems.26.2.157
8. Zaitsev D.A. Verification of Computing Grids with Special
Edge Conditions by Infinite Petri Nets / D. A. Zaitsev
// Automatic Control and Computer Sciences. – 2013. –
Vol. 47, Issue 7. – P. 403–412. DOI:
10.3103/S0146411613070262
9. Murata T. Petri Nets: Properties, Analysis and Applications
/ T. Murata // Proceedings of the IEEE, 1989. – Vol. 77, Issue
4. – P. 541–580. DOI: 10.1109/5.24143
10. Berthomieu B. The Tool TINA: Construction of Abstract
State Spaces for Petri Nets and Time Petri Nets / B. Berthomieu,
P.-O. Ribet, F. Vernadat // International Journal of
Production Research. – 2004. – Vol. 42, № 14. – P. 2741–
2756. DOI: 10.1080/00207540412331312688
11. Zaitsev D. A. Infinite Petri Nets: Part 2, Modeling Triangular,
Hexagonal, Hypercube and Hypertorus Structures /
D. A. Zaitsev, I. D. Zaitsev, T. R. Shmeleva // Complex
Systems. – 2017. – Vol. 26, № 4. – P. 341–371. DOI:
10.25088/ComplexSystems.26.4.341
12. Шмелева Т.Р. Программный генератор моделей Петри
треугольных коммуникационных решеток / Т. Р. Шме-
лева // Сборник научных трудов ОНАС им. А. С. Попо-
ва. – 2016. – № 1. – С. 82–89.
13. Shmeleva T. TriangularGrid [Models for the MCC’2016] /
T. Shmeleva // Model Checking Contest @ Petri Nets
2016, 6th edition, Torun, Poland, June 21 2016. – Torun,
2016.







Copyright (c) 2019 T. R. Shmeleva

Creative Commons License
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

Address of the journal editorial office:
Editorial office of the journal «Radio Electronics, Computer Science, Control»,
National University "Zaporizhzhia Polytechnic", 
Zhukovskogo street, 64, Zaporizhzhia, 69063, Ukraine. 
Telephone: +38-061-769-82-96 – the Editing and Publishing Department.
E-mail: rvv@zntu.edu.ua

The reference to the journal is obligatory in the cases of complete or partial use of its materials.