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

Анотація

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