Пошук академічних текстів

Інформація × Реєстраційний номер 2120U009232, Матеріали видань та локальних репозитаріїв Категорія Опубліковано, Стаття Назва роботи АНАЛІЗ ПІДХОДІВ ДО МОДЕЛЮВАННЯ ТА ВЕРИФІКАЦІЇ КІБЕРФІЗИЧНИХ СИСТЕМ Автор Коротунов С. Ю.Табунщик Г. В.Korotunov S. U.Tabunshchyk G. V. Дата публікації 06-11-2020 Постачальник інформації Журнал "Радіоелектроніка, інформатика, управління" (Національний університет "Запорізька політехніка") Першоджерело https://ric.zp.edu.ua/article/view/214805 Видання National University "Zaporizhzhia Polytechnic" Опис Актуальність. Сучасні тенденції в продуктивності та складності вимог до використання систем вимагають принципово нових підходів до проектування, в яких кібернетичні та фізичні компоненти інтегруються на різних етапах. Кіберфізичні системи оточують людину майже у всіх сферах існування, починаючи з помешкань та транспорту і закінчуючи медичними апаратами та міжрегіональними електромережами. Тому верифікація та перевірка роботи таких систем є актуальною задачею сьогодення. В таких системах програмне забезпечення та фізичні підсистеми працюють у різних часових та просторових вимірах, взаємодіють різними способами. Розглянуто основні підходи до верифікації кіберфізичних систем. Об’єктом досліджень є процес верифікації кіберфізичних систем, предметом – методи верифікації кіберфізичних систем, моделі та логіки що використовуються при формальній верифікації. Мета.Мета роботи полягає в проведенні аналізу підходів до верифікації кіберфізичних систем, з деталізацією окремих етапів, таких як вибір моделей, інструментів верифікації, та, власно, методів верифікації.Метод. Основними методами, що викладені в роботі, є методи формальної верифікації кіберфізичних систем, а саме – симуляція, доведення теорем, символічне виконання та перевірка моделі. Детально розглянуто методологію методу перевірки моделі – модель Кріпке та темпоральні логіки: логіка дерев обчислень та логіка лінійного часу. Також проведено моделювання з використанням скінчених автоматів.Результати. Виконано моделювання кіберфізичної системи у вигляді створення моделі Кріпке, що дозволило описати всі стани системи, необхідні для виконання формальної верифікації. Висновки. Проведено дослідження характеристик кіберфізичних систем, виконано аналіз методів верифікації таких систем. Зазначені недоліки стандартної методології, які більш за все стосуються етапу моделювання кіберфізичних систем. Доведено найбільшу перспективність методу перевірки моделі, для якого розглянуто основну методологію. Дано характеристику моделям Кріпке та темпоральним логікам як основним елементам методу перевірки моделі. Показано можливість використання скінченних автоматів, а саме моделей Кріпке, для моделювання елементів кіберфізичної системи. Наукова новизна роботи полягає в тому що було розроблено моделі кіберфізичних систем, які, на відміну від існуючих, засновані на моделях Кріпке, що дозволяє зробити детальний опис усіх станів системи, що, у свою чергу, є важливим кроком для виконання верифікації такої системи. Практичною цінністю роботи є розроблені моделі електронезалежної станції альтернативної енергетики, що дозволять автоматизувати процес зарядки електричних транспортних засобів. Були реалізовані цифрові двійники, які дозволяють моделювати процеси електронезалежної станції альтернативної енергетики. Розроблені двійники використовуються при вивчені дисциплін при підготовки бакалаврів та магістрів спеціальності 121 комп’ютерні науки. Додано в НРАТ 2026-02-09 Закрити