Verification of the hexagonal communication grid by infinite Petri nets
DOI:
https://doi.org/10.30837/rt.2018.3.194.07Keywords:
computing grids, hexagonal communication structure, infinite Petri net, direct parametric specification, linear invariant, verification of protocolsAbstract
A formal direct parametric description of the hexagonal grid model with side k is constructed according to the specified grid composition rules. A system of linear equations is constructed for finding invariants of positions on the basis of a direct description of the model. A method for calculating linear invariants of infinite Petri nets with a regular structure for an open hexagonal grid is used, and a solution of a system of linear equations in parametric form is obtained. It is proved that the hexagonal grid model, represented in the form of infinite Petri net, is a p-invariant Petri net for an arbitrary natural number k and has the boundedness and conservativeness properties. Communication grids, representing the implementation of the studied model, can be constructed using devices with limited capacity without overflow.References
Телекоммуникационные системы и сети : учеб. пособие : в 3 т. / Г. П. Катунин, В. Н. Попантонопуло, В. П. Шувалов, Г. В. Мамчев. – 2-е изд., испр. и доп. – Москва : Горячая линия – Телеком, 2004 ; 2005.
Sayandev Mukherjee. Analytical Modeling of Heterogeneous:Cellular Networks Geometry, Coverage, and Capacity. – Cambridge University Press, 2014. – 180 p.
Kolchin A.V., Letichevsky A.A., Potienko S.V., Peschanenko V.S.. Overview of modern systems and verification methods of formal models // Problems of Programming. 2012. – No. 4. – Р. 75-88.
Shmeleva T.R., Zaitsev D.A., Zaitsev I.D. Analysis of Square Communication Grids via Infinite Petri Nets // Transactions of Odessa National Academy of Telecommunication. – 2009. – no. 1. – Р. 27–35.
Zaitsev D.A., Zaitsev I.D., Shmeleva T.R. Infinite Petri Nets: Part 1, Modeling Square Grid Structures // Complex Systems. – 2017. – 26(2). – Р. 157-195.
Murata T. Petri Nets: Properties, Analysis and Applications // Proceedings of the IEEE. – 1989. – 77(4). – p. 541–580.
Berthelot G., Terrat R. Petri Nets Theory for the Correctness of Protocols // IEEE Trans. on Communications, no. 12, 1982, vol. 30, p. 2497-2505.
Zaitsev D.A. Verification of Computing Grids with Special Edge Conditions by Infinite Petri Nets // Automatic Control and Computer Sciences. – 2013. – Vol. 47, N 7. – Р. 403-412.
Шмелёва Т.Р. Параметрическая спецификация открытой шестиугольной
решетки // 71 НТ конферен-ция ОНАС, декабрь 6-8, 2016. – Одесса, 2016. – С. 65-68.
Downloads
Published
How to Cite
Issue
Section
License
Authors who publish with this journal agree to the following terms:
1. Authors retain copyright and grant the journal right of first publication with the work simultaneously licensed under a Creative Commons Attribution License that allows others to share the work with an acknowledgement of the work's authorship and initial publication in this journal.
2. 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.
3. 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 (See The Effect of Open Access).