Верификация протоколов треугольных коммуникационных решеток бесконечными сетями Петри

Abstract

RU: Актуальность. Вычислительные и коммуникационные решетки являются мощным средством повышения производительности и качества обслуживания современных сетей. В двумерных решетках основными формами ячейки являются треугольник, четырехугольник и шестиугольник. Треугольные решетки применяются при решении краевых задач с треугольными конечными элементами в системах радиовещания и телевидения. Наиболее простые и эффективные способы реализации решеток могут обладать скрытыми дефектами и уязвимостями с точки зрения безопасного обмена информации. Таким образом, верификация решеток является актуальной задачей. Цель работы – построение моделей треугольных коммуникационных решеток в форме бесконечных сетей Петри и исследование их свойств для доказательства корректности (верификации) протоколов. Методы исследований базируются на основных положениях теории графов, линейной алгебры, теоретических основах сетей Петри, математического и имитационного моделирования. Результаты. Построено параметрическое описание треугольной коммуникационной решетки на плоскости в прямой и двойственной форме. Узел коммутации реализует полнодуплексный режим работы и буферизацию пакетов с ограниченным размером внутреннего буфера. Получены аналитические выражения для оценки числа компонентов модели. Решение бесконечных системы линейных уравнений в параметрической форме позволило доказать инвариантность модели произвольного размера. Инвариантность является одним из основных свойств модели идеального протокола, определяющих безопасность работы сети. Практическая значимость полученных результатов заключается в построении схем безопасных решеток для дальнейшей программной и аппаратной реализации, что официально подтверждено включением моделей треугольных решеток в архив моделей сетей Петри Лаборатории Информатики университета Париж 6. Выводы. Впервые построена математическая модель треугольных коммуникационных решеток с регулярной структурой произвольного размера в форме бесконечных сетей Петри для верификации протоколов передачи информации в решетках. Применение методики для верификации треугольных коммуникационных структур позволяет выполнить дальнейшее развитие теории бесконечных сетей Петри для построения и исследования моделей произвольных решеток с регулярной структурой. UK: Актуальність. Обчислювальні та комунікаційні ґратки є потужним засобом підвищення продуктивності і якості обслуговування сучасних мереж. У двовимірних ґратках основними формами осередку є трикутник, чотирикутник і шестикутник. Трикутні гратки застосовуються при вирішенні крайових задач з трикутними кінцевими елементами, в системах радіомовлення і телебачення. Найбільш прості та ефективні способи реалізації ґраток можуть володіти схованими дефектами і уразливостями з точки зору безпечного обміну інформацією. Таким чином, верифікація ґраток є актуальним завданням. Мета роботи – побудова моделей трикутних комунікаційних ґраток в формі нескінченних сітей Петрі та дослідження їх властивостей, для доказу коректності (верифікації) протоколів. Метод. Методи досліджень базуються на основних положеннях теорії графів, лінійної алгебри, теоретичних основах сітей Петрі, математичного та імітаційного моделювання. Результати. Побудовано параметричний опис трикутної комунікаційної ґратки на площині в прямій і двоїстої формі. Вузол комутації реалізує повнодуплексний режим роботи та буферизацію пакетів з обмеженим розміром внутрішнього буфера. Отримано аналітичні вирази для оцінки числа компонентів моделі. Рішення нескінченних системи лінійних рівнянь в параметричної формі дозволило довести інваріантність моделі довільного розміру. Інваріантність є одною з основних властивостей моделі ідеального протоколу, що визначає безпеку роботи мережі. Практична значимість отриманих результатів полягає в побудові схем безпечних ґраток для подальшої програмної і апаратної реалізації, що офіційно підтверджено включенням моделей трикутних ґраток в архів моделей сітей Петрі Лабораторії Інформатики університету Париж 6. Висновки. Вперше побудована математична модель трикутних комунікаційних ґраток з регулярною структурою довільного розміру в формі нескінченних сітей Петрі для верифікації протоколів передачі інформації в ґратках. Застосування методики для верифікації трикутних комунікаційних структур дозволяє виконати подальший розвиток теорії нескінченних сітей Петрі для побудови та дослідження моделей довільних ґраток з регулярною структурою. EN: 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.