Аналіз підходів до моделювання та верифікації кіберфізичних систем

Abstract

UK: Актуальність. Сучасні тенденції в продуктивності та складності вимог до використання систем вимагають принципово нових підходів до проектування, в яких кібернетичні та фізичні компоненти інтегруються на різних етапах. Кіберфізичні системи оточують людину майже у всіх сферах існування, починаючи з помешкань та транспорту і закінчуючи медичними апаратами та міжрегіональними електромережами. Тому верифікація та перевірка роботи таких систем є актуальною задачею сьогодення. В таких системах програмне забезпечення та фізичні підсистеми працюють у різних часових та просторових вимірах, взаємодіють різними способами. Розглянуто основні підходи до верифікації кіберфізичних систем. Об’єктом досліджень є процес верифікації кіберфізичних систем, предметом – методи верифікації кіберфізичних систем, моделі та логіки що використовуються при формальній верифікації. Мета. Мета роботи полягає в проведенні аналізу підходів до верифікації кіберфізичних систем, з деталізацією окремих етапів, таких як вибір моделей, інструментів верифікації, та, власно, методів верифікації. Метод. Основними методами, що викладені в роботі, є методи формальної верифікації кіберфізичних систем, а саме – симуляція, доведення теорем, символічне виконання та перевірка моделі. Детально розглянуто методологію методу перевірки моделі – модель Кріпке та темпоральні логіки: логіка дерев обчислень та логіка лінійного часу. Також проведено моделювання з використанням скінчених автоматів. Результати. Виконано моделювання кіберфізичної системи у вигляді створення моделі Кріпке, що дозволило описати всі стани системи, необхідні для виконання формальної верифікації. Висновки. Проведено дослідження характеристик кіберфізичних систем, виконано аналіз методів верифікації таких систем. Зазначені недоліки стандартної методології, які більш за все стосуються етапу моделювання кіберфізичних систем. Доведено найбільшу перспективність методу перевірки моделі, для якого розглянуто основну методологію. Дано характеристику моделям Кріпке та темпоральним логікам як основним елементам методу перевірки моделі. Показано можливість використання скінченних автоматів, а саме моделей Кріпке, для моделювання елементів кіберфізичної системи. Наукова новизна роботи полягає в тому що було розроблено моделі кіберфізичних систем, які, на відміну від існуючих, засновані на моделях Кріпке, що дозволяє зробити детальний опис усіх станів системи, що, у свою чергу, є важливим кроком для виконання верифікації такої системи. Практичною цінністю роботи є розроблені моделі електронезалежної станції альтернативної енергетики, що дозволять автоматизувати процес зарядки електричних транспортних засобів. Були реалізовані цифрові двійники, які дозволяють моделювати процеси електронезалежної станції альтернативної енергетики. Розроблені двійники використовуються при вивчені дисциплін при підготовки бакалаврів та магістрів спеціальності 121 комп’ютерні науки. EN: Context. Current trends in the performance and complexity of system requirements require fundamentally new approaches to design, in which cybernetic and physical components are integrated at different stages. Cyber-physical systems are systems that provide close interaction between physical and cybernetic components, integration of computing, physical processes and networks. In such systems, software and physical subsystems operate in different temporal and spatial dimensions, interacting in different ways. Cyber-physical systems surround humans in almost every area of existence, from housing and transportation to medical devices and interregional power grids. Therefore, verification and validation of such systems is an urgent task today. Approaches to verification of cyber-physical systems are considered. The object of research is the process of verification of cyber-physical systems, the subject is the methods of verification of cyber-physical systems, models and logic used in formal verification. Objective. The purpose of the work is to analyze approaches to the verification of cyber-physical systems, detailing the individual steps, such as the selection of models, verification tools, and, in fact, verification methods. Method. The main methods outlined in the paper are methods of formal verification of cyber-physical systems, namely simulation, theorem proving, symbolic execution, and model checking. In addition, the methodology of the model checking method – the Kripke structure and temporal logics: logic of computational trees and linear time logic is discussed in detail. Modeling using finite state machines is also performed. Results. The paper deals with modeling of the cyber-physical system in the form of creation of the Kripke structure that allowed to describe all states of the system necessary for executing of formal verification. Conclusions. The paper describes the characteristics of cyber-physical systems, analyzes the methods of verification of such systems. After analysis the conclusion is made about the most promising method of model verification, for which the basic methodology is considered. Characteristics of Kripke structure and temporal logics are described as the main elements of the model checking method. Following the review, the shortcomings of the standard methodology most relevant to the modeling stage of cyber-physical systems are concluded. The possibility of using finite state machines, namely Kripke structures, for modeling elements of a cyber-physical system is shown. The scientific novelty of the work is that models of cyber-physical systems have been developed, which, unlike existing ones, are based on Kripke structures, which allow to make a detailed description of all states of the system, which, in turn, is an important step to verify such a system. The practical value of the work is the developed models of the independent power station of alternative energy, which will automate the process of charging electric vehicles. Digital duplicates have been implemented, which allow modeling the processes of an independent energy station of alternative energy. The developed duplicates are used in the study of disciplines in the preparation of bachelors and masters in 121 computer science.