Object of research – telecommunication processes, as a result of software or hardware implementation of telecommunication protocols, which stipulate unlimited number of interacting devices. Subject of research – formal methods of telecommunication protocols verification by infinite Petri nets, methods of analysis, synthesis and transformation of correspondent models of telecommunication systems by reenterable colored Petri nets. Purpose of research – development of models, methods, and tools of analysis, synthesis, and transformation of telecommunication systems models for verification of protocols and efficiency evaluation of networking technologies, which stipulate an arbitrary number of interacting systems. Research methods: methods of multisets theory and multisets rewriting systems, linear algebraic methods, theory of partially ordered sets (lattices) and number theory methods, methods of graph theory, methods of Petri net theory, simulation and mathematical statistics methods, methods of process algebra (calculus), elements of theories of reenterable, preemptive and parallel programs. Theoretical and practical results: a task of verification of telecommunication protocols with arbitrary number of communicating devices and complex verification of families of telecommunication protocols has been solved that required to introduce for the first time a class of infinite Petri nets and to develop the basics of infinite Petri nets theory; methods of graph theory have been further developed, a transmissions graph and a graph of possible blockings of devices have been introduced for the first time and applied to study the liveness of telecommunication systems models, a complete classification of deadlocks obtained; to study radio and cellular communication protocols, communication systems of supercomputers and networks-on-chip, generalized models of triangular, hexagonal, and rectangular lattices on plane, hypercube and hypertorus in multidimensional spaces have been built; for the first time, a class of reenterable models of telecommunication networks is introduced, which contains each component in a single instance and specifies the packet location within a network using a topological information descriptor; advantages of reenterable models are reduction of the model size and time of its development in one and a half times and re-use of models; reenterable models of IP, MPLS, and PBB networks, rectangular grids, IP networks routing based on distance-vector protocols have been developed, and the measuring components method has been further developed for the performance and quality of service evaluation directly in the process of simulation; reenterable models have been applied to investigate the cybersecurity aspects of the computing grids operation and a possibility of blocking grids via inducing deadlocks has been revealed; as a practical result of the dissertation, a library of models and software have been developed to automatically synthesize models.
