Підхід до перевірки віртуальної топології програмно-конфігурованої мережі



Вадим Вікторович Шкарупило, Равіль Камілович Кудерметов, Артур Валентинович Тіменко, Ольга Володимирівна Польська

Анотація


У наш час концепція програмно-конфігурованих мереж широко розглядається у якості однієї з основоположних технологій подальшого розвитку Інтернету – у вигляді Інтернету речей. При цьому, спираючись на специфіку названих мереж, оперують поняттям віртуальної топології мережі. Це дає змогу гнучким та оперативним чином реагувати на зміну вимог до розподілених програмних систем, побудованих на основі мережі. При цьому постає проблема перевірки узгодженості компонентів системи. З цією метою у статті проаонується підхід до перевірки віртуальної топології програмно-конфігурованої мережі. Запропонований підхід ґрунтується на використанні темпоральної логіки дій (Temporal Logic of Actions, TLA). В основі запропонованого підходу – використання концепції «дії» (action). Для представлення специфіки запропонованого підходу використано структуру Кріпке. Відмінна риса запропонованого підходу – гнучкість реконфігурування специфікації (формальної моделі) системи з віртуальною топологією. Перевірку топології запропоновано виконувати шляхом автоматизованої формальної верифікації методом перевірки на моделі. З метою поліпшення автоматизації, застосовано реалізацію методу перевірки на моделі TLA Checker (TLC), що ґрунтується на обході простору станів системи переходів в основі формальної моделі методом обходу в ширину (Breadth-first Search, BFS).

Ключові слова: ad-hoc, Quality of Services, верифікація, віртуальна топологія, Інтернет речей, перевірка на моделі, програмно-конфігурована мережа, специфікація.


Повний текст:

PDF

Посилання

  • Поки немає зовнішніх посилань.