VERIFICATION OF THE TRIANGULAR COMMUNICATION GRIDS PROTOCOLS BY INFINITE PETRI NETS
DOI:
https://doi.org/10.15588/1607-3274-2018-4-3Keywords:
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
Downloads
How to Cite
Issue
Section
License
Copyright (c) 2019 T. R. Shmeleva
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
Creative Commons Licensing Notifications in the Copyright Notices
The journal allows the authors to hold the copyright without restrictions and to retain publishing rights without restrictions.
The journal allows readers to read, download, copy, distribute, print, search, or link to the full texts of its articles.
The journal allows to reuse and remixing of its content, in accordance with a Creative Commons license СС BY -SA.
Authors who publish with this journal agree to the following terms:
-
Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License CC BY-SA that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
-
Authors are able to enter into separate, additional contractual arrangements for the non-exclusive distribution of the journal's published version of the work (e.g., post it to an institutional repository or publish it in a book), with an acknowledgement of its initial publication in this journal.
-
Authors are permitted and encouraged to post their work online (e.g., in institutional repositories or on their website) prior to and during the submission process, as it can lead to productive exchanges, as well as earlier and greater citation of published work.
