Поведінкова верифікація систем інтернету речей на основі мереж Петрі
DOI:
https://doi.org/10.15276/aait.04.2019.4Ключові слова:
системи Інтернет речей, поведінкова верифікація, мережа Петрі, покриття перевіряються властивостей, складність верифікаціїАнотація
Швидкий розвиток, впровадження у всіх сферах людської діяльності та зростаюча відповідальність функцій Інтернет- систем речей посилюють і ускладнюють вимоги до надійності їх проектних рішень на етапах розробки та працездатності під час впровадження в життя. Загальновідомі методи перевірки проектів та реалізацій базуються на засобах системного, структурного, функціонального, конструкторсько-технологічного аналізу та синтезу Інтернет-систем речей. Однак їхні можливості не занижують доцільність розробки формалізованих моделей та методів перевірки. У цьому дослідженні представлені елементи технології та етапи методології перевірки поведінки проектів функціонального рівня для Інтернет- систем речей, представлених за допомогою мереж Петрі. Загальна перевірка представлена трьома етапами - аналіз правильності загальних структурних та функціональних властивостей, фактична перевірка міжрівневих та міжкомпонентних взаємодій, поведінкове тестування в режимі онлайн та офлайн у класі помилок функціонального типу. У запропонованому аналізі визначаються основні сутності та взаємозв'язки систем речей Інтернету речей та перевіряються архітектурний рівень, що визначає структуру, компоненти, функції, інтерфейси, взаємодії асинхронно-подій та представляють елементи мереж Петрі - їхні позиції, переходи, дуги , функції, розмітка. Тестування в Інтернеті та офлайн для динамічної перевірки поведінки в Інтернеті систем речей проводиться на основі відповідно фону або спеціального формування багатьох технологічних потоків в мережі Петрі, активованих під час її моделювання та охоплення об'єктів мережі Петрі . У цій роботі представлені загальні оцінки витрат ресурсів та часу на проектування Інтернет-систем речей без перевірки та з верифікацією, показано їх зменшення у разі помилок проектування, перероблення та застосування верифікації. Перевірка проілюстрована на прикладі мереж Петрі, що імітують автоматичну систему освітлення.