Поведінкова верифікація систем інтернету речей на основі мереж Петрі

Анотація

Швидкий розвиток, впровадження в усі сфери діяльності людини і зростання відповідальності
виконуваних функцій систем Інтернет речей посилюють і ускладнюють вимоги до достовірності їх проектних рішень на
етапах розробки і працездатності в ході експлуатації реалізацій. Відомі методи верифікації проектів і реалізацій
спираються на засоби системного, структурного, функціонального, конструкторсько-технологічного аналізу і синтезу
систем Інтернет речей. Однак їхній ресурс не применшує доцільність розвитку формальних моделей і методів верифікації,
зокрема, їх комплексування на ранніх системно-функціональних етапах, де неминуче і істотно «ручне» проектування. У
даній роботі наведені елементи комплексної поведінкової верифікації проектів системно-функціонального рівня для систем
Інтернет речей, які подаються за допомогою вхідних UML-діаграм і проектованих мереж Петрі. Верифікація включає на
першому етапі «ручний» етап системного аналізу коректності сутностей і відносин вхідних UML-діаграм і простих
мереж Петрі, що виконується як їх покриття при активізації в візуальному моделюванні. Для цього етапу наведено
загальні оцінки витрат на перепроектування в разі появи помилок. На другому етапі в верифікації системнофункціонального рівня виконується автоматизований аналіз коректності більш складних мереж Петрі, що відповідають
реальним об'єктам, в середовищі CPN Tools з моделюванням їх поведінки і побудовою графа досяжних станів (розміток). В
цьому випадку результат дозволяє динаміку роботи мережі Петрі, оцінити наявність тупиків, висячих вершин,
нескінченних циклів, властивості безпеки і жвавості і при необхідності виконати перепроектування. Спільне комплексне
застосування системної «ручний» і функціональної автоматизованої верифікації для вхідних UML-моделей і проектованих
моделей мереж Петрі дозволяє скоротити час проектування систем Інтернет речей за рахунок виключення або
своєчасного усунення проектних помилок.