Search academic texts

Information × Registration Number 2120U009232, Article popup.category Опубліковано, Стаття Title ANALYSIS OF APPROACHES TO THE SIMULATION AND VERIFICATION OF CYBER-PHYSICAL SYSTEMS popup.author Коротунов С. Ю.Табунщик Г. В.Korotunov S. U.Tabunshchyk G. V. popup.publication 06-11-2020 popup.source_user Журнал "Радіоелектроніка, інформатика, управління" (Національний університет "Запорізька політехніка") popup.source https://ric.zp.edu.ua/article/view/214805 popup.publisher National University "Zaporizhzhia Polytechnic" Description Актуальність. Сучасні тенденції в продуктивності та складності вимог до використання систем вимагають принципово нових підходів до проектування, в яких кібернетичні та фізичні компоненти інтегруються на різних етапах. Кіберфізичні системи оточують людину майже у всіх сферах існування, починаючи з помешкань та транспорту і закінчуючи медичними апаратами та міжрегіональними електромережами. Тому верифікація та перевірка роботи таких систем є актуальною задачею сьогодення. В таких системах програмне забезпечення та фізичні підсистеми працюють у різних часових та просторових вимірах, взаємодіють різними способами. Розглянуто основні підходи до верифікації кіберфізичних систем. Об’єктом досліджень є процес верифікації кіберфізичних систем, предметом – методи верифікації кіберфізичних систем, моделі та логіки що використовуються при формальній верифікації. Мета.Мета роботи полягає в проведенні аналізу підходів до верифікації кіберфізичних систем, з деталізацією окремих етапів, таких як вибір моделей, інструментів верифікації, та, власно, методів верифікації.Метод. Основними методами, що викладені в роботі, є методи формальної верифікації кіберфізичних систем, а саме – симуляція, доведення теорем, символічне виконання та перевірка моделі. Детально розглянуто методологію методу перевірки моделі – модель Кріпке та темпоральні логіки: логіка дерев обчислень та логіка лінійного часу. Також проведено моделювання з використанням скінчених автоматів.Результати. Виконано моделювання кіберфізичної системи у вигляді створення моделі Кріпке, що дозволило описати всі стани системи, необхідні для виконання формальної верифікації. Висновки. Проведено дослідження характеристик кіберфізичних систем, виконано аналіз методів верифікації таких систем. Зазначені недоліки стандартної методології, які більш за все стосуються етапу моделювання кіберфізичних систем. Доведено найбільшу перспективність методу перевірки моделі, для якого розглянуто основну методологію. Дано характеристику моделям Кріпке та темпоральним логікам як основним елементам методу перевірки моделі. Показано можливість використання скінченних автоматів, а саме моделей Кріпке, для моделювання елементів кіберфізичної системи. Наукова новизна роботи полягає в тому що було розроблено моделі кіберфізичних систем, які, на відміну від існуючих, засновані на моделях Кріпке, що дозволяє зробити детальний опис усіх станів системи, що, у свою чергу, є важливим кроком для виконання верифікації такої системи. Практичною цінністю роботи є розроблені моделі електронезалежної станції альтернативної енергетики, що дозволять автоматизувати процес зарядки електричних транспортних засобів. Були реалізовані цифрові двійники, які дозволяють моделювати процеси електронезалежної станції альтернативної енергетики. Розроблені двійники використовуються при вивчені дисциплін при підготовки бакалаврів та магістрів спеціальності 121 комп’ютерні науки. popup.nrat_date 2026-02-09 Close