За результатами теоретичних і експериметальних досліджень запропоновано нові формальні методи вирішення відкритих проблем логічної коректності протоколів інформаційно-обчислювальних мереж. Показано, що існування в кожному циклі топології мережі хоча б одного каналу зв'язку з сингулярним алфавітом повідомлень є критерієм алгоритмічної розв'язності у ході перевірки логічної коректності протоколів зі складною топологією мережі. За допомогою цього критерію розроблено метод аналізу логічної коректності, який розширює клас перевірних протоколів. Під час розв'язання проблеми комбінаторного зростання числа аналізованих конфігурацій розроблено метод стиснення логічної структури еквівалентними перетвореннями, застосування якого скорочує число аналізованих ситуацій відносно існуючих методів більш ніж на 25 - 30 %. Під час проведення аналізу протоколів з обмеженою та необмеженою взаємодіями, через черги типу FIFO, одержано умови, які визначають класи протоколів із заздалегідь відомими властивостями. Знайдено достатню умову експоненціального переповнення мережі необробленими кадрами даних, на базі якої розроблено метод ідентифікації проблем в управлінні потоками даних у великих мережах. Запропоновані методи дозволяють розширити клас протоколів, які перевіряються, а також суттєво скоротити витрати часу та пам'яті в процесі їх аналізу.

  Скачати повний текст