Applying Infinite Petri Nets to the Cybersecurity of Intelligent Networks, Grids and Clouds

Correctness of networking protocols represents the principal requirement of cybersecurity. Correctness of protocols is established via the procedures of their verification. A classical communication system includes a pair of interacting systems. Recent developments of computing and communication grids for radio broadcasting, cellular networks, communication subsystems of supercomputers, specialized grids for numerical methods and networks on chips require verification of protocols for any number of devices. For analysis of computing and communication grid structures, a new class of infinite Petri nets has been introduced and studied for more than 10 years. Infinite Petri nets were also applied for simulating cellular automata. Rectangular, triangular and hexagonal grids on plane, hyper cube and hyper torus in multidimensional space have been considered. Composing and solving in parametric form infinite Diophantine systems of linear equations allowed us to prove the protocol properties for any grid size and any number of dimensions. Software generators of infinite Petri net models have been developed. Special classes of graphs, such as a graph of packet transmission directions and a graph of blockings, have been introduced and studied. Complex deadlocks have been revealed and classified. In the present paper, infinite Petri nets are divided into two following kinds: a single infinite construct and an infinite set of constructs of specified size (and number of dimensions). Finally, the paper discusses possible future work directions.

Automated summary

The correctness of networking protocols is crucial for cybersecurity, and recent developments in computing and communication grids have led to the need for verification of protocols for any number of devices. The introduction and study of infinite Petri nets have provided a new approach to analyzing computing and communication grid structures. Software generators for infinite Petri net models have been developed, and special classes of graphs like packet transmission directions and blockings have been introduced and studied for protocol analysis.