Об’єкт дослідження – телекомунікаційні процеси як результат програмної або апаратної реалізації телекомунікаційних протоколів, які передбачають взаємодію необмеженої кількості пристроїв. Предмет дослідження – формальні методи верифікації телекомунікаційних протоколів на основі нескінченних сіток Петрі, методи аналізу, синтезу та перетворення відповідних моделей телекомунікаційних систем реєнтерабельними розфарбованими сітками Петрі. Мета дослідження – розробка моделей, методів та інструментальних засобів аналізу, синтезу та перетворення моделей телекомунікаційних систем для верифікації протоколів і оцінки ефективності мережевих технологій, які передбачають довільну кількість взаємодіючих систем. Методи дослідження: методи теорії мультимножин і перезапису мультимножин, методи лінійної алгебри, методи теорії частково впорядкованих множин (ґраток) і теорії чисел, методи теорії графів, методи теорії сіток Петрі, методи імітаційного моделювання і математичної статистики, методи алгебри (числення) процесів, елементи теорії реєнтерабельних, преємптивних і паралельних програм. Теоретичні та практичні результати: розв'язано завдання верифікації телекомунікаційних протоколів з довільною кількістю взаємодіючих пристроїв і комплексної верифікації сімейств телекомунікаційних протоколів для чого вперше введений клас нескінченних сіток Петрі і розроблено основи теорії нескінченних сіток Петрі; отримали подальший розвиток методи теорії графів, вперше введені граф передач і граф можливих блокувань пристроїв, за допомогою яких досліджено живість моделей телекомунікаційних систем та розроблена повна класифікація тупиків; для дослідження протоколів систем радіомовлення і стільникового зв'язку, комунікаційних систем суперкомп'ютерів і мереж на чипі побудовані узагальнені моделі трикутної, шестикутної та прямокутної ґраток на площині, гіперкуба і гіпертора в багатовимірних просторах; вперше введено клас реєнтерабельних моделей телекомунікаційних мереж, який містить кожен компонент в єдиному екземплярі і задає місце розташування пакета в мережі за допомогою дескриптора топологічної інформації; перевагами реєнтерабельних моделей є скорочення розміру моделі і часу її розробки у півтори рази та повторне застосування моделі; побудовано реєнтерабельні моделі IP, MPLS, PBB мереж, прямокутних ґраток, маршрутизації IP мереж за дистанційно-векторними протоколами та отримав подальший розвиток метод вимірювальних компонентів для оцінки продуктивності і якості обслуговування безпосередньо в процесі імітаційного моделювання; реєнтерабельні моделі застосовано для дослідження аспектів кібербезпеки функціонування обчислювальних ґраток та виявлена можливість блокування ґраток через створення тупиків; в результаті виконання роботи побудовано бібліотеки моделей та програмне забезпечення для автоматичного синтезу моделей.
