Тіменко, Артур ВалентиновичTimenko, Artur V.2021-01-152021-01-1520192409-3858 (Print)2519-1845 (Online)https://eir.nuos.edu.ua/handle/123456789/3411Тіменко, А. В. Щодо аспектів специфікації і перевірки протоколів інтернету речей = On the aspects of iot protocols specification and checking / А. В. Тіменко // Shipbuilding & Marine Infrastructure. – 2019. – № 2 (12). – С. 35–41.Анотація. Сучасний рівень складності різноманітних програмних систем зумовлює потребу адаптації та доопрацювання процесу розроблення таких систем належним чином. Показовими прикладами останніх є системи, побудовані згідно з концепцією Інтернету речей, що, зокрема, передбачає застосування спеціалізованих протоколів взаємодії компонентів. Концепція Інтернету речей охоплює мільярди різнорідних «розумних» пристроїв, що взаємодіють один з одним на основі різноманітних протоколів. З огляду на варіативність протоколів взаємодії та їх реалізацій виникає проблема сумісності таких пристроїв. Разом із цим варто відзначити, що під час проектування різного роду систем, наприклад систем критичного призначення, все більшого поширення набуває використання формальних методів, зокрема методів перевірки на моделі. Робота адресується вирішенню проблеми перевірки сумісності компонентів систем Інтернету речей шляхом автоматизованого застосування методів перевірки на моделі. Мета роботи – запропонувати підхід до вирішення проблеми перевірки сумісності компонентів систем Інтернету речей за рахунок застосування методу перевірки на моделі. Методика полягає в наступному: спочатку синтезується абстрактна специфікація, потім ця специфікація деталізується і перевіряється методом перевірки на моделі в автоматизованому режимі. Як результат запропоновано підхід до перевірки сумісності компонентів систем Інтернету речей, що полягає в автоматизованій формальній верифікації протоколів взаємодії. Синтез специфікації протоколу MQTT згідно з запропонованим підходом розглядається як тематичне дослідження.ukIoTпротоколспецифікаціяверифікаціяперевірка на моделісумісністьQoSTLAIoTprotocolspecificationverificationmodel checkinginteroperabilityQoSTLAArticle