Методы восстановления и анализа формальной модели наблюдаемого поведения для процессов во встроенных системах тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Гончаров Алексей Андреевич
- Специальность ВАК РФ00.00.00
- Количество страниц 242
Оглавление диссертации кандидат наук Гончаров Алексей Андреевич
Реферат
Synopsis
Введение
ГЛАВА 1. Методы верификации программного обеспечения и возможности применения для встраиваемых систем
1.1 Введение
1.2 Методы и инструменты статического анализа
1.3 Формальные методы и инструменты
1.4 Динамические методы и инструменты
1.5 Синтетические методы и инструменты
1.6 Экспертиза
1.7 Выводы
ГЛАВА 2. Разработка метода динамической актуализации процессов встроенных систем
2.1 Введение
2.2 Верификация и отладка ПО в современных электронных системах
2.3 Обнаружение модели в интеллектуальном анализе процессов: сравнительный анализ алгоритмов
2.4 Восстановление модели наблюдаемого поведения: индуктивный алгоритм и алгоритм выравнивания
2.5 Апробация метода с использованием индуктивного метода и алгоритма выравнивания
2.6 Выводы по использованию метода с использованием индуктивного метода и алгоритма выравнивания
2.7 Метод динамической актуализации для встроенных систем
2.8 Апробация метода динамической актуализации и сравнение с методом на основе индуктивного алгоритма и алгоритма выравнивания
2.9 Эксперименты на целевой платформе
2.10 Выводы после экспериментов на целевой платформе
2.11 Метод динамической актуализации для параллельных процессов
2.12 Апробация метода динамической актуализации для параллельных процессов
2.13 Выводы по главе
ГЛАВА 3. Разработка метода анализа процессов во встроенных системах по формальной модели наблюдаемого поведения
3.1 Анализ поведения процессов с использованием событийных графов
3.2 Преобразование событийного графа в граф состояний
3.3 Темпоральная логика
3.4 Использование нейронных сетей для анализа журналов событий и моделей процессов
3.5 Графовые нейронные сети для прогнозирования следующего события: обзор современных подходов
3.6 Архитектуры GNN, применяемые для прогнозирования событий во встраиваемых системах
3.7 Проблемы и стратегии развертывания GNN на устройствах
3.8 Аппаратно-ориентированное проектирование и методы оптимизации для встраиваемых систем с ограниченными ресурсами
3.9 Сравнение использования нейронных сетей GCN и классических алгоритмов для задач прогнозирования следующего события
3.10 Сравнение использования нейронных сетей GCN и классических алгоритмов для задачи поиска аномального поведения
3.11 Выводы
ГЛАВА 4. Анализ эффективности предлагаемого методов и предлагаемые инструментальные средства анализа
4.1 Оценка требований к памяти целевой платформы
4.2 Масштабирование метода
4.3 Рекомендации при использовании предлагаемого метода
4.4 Предлагаемые инструментальные средства
4.5 Выводы
Заключение
Список литературы
Приложение А. Акт внедрения результатов работы на практике
Публикации
Реферат
Актуальность темы. В настоящее время встроенные системы повсеместно распространены во многих областях, включая медицинские приборы, бытовую технику, автомобилестроение, системы автоматизации, промышленные роботы и многие другие. Одновременно с повсеместным распространением встроенных систем происходит усложнение аппаратной и программной составляющих отдельных вычислительных устройств, объединяемых между собой. Проектирование, внедрение и проверка таких систем представляют из себя сложные задачи, поскольку системы подвержены воздействию различных факторов, таких как задержки связи, скорости обработки и некорректности аппаратной и программной составляющих.
Верификация и отладка программного обеспечения - достаточно длительный и трудоёмкий этап при разработке встроенных систем. Встроенные системы часто представляют собой вычислительное устройство с серьезными ограничениями по производительности и внутренней памяти, что делает традиционные подходы, основанные на накоплении полного журнала событий, неприменимыми для задач длительного автономного мониторинга и отладки на этапе натурных испытаний. Существующие системы и способы мониторинга и анализа поведения встроенных систем зачастую представляют из себя либо платформозависимые инструменты, либо являются достаточно сложными для использования и внедрения, а также обладают недостатками в части масштабирования.
Формальные методы анализа, включая формальную верификацию, являются эффективными способами проверки корректной работы программного обеспечения для встроенных систем. Однако формальная модель процессов, составленная на этапе проектирования, не может отразить все особенности реальной эксплуатации. Таким образом, актуальными задачами являются получение формальной модели наблюдаемого поведения в процессе работы системы и проверка свойств спецификации применительно к этой модели, включая сравнение её с моделью ожидаемого поведения. В особенности это становится
актуальным на этапе натурных испытаний системы. В связи с этим средство динамической актуализации формальной модели наблюдаемого поведения становится важным инструментом для мониторинга работоспособности системы во времени. Под динамической актуализацией понимается создание модели с помощью встроенных средств в процессе работы системы.
Встроенные системы могут осуществлять длительную автономную работу без связи. По этой причине использование методов, предполагающих накопление журналов событий системы, в связи с ограниченностью ресурсов целевой платформы зачастую невозможно. Таким образом, актуальным является создание метода динамической актуализации, способного во время работы сохранять модель процессов системы с заранее прогнозируемыми затратами памяти, необходимой вычислительной мощностью, при которой получаемая модель является корректной.
Целью диссертационной работы является снижение требований к ресурсам для инструментальных средств мониторинга встроенных систем за счет создания метода и средств динамической актуализации формальной модели наблюдаемого поведения. Для достижения заданной цели в рамках диссертации были поставлены и решены следующие задачи:
1. Проведение анализа существующих методов восстановления формальной модели наблюдаемого поведения программно-аппаратных систем, в том числе определение критериев и условий использования методов для встроенных систем.
2. Разработка метода актуализации формальной модели наблюдаемого поведения, позволяющего наблюдать за поведением встроенных систем на протяжении длительных периодов непрерывной работы и реализуемого с учетом ограниченных ресурсов систем.
3. Разработка метода анализа полученной формальной модели наблюдаемого поведения встроенной системы, позволяющего предсказывать следующее событие, анализировать аномалии поведения, а также оценивать функциональное покрытие, вероятность пребывания системы в заданных
состояниях, определять последовательность событий, которая привела к отказу.
4. Разработка инструментальных средств автоматизированного анализа процессов встроенных систем на основе разработанного метода.
Методы исследования. В диссертации применялись методы интеллектуального анализа процессов (Process Mining), методы теории графов, методы статического анализа данных.
Основные положения, выносимые на защиту:
1. Метод динамической актуализации формальной модели наблюдаемого поведения процессов во встроенных системах, основанный на использовании предварительно определенных таблиц переходов, который, в отличие от подходов, требующих накопления полного журнала событий, обеспечивает фиксированное и прогнозируемое на этапе проектирования потребление ресурсов памяти (единицы Кбайт) и требования к вычислительной мощности, что делает его применимым для длительного автономного мониторинга систем с ограниченными ресурсами.
2. Метод анализа формальной модели наблюдаемого поведения, включающий:
2.1 Алгоритм преобразования событийных графов наблюдаемого поведения в графы состояний для последующего анализа свойств системы с использованием темпоральной логики и алгоритмов анализа графов.
2.2 Подход к прогнозированию следующего события и обнаружению аномалий на базе эвристического алгоритма, позволяющий снизить требования к необходимым ресурсам для реализации на базе вычислительных ресурсов микроконтроллеров.
2.3 Подход к прогнозированию следующего события и обнаружению аномалий с использованием графовых нейронных сетей, позволяющий увеличить точность прогнозирования поведения.
3. Программные средства динамической актуализации формальной модели поведения и её анализа, позволяющие сократить время разработки средств
мониторинга и автоматизировать процесс верификации на этапе натурных испытаний встроенных систем.
Научная новизна диссертации отражена в следующих пунктах:
1. Предложен метод динамической актуализации формальных моделей поведения для встроенных систем, который, в отличие от классических подходов Process Mining, основан на использовании предварительно определенных таблиц переходов. Это позволяет устранить зависимость от накопления полного журнала событий и гарантировать фиксированное потребление ресурсов на этапе проектирования.
2. Предложен алгоритм преобразования событийных графов наблюдаемого поведения в графы состояний, что обеспечивает возможность применения аппарата темпоральной логики и алгоритмов анализа графов для верификации свойств системы в реальном времени.
3. Предложен гибридный подход к анализу моделей поведения, который сочетает эвристический алгоритм для работы в условиях экстремального дефицита ресурсов и подход на основе графовых нейронных сетей для повышения точности прогнозирования. Это позволяет гибко выбирать инструмент анализа в зависимости от задач и доступных вычислительных мощностей.
4. Введен механизм обработки параллельных процессов через матрицы взаимодействия, что расширяет класс исследуемых систем с последовательных на распределенные и параллельные.
Научно-техническая задача, решаемая в диссертации, заключается в создании метода динамической актуализации формальной модели наблюдаемого поведения встроенных систем, позволяющего наблюдать за поведением исследуемых систем автономно на протяжении длительных периодов непрерывной работы и реализуемого с учетом ограниченных ресурсов систем.
Объектом исследования являются непрерывно работающие автономные встраиваемые системы с ограниченными ресурсами.
Предметом исследования являются методы восстановления и анализа формальной модели наблюдаемого поведения для процессов встроенных систем.
Теоретическая и практическая значимость. Теоретическая значимость работы состоит в развитии методологии формальной верификации и мониторинга встроенных систем:
1. Разработанная модель и метод обосновывают принципиальную возможность и условия проведения строгого формального анализа поведения системы в реальном времени, а не постфактум. Это вносит вклад в теорию динамической верификации, переводя ее из области анализа исторических данных в область анализа текущего состояния.
2. Полученные результаты позволяют теоретически определять и гарантировать верхние границы потребления памяти и вычислительной сложности для задач мониторинга на этапе проектирования системы. Это формирует теоретический базис для построения детерминированных, а не эмпирических, методов обеспечения надежности в ресурсо-ограниченных средах.
3. Предложенные методы анализа задают новое направление в построении "легковесных" интеллектуальных систем диагностики, теоретически формализуя требования к данным и методам для эффективного применения темпоральной логики и машинного обучения в условиях жестких ограничений.
4. Теоретически обоснован переход от сырых потоков событий к структурированным формальным моделям в качестве основы для проактивного мониторинга. Это открывает возможности для разработки новых классов алгоритмов принятия решений, оперирующих не данными, а семантическими состояниями системы.
Практическая значимость работы подтверждается следующими результатами:
1. На основе разработанных методов созданы программные средства (библиотеки на языке С), которые были успешно апробированы на отладочных платах (STM32F103) и внедрены в проекты ООО «Специальный
Технологический Центр» (что подтверждено актом внедрения). Внедрение позволило автоматизировать процесс верификации встроенного ПО на этапе натурных испытаний, сократив его трудоемкость.
2. Разработанные методы ориентированы на широкий класс практических задач:
2.1. Длительный автономный мониторинг и прогнозная диагностика критически важных систем (авионика, космические аппараты, медицинские импланты), где невозможен полный сбор журналов из-за ограничений по памяти и энергопотреблению.
2.2. Сокращение времени и стоимости разработки встроенных систем за счет автоматизации верификации и выявления аномалий на ранних этапах испытаний.
2.3. Повышение надежности широкого спектра IoT-устройств, систем промышленной автоматизации и робототехники за счет портируемых и ресурсо-эффективных средств анализа поведения в реальном времени.
Достоверность. Теоретическая достоверность обеспечивается применением корректного и признанного научным сообществом математического аппарата, включая теорию конечных автоматов, теорию графов, темпоральную логику и методы Process Mining. Разработанные методы и алгоритмы имеют строгое формальное обоснование.
Экспериментальная достоверность подтверждается воспроизводимыми результатами, полученными в контролируемых условиях на отладочных платах (например, STM32F103). Проведенные эксперименты демонстрируют стабильные и предсказуемые метрики, такие как фиксированное потребление памяти (единицы КБайт) и времени обработки, что является практической валидацией первого положения диссертации.
Корректность и обоснованность предложенных подходов дополнительно подтверждается их сравнительным анализом с существующими методами. Так, разработанный метод динамической актуализации модели, в отличие от
классических подходов Process Mining, не требует накопления полного журнала событий, что подтверждает его преимущества для ресурсо-ограниченных систем.
Апробация результатов проведена в рамках 14 докладов на всероссийских и международных конференциях (включая MICSECS 2020, CCIE2024, International Conference on Artificial Intelligence, Computer, Data Sciences and Applications), где они получили положительную оценку научного сообщества. Ключевые результаты опубликованы в трех статьях в рецензируемых научных изданиях.
Окончательным доказательством достоверности и практической значимости результатов является их успешное внедрение в проекты промышленной компании ООО «Специальный Технологический Центр», что подтверждено соответствующим актом. Внедрение демонстрирует работоспособность разработанных методов и программных средств в реальных условиях.
Внедрение результатов работы. Результаты использованы при проведении лекционных и лабораторных занятиях в курсах университета ИТМО:
• «Встроенные системы» и «Системы ввода/вывода» для бакалавров по направлению 09.03.01 на образовательной программе «Компьютерные системы и технологии».
• «Организация вычислительных систем» для магистров по направлению 09.04.01 на образовательной программе «Компьютерные системы и технологии».
Методы мониторинга с использованием динамической актуализации модели внедрены в проектах в ООО «СТЦ», что отражено в акте о внедрении.
Апробация результатов работы производилась в 14 докладах на 14 конференциях:
1. 12th The Majorov International Conference on Software Engineering and Computer Systems (MICSECS 2020), СПб, 10-11 декабря 2020 г. (Goncharov A., Bykovskii S. «Panorama Stitching Method Using Sensor Fusion»)
2. Пятидесятая научная и учебно-методическая конференция 2021 Университета ИТМО, СПб, 1-4 февраля 2021 г. (Гончаров А.А.,
Быковский С.В. «Разработка архитектуры распределенной операционной среды для роботизированных систем на базе микросервисов»)
3. Юбилейный X Конгресс молодых ученых, СПб, 14-17 апреля 2021 г. (Гончаров А.А. «Разработка архитектуры типового узла распределенной операционной среды для кибер-физических систем на базе микросервисов»)
4. Пятьдесят первая (LI) научная и учебно-методическая конференция Университета ИТМО, СПб, 2-5 февраля 2022 г. (Гончаров А.А., Быковский С.В. «Метод анализа процессов встроенных систем на базе моделей наблюдаемого поведения»)
5. XI Конгресс молодых ученых, СПб, 4-8 апреля 2022 г. (Гончаров А.А., Быковский С.В. «Разработка метода анализа процессов встроенных систем на базе моделей наблюдаемого поведения»)
6. 52 Научная и учебно-методическая конференция Университета ИТМО, СПб, 31 января - 3 февраля 2023 г. (Гончаров А.А., Быковский С.В. «Использование методов анализа процессов для верификации встроенных систем»)
7. XII КМУ 2023, СПб, 3 - 6 апреля 2023 г. (Гончаров А.А., Быковский С.В «Средство динамической актуализации формальной модели процессов для программного обеспечения микроконтроллеров»)
8. Пятьдесят третья (LIII) научная и учебно-методическая конференция Университета ИТМО, СПб, 29 января - 2 февраля 2024 г. (Шибаев А.Л., Гончаров А.А. Метод восстановления модели параллельных процессов во встроенных системах)
9. XIII Конгресс молодых ученых ИТМО, СПб, 8-11 апреля 2024 г. (Гончаров А.А., Быковский С.В., Шибаев А.Л. «Средство восстановления модели параллельных процессов во встроенных системах»)
10. 8th International Conference on Computing, Control and Industrial Engineering (CCIE2024), Wuhan, China, 22 - 23 June 2024. (Goncharov A., Bykovskii S.,
Kustarev P., Zhdanov A. «Dynamic Actualization of Formal Model for Microcontrollers Software»)
11. I Всероссийская научная студенческая конференция «Современная наука: вызовы, перспективы и возможности», СПб, 18 ноября 2024 г. (А. Л. Шибаев, А. А. Гончаров «Методы построения формальной модели наблюдаемого поведения»)
12.Пятьдесят третья (LIII) научная и учебно-методическая конференция Университета ИТМО, СПб, 27-31 января 2025 г. (Гончаров А.А. «Анализ моделей процессов встраиваемых систем»)
13.XIV Конгресс молодых ученых ИТМО, СПб, 7-11 апреля 2025 г. (Гончаров А.А. «Средство анализа графовых моделей встроенных систем»)
14.2025 International Conference on Artificial Intelligence, Computer, Data Sciences and Applications (Aleksei Goncharov, Sergei Bykovskii, Alexander Belozubov, Andrey Shibaev «Heuristic Algorithm for event prediction in Embedded Systems»).
Публикации. По результатам, представленным в диссертации, было опубликовано четыре статьи, из которых две в изданиях, индексируемых в международных базах данных Web of Science и Scopus и две публикации в журналах из перечня ВАК.
1. Гончаров А.А., Быковский С.В. Метод восстановления модели процессов во встроенных системах по журналу событий // Известия высших учебных заведений. Поволжский регион. Технические науки -2023. - № 3(63). - С
2. Гончаров А.А., Быковский С.В. Метод динамической актуализации модели взаимодействия параллельных процессов во встроенных системах // Известия высших учебных заведений. Приборостроение -2024. - Т. 67. -№ 9. - С
3. Goncharov A., Bykovskii S., Kustarev P., Zhdanov A. Dynamic Actualization of Formal Model for Microcontrollers Software//Lecture Notes in Electrical Engineering, 2024, Vol. 1253, pp
4. Goncharov A., Bykovskii S., Belozubov A., Shibaev A. Heuristic Algorithm for event prediction in Embedded Systems // 2025 International Conference on Artificial Intelligence, Computer, Data Sciences and Applications (ACDSA) -2025, pp
Личный вклад автора. Автором лично выполнен анализ литературных источников и существующих методов верификации встроенных систем (статический анализ, формальные и динамические методы), который послужил теоретической основой для разработки новых решений.
Автором разработаны метод динамической актуализации формальной модели наблюдаемого поведения процессов и метод анализа этой модели, включающий алгоритмы преобразования графов и подходы к прогнозированию событий и обнаружению аномалий.
В рамках предложенных методов автором разработаны:
1. Алгоритм преобразования событийных графов в графы состояний для последующего анализа свойств системы.
2. Эвристический алгоритм и подход с использованием графовых нейронных сетей для прогнозирования следующего события и обнаружения аномалий, адаптированные к ограниченным ресурсам микроконтроллеров.
3. Библиотеки на языке C, реализующие предложенные методы, которые были апробированы автором на отладочных платах.
Анализ рассмотренных в диссертации методов извлечения данных, теоретическое обоснование и реализация предложенных методов выполнены автором лично.
Научный руководитель обеспечивал методическую поддержку в оформлении публикаций и ключевых формулировок диссертации.
В совместных публикациях вклад автора заключался в постановке задачи исследования, разработке моделей и методик, проведении экспериментальных исследований, обработке и обобщении полученных результатов, а также формулировании выводов и практических рекомендаций.
Структура и объем диссертации. Диссертационная работа состоит из введения, четырёх глав, заключения, списка литературы и приложения, содержащего материалы, подтверждающие внедрение результатов диссертации. Полный объём диссертации составляет 241 страница текста с 12 таблицами и 41 рисунками. Список литературы содержит 118 наименований.
СОДЕРЖАНИЕ РАБОТЫ
Первая глава диссертационного исследования посвящена комплексному анализу методов верификации программного обеспечения (ПО) с акцентом на их применимость к встраиваемым системам, что формирует теоретико-методологическую базу для последующего исследования методов восстановления формальных моделей наблюдаемого поведения. Встраиваемые системы, интегрирующие аппаратную и программную компоненты для взаимодействия с физическими процессами в критически важных областях (автомобилестроение, авионика, медицина, промышленность), предъявляют исключительно высокие требования к надежности, безопасности и корректности функционирования ПО. Исторические прецеденты катастрофических последствий ошибок ПО (Therac-25, Boeing 737 MAX) подчеркивают важность эффективной верификации. В главе систематизированы ключевые понятия жизненного цикла ПО (этапы, виды деятельности, роли, артефакты), определены фундаментальные различия между верификацией и валидацией. Качество ПО рассмотрено через призму модели ISO 9126. Подчеркнута ключевая роль верификации независимо от модели жизненного цикла.
Основное содержание главы составляет детальная классификация и анализ методов верификации: статический анализ, формальные методы, динамические методы, синтетические методы и экспертиза. В выводах главы обосновано, что формальные методы (особенно проверка моделей и дедуктивный анализ) являются основой обеспечения корректности критических встраиваемых систем. Синтетические методы, интегрирующие формальный анализ с динамической проверкой (тестирование на основе моделей, символическое выполнение), признаны наиболее перспективным направлением. Динамические методы необходимы для оценки поведения в реальных условиях, а экспертиза - для учета аппаратных ограничений. Глава формирует теоретический фундамент, демонстрирующий, что эффективное восстановление и анализ формальных моделей наблюдаемого поведения встраиваемых систем требует комбинации рассмотренных методов верификации.
Вторая глава диссертационного исследования посвящена разработке и верификации метода динамической актуализации формальных моделей наблюдаемого поведения встраиваемых систем. Основной научной задачей являлось преодоление фундаментальных ограничений существующих подходов к анализу процессов в ресурсно-ограниченных средах, таких как микроконтроллеры с дефицитом памяти и вычислительной мощности. Исследование базируется на адаптации методологии интеллектуального анализа процессов (Process Mining), традиционно применявшейся в бизнес-информатике, к специфике встраиваемых систем. Ключевым достижением стало создание метода, обеспечивающего реконструкцию и постоянное обновление формальных моделей процессов в режиме реального времени без накопления объемных журналов событий.
В рамках теоретического обоснования проведен сравнительный анализ алгоритмов Process Mining (альфа, альфа+, эвристический, индуктивный), подтвердивший целесообразность использования индуктивного алгоритма для работы с зашумленными данными встраиваемых систем. Предложен усовершенствованный метод (рисунок 1), интегрирующий индуктивный алгоритм построения моделей процессов с алгоритмом выравнивания для обогащения моделей частотными характеристиками переходов. Апробация метода на 100 студенческих проектах в среде имитатора STM32F4 (SystemC) продемонстрировала:
1. Высокую эффективность сжатия данных.
2. Точность восстановления моделей при вариативности реализации ПО.
3. Возможность автоматизированной оценки соответствия эталону через метод воспроизведения на основе токенов.
Рисунок 1 - Структурная схема предлагаемого метода анализа процессов встроенных систем на базе наблюдаемого поведения с пост-обработкой данных Для устранения недостатков, связанных с требованиями к памяти и производительности в реальных устройствах, разработан метод динамической актуализации моделей на основе предварительно подготовленных таблиц (рисунок 2). Метод предполагает:
1. Задание временных ограничений переходов между событиями.
2. Обновление модели процессов встраиваемых систем в режиме реального времени.
3. Исключение хранения полного журнала событий.,
Методы на основе Process Mining требуют хранения журнала событий, что зачастую неприемлемо для микроконтроллеров. Предлагаемый метод динамической актуализации на основе таблиц является решением проблемы ограниченности ресурсов встраиваемых систем.
Рисунок 2 - Предлагаемый метод с динамической актуализацией модели
Рекомендованный список диссертаций по специальности «Другие cпециальности», 00.00.00 шифр ВАК
Извлечение читаемых моделей из логов событий2026 год, кандидат наук Бегичева Антонина Константиновна
Исправление моделей процессов с сохранением их структуры на основе журналов событий2019 год, кандидат наук Мицюк Алексей Александрович
Методы машинного обучения для контроля качества данных в научных экспериментах2020 год, кандидат наук Борисяк Максим Александрович
Методы обработки, декодирования и интерпретации электрофизиологической активности головного мозга для задач диагностики, нейрореабилитации и терапии нейрокогнитивных расстройств2022 год, доктор наук Осадчий Алексей Евгеньевич
Развитие алгебраической теории коллективных движений атомных ядер2020 год, доктор наук Ганев Хубен Ганев
Введение диссертации (часть автореферата) на тему «Методы восстановления и анализа формальной модели наблюдаемого поведения для процессов во встроенных системах»
поведения
Подход динамической актуализации на основе таблиц модели включает:
1. Создание таблиц с комбинациями переходов процессов. Таблицы делятся на три: таблица с временными ограничениями, таблица с корректными по времени событиями и превышающие временные ограничения события.
2. Сбор данных о событиях системы. Обновление таблиц и модели процессов в реальном времени, обеспечивая постоянную актуальность модели.
На рисунке 3 показан простейший пример после некоторого времени работы наблюдаемой системы, отображающий таблицы и график событийного графа с частотными характеристиками переходов. Сплошные линии представляют правильные переходы между событиями, а пунктирные — переходы с нарушением временных ограничений. Визуализация создается вне целевой платформы, к примеру, с помощью Graphviz и помогает визуально оценить модель реальной системы и нарушения временных ограничений.
Временные ограничения между переходами (мке)
Из \ В С1 С2 сз.
С1 100 100 100
С2 100 100 200
сз 300 200 100
Переходы между событиями с корректным временем перехода
Из \ В С1 С2 сз
С1 2 2 I
С2 0 0 2
СЗ 1 1 3
С1
/ '2 V \
и \
С2 1
>2 .1
Переходы между событиями с превышением времени перехода
Из \ В С1 С2 сз
С1 1 2 0
С2 0 0 0
СЗ 0 0 0
Рисунок 3 - Таблицы и визуализация модели для примера
Для сравнения были реализованы две библиотеки на языке C:
1. Метод с постобработкой, который требует хранения журнала событий и осуществляет ресурсоемкое восстановление модели.
2. Метод с динамической актуализацией, который обновляет таблицы в реальном времени, а также позволяет экономичнее использовать память устройства.
Эксперименты проводились на отладочной плате Blue Pill (микроконтроллер STM32F103C8T):
1. Сравнение методов по использованию памяти (RAM): метод с постобработкой журнала событий (таблица 1) исчерпывает память при ~2000 событий. Метод с таблицами обеспечивает долговременную работу (таблица 2, рисунок 4).
2. Сравнение методов по скорости работы: метод с постобработкой имеет растущее время восстановления модели (таблица 3, рисунок 5), а метод динамической
актуализации с предподготовленными таблицами обеспечивает практически мгновенную актуализацию модели.
Результат работы обоих методов - граф процесса с частотными характеристиками и аномалиями (рисунок 6).
Таблица 1 - Ресурсы памяти микроконтроллера STM32F103C8T для метода с постобработкой для хранения журнала событий
Количество регистрируемых событий ЯЛМ %
10 9,18
100 12,7
1000 47,85
2000 86,91
Таблица 2 - Ресурсы памяти микроконтроллера STM32F103C8T для метода с
предподготовленными таблицами
Количество регистрируемых событий ялм %
6553600*0,0001 12,7
58982400*0,0001 24,41
104857600*0,0001 71,29
Рисунок 4 - Сравнение методов по необходимым ресурсам памяти (RAM %) относительно количества регистрируемых событий
Таблица 3 - Временные характеристики рассматриваемых методов для микроконтроллера STM32F103C8T (для частоты работы в 1 МГц)
Метод Добавление 1 события, мс Восстановление модели из N событий, мс
10 100 200 1000 2000
Метод с постобработкой 0,124 22 29 30 91 109
Метод с таблицами 0,121 Строится в процессе работы системы
Восстановление модели из N событий (1 МГц частота МК)
120
юо
во
и £
с£
и о. л
60
40
О 250 500 750 1000 1250 1500 1750 2000
Количество записей в журнале событий
Рисунок 5 - Восстановление модели для метода с постобработкой в зависимости
от количества записей в журнале событий
Рисунок 6 - Событийный граф с частотными характеристиками, полученный во время работы тестовой программы на целевой платформе (пунктирной линией выделены переходы с нарушением установленных временных ограничений)
Далее предлагаемый метод с предподготовленными таблицами был расширен (рисунок 7) для распределенных систем через события взаимодействия. Использование матриц смежности для отдельных устройств и матриц взаимодействия позволяет формировать единую формальную модель.
Рисунок 7 - Предлагаемый метод актуализации модели процессов во встроенных
система для параллельных процессов
Апробация метода для параллельных процессов проводилась в два этапа: имитационное моделирование и тестирование на реальных микроконтроллерах. В имитационной среде было создано пять независимых потоков, представляющих устройства с уникальными событиями и случайными задержками для эмуляции нарушений временных условий. Результаты моделирования (рисунок 8) показали корректное построение графов, обнаружение некорректных переходов и возможность объединения моделей. На реальных микроконтроллерах STM32F103RB метод был реализован в виде библиотеки; два устройства взаимодействовали через UART, сохраняя локальные модели в таблицах (216 байт для первого устройства, 486 байт для второго устройства, ячейки в таблицах по 2 байта). Модели передавались на персональный компьютер (ПК) и объединялись. Результаты (рисунок 9) подтвердили обнаружение аномалий, фиксированное потребление памяти и возможность масштабирования времени наблюдения за распределенной системой путем изменения размерности ячеек. Эксперименты показали, что метод эффективно работает в распределенных системах, требует прогнозируемых ресурсов и позволяет масштабировать анализ.
Рисунок 8 - Апробация в многопоточной среде, имитирующей работу распределенных встраиваемых систем
Рисунок 9 - Апробация с использованием встраиваемых систем
Интеллектуальный анализ процессов адаптирован для встроенных систем. Метод (индуктивный алгоритм + выравнивание) эффективен для восстановления моделей, но ресурсоемок. Разработанный метод динамической актуализации на основе таблиц решает проблему ограниченных ресурсов, используя фиксированную на этапе проектирования память, позволяя осуществлять практически мгновенное обновление модели и обеспечивая применимость для восстановления моделей параллельных процессов.
Третья глава посвящена разработке методов анализа процессов во встроенных системах на основе полученной формальной модели наблюдаемого поведения.
Для анализа процессов событийный граф с частотными характеристиками предлагается преобразовать в граф состояний. Этапы: добавление вершин состояний, перенос событий на дуги, слияние эквивалентных вершин для получения сокращенного орграфа состояний. Полученный граф состояний позволяет производить верификацию свойств системы с использование темпоральной логики на соответствие спецификации.
Затем рассматривается потенциал нейронных сетей (НС), особенно графовых (GNN), для анализа полученных моделей процессов встроенных систем: обнаружение аномалий и прогнозирования следующего события.
Для задачи прогнозирования следующего события сравниваются: нейронные сети GCN, классические алгоритмы (Цепи Маркова, взвешенные случайные блуждания, алгоритмы поиска частых шаблонов (SPS) и предлагается эвристический алгоритм (на основе весов рёбер и степеней узлов).
Эксперименты на синтетических взвешенных матрицах смежности (5x5 -300x300) показали (рисунки 10 - 13):
1. Время вывода/прогноза: эвристический алгоритм и SPS самые быстрые, Цепи Маркова заметно медленнее.
2. Время обучения/построения модели: SPS эффективен, НС и Марковские цепи ресурсоемки.
3. Точность: Эвристика и SPS лидируют на больших матрицах.
4. Память: Эвристика и SPS наиболее эффективны, НС и Марковские цепи экспоненциально растут в зависимости от размерностей входных данных.
Рисунок 10 - Сравнение потребления памяти для задачи предсказания
следующего события
Рисунок 11 - Сравнение времени прогнозирования для задачи предсказания
следующего события
Рисунок 12 - Сравнение точности прогноза для задачи предсказания следующего
события
Рисунок 13 - Сравнение времени построения/обучения модели для задачи
предсказания следующего события
Общий вывод: алгоритм поиска частых шаблонов сбалансирован; зато эвристика не требует построения модели.
Далее было произведено сравнение методов обнаружения аномалий. Сравнивались два подхода: метод главных компонент (РСА) и автокодировщик (нейросетевой подход) на матрицах с точечными и кластерными аномалиями показало компромисс (рисунки 14 - 17):
1. Скорость/Память: РСА значительно эффективнее.
2. Точность: Нейросети превосходят на сложных аномалиях.
3. Время обучения нейросетей: экспоненциально растут с размером данных.
Рисунок 14 - Сравнение времени построения/обучения модели для задачи
предсказания следующего события
Рисунок 15 - Сравнение времени построения/обучения модели для задачи
предсказания следующего события
Рисунок 16 - Сравнение времени построения/обучения модели для задачи
предсказания следующего события
• -4 Нейронная сеть I
Рисунок 17 - Сравнение времени построения/обучения модели для задачи
предсказания следующего события
Вывод: метод главных компонент предпочтителен при ограниченных ресурсах; нейронные сети для высокой точности на сложных аномалиях.
Таким образом, в главе экспериментально обоснован выбор алгоритмов анализа для встроенных систем: для задач, требующих высокой скорости и
минимального потребления ресурсов (анализ на самом устройстве), предпочтительны классические методы. Нейросетевые подходы оправданы при анализе сложных данных на внешнем ПК, где точность является приоритетом.
Четвертая глава посвящена анализу эффективности предложенных методов восстановления и анализа формальных моделей наблюдаемого поведения, особенно в контексте ограниченных ресурсов встроенных систем.
Предложенный табличный метод обеспечивает значительное преимущество в эффективности памяти перед последовательным накоплением. Эмпирическая формула для минимального числа фиксируемых событий Кт1П = а* 28*Б, где а -количество активных переходов, 5 - размерность ячейки в байтах. Формула для требуемого объема памяти для табличного метода: У = Т*е2*Б, где Т -количество таблиц, е - количество фиксируемых событий. Для метода последовательного накопления журнала: V = т* Ь, где т - количество байт на событие, Ь - количество событий. Предполагается, что т =1 байт для <256 событий и 2 байта для > 256 событий. Таблица 4 сравнивает методы по использованию памяти и количеству фиксируемых событий, демонстрируя, что предлагаемый метод выгоднее при меньшем количестве фиксируемых событий системы и что большая размерность ячеек значительно увеличивает количество фиксируемых событий. Рисунок 18, сравнивающий рост зарегистрированных событий с объемом памяти, иллюстрирует, что при большом числе событий предлагаемый метод позволяет хранить больше событий в формате переходов из-за меньшего потребления памяти. Выводится формула для усредненного времени работы
системы до исчерпания таблиц: t = = — , где ^ - усредненная частота
событий. Приводятся примеры расчета: для Т=3, е=10, а=1, S=2 (600 байт памяти) можно зафиксировать 65 536 событий, что при частоте событий 200 мс может позволять фиксировать поведения системы до 3,64 часа работы. При S=4 (1200 байт) - 4,29 млрд событий, что дает до 9942 суток работы. Подчеркивается, что выбор метода и параметров зависит от частоты событий и требований к памяти. На
рисунке 19 представлена апробация на реальном проекте встраиваемой системы управления, где потребление памяти составило 1176 байт.
Таблица 4 - Сравнение методов в части требований к памяти целевой платформы и количества событий, которые можно зафиксировать
Необходимое Количество событий,
Метод количество памяти, байт которые можно зафиксировать
1 000 1 000
Метод с последовательным накоплением данных (т= 1)
10 000 10 000
100 000 100 000
е = 10; а = 1; 5 = 2 600 65 536*
е = 10; а = 4; 5 = 2 600 262 144*
Предлагаемый е = 10; а = 1; 5 = 4 1200 4 294 967 296*
метод (Т = 3)
е = 50; а = 1; 5 = 2 15 000 65 536*
е = 50; а = 4; 5 = 2 15 000 262 144*
*минимальное количество
е = 50; а = 1; 5 = 4 30 000 4 294 967 296*
событий е = 100; а = 1 ^ = 2 60 000 65 536*
е = 100; а = 4 ^ = 2 60 000 262 144*
е = 100; а = 1 ^ = 4 120 000 4 294 967 296*
Количество регистрируемых переходов в зависимости от количества выделенной памяти при различном количестве фиксируемых событий
10000000 1000000 100000 10000 1000 100 10 1
10000 65536 100000 1000000 10000000 к-во регистрируемых переходов
■ Метод с последовательным накоплением данных т = 1
■ Предлагаемый метод Т = 3; е = 10; а = 1; S = 2; Ктт = 65 536
■ Предлагаемый метод Т = 3; е = 10; а = 4; S = 2; Ктт = 262 144
■ Предлагаемый метод Т = 3; е = 10; а = 1; S = 4; Ктт = 4 294 967 296
■ Предлагаемый метод Т = 3; е = 100; а = 1; S = 2; Ктт = 65 536
■ Предлагаемый метод Т = 3; е = 100; а = 40; S = 2; Ктт = 2 621 440
■ Предлагаемый метод Т = 3; е = 100; а = 1; S = 4; Ктт = 4 294 967 2963
Рисунок 18 - Сравнительные графики роста количества регистрируемых событий встраиваемой системы в зависимости от количества выделенной памяти
т й а б
к
т я
ма п
й о
е
у
б
е р
т
о в-
-к
Рисунок 19 - Апробация на реальном проекте встраиваемой системы управления
Далее рассматривается возможность масштабирования метода путем перехода к таблицам большей размерности (трехмерным, четырехмерным и т. д.), что позволит сохранять последовательности из трех и более событий. Это приведет к кратному увеличению требований к памяти, но позволит хранить больше информации о последовательностях. Таблица 5 представляет сравнение и зависимости от размерности используемых таблиц, показывая формулы для длины сохраняемой последовательности, необходимого количества памяти (Т * ем * Б) и минимального количества фиксируемых переходов (а * М8*5).Приводится пример последовательности событий (С1-> С2-> С3-> С2-> С3-> С1-> С3-> С2-> С3) и ее разбиение на переходы для двумерных, трехмерных и четырехмерных таблиц. Отмечается, что сбои ПО легче отслеживать благодаря более подробным переходам, что стало возможным за счёт увеличенного объема памяти.
Таблица 5 - Масштабирование метода за счёт использования таблиц
различной размерности
Длина сохраняемой последовательности событий Необходимое количество памяти Минимальное количество потенциально фиксируемых переходов при заданных таблицах
[ ][ ] (2) 1 Т * е2 * Б а * 28*5
[ ][ ][ ] (3) 2 Т * е3 * Б а * 38*5
[ ][ ][ ][ ] (4) 3 Т * е4 * Б а * 48*5
[ ]...[] ОТ N - 1 Т*ем * Б а * Ы8*Б
Далее описаны рекомендации при использовании предлагаемого метода. Предлагается отслеживать только критические действия системы при ограниченных ресурсах памяти; выбирать размер ячейки в зависимости от периода наблюдения и частоты событий; отмечается, что максимальная эффективность достигается при равномерном распределении событий. Для улучшенного анализа причин сбоев предлагается составить перечень ключевых событий и переходов, установить буфер последних N событий и выгружать его при критическом событии. Этот способ сохраняет компактность данных и позволяет частично воссоздать последовательность событий перед сбоем.
С учетом ранее рассмотренных методов предлагается схема инструментальных средств (рисунок 20). Инструментальные средства для прогнозирования следующего события ^СМэвристический алгоритм), поиска аномалий (Автокодировщик/Метод главных компонент) и анализа требований спецификаций (проверка на изоморфизм графов, поиск путей, проверка покрытия
состояний, проверка свойств LTL) могут размещаться как вне целевой платформы, так и на ней, в зависимости от ресурсов и требований к оперативности анализа. Предлагаемая архитектура представляет собой гибкий конвейер, объединяющий различные методы для решения задач прогнозирования, обнаружения аномалий и верификации, с возможностью адаптации размещения компонент. Проведенный анализ показал, что предложенный метод позволяет обеспечить непрерывный мониторинг системы на протяжении от нескольких часов до нескольких лет (9942 суток в одном из сценариев) при затратах памяти всего в единицы КБ, что доказывает его высокую эффективность для автономных встраиваемых систем
Рисунок 20 - Итоговый вид инструментальных средства для анализа процессов
встроенных систем
В заключении подводится итог диссертационной работы, основным научным результатом которой является создание метода динамической актуализации формальной модели наблюдаемого поведения встроенных систем. Этот метод позволяет осуществлять автономное наблюдение за поведением систем на протяжении длительных периодов с учетом ограниченных ресурсов. Разработанный метод позволяет предсказывать следующее событие, анализировать аномалии поведения, а также дает возможность оценивать функциональное
покрытие, вероятность пребывания системы в заданных состояниях, учитывать частотные характеристики переходов и определять последовательность событий перед отказом. Предлагаемый метод характеризуется заранее рассчитываемыми на этапе проектирования требованиями к памяти целевой платформы и позволяет фиксировать события на всех уровнях ПО. Перечисляются основные результаты, полученные в процессе разработки метода, которые также являются положениями, выносимыми на защиту.
Synopsis
Relevance. Embedded systems are now ubiquitous in many fields, including medical devices, home appliances, automotive, automation systems, industrial robots, and many others. Along with the widespread adoption of embedded systems, the hardware and software components of individual computing devices interconnected are becoming increasingly complex. Designing, implementing, and testing such systems are complex tasks, as they are subject to various factors, such as communication latency, processing speed, and hardware and software inconsistencies.
Software verification and debugging is a lengthy and labor-intensive stage in the development of embedded systems. Embedded systems often consist of computing devices with severe performance and internal memory limitations, making traditional approaches based on accumulating a complete event log inapplicable for long-term autonomous monitoring and debugging during field testing. Existing systems and methods for monitoring and analyzing embedded system behavior are often platform-dependent, complex to use and implement, and have scalability limitations.
Formal analysis methods, including formal verification, are effective ways to verify the correct operation of software for embedded systems. However, a formal process model created at the design stage cannot reflect all the specifics of real-world operation. Therefore, the current tasks are to obtain a formal model of the observed behavior during system operation and to verify the specification properties against this model, including comparing it with the expected behavior model. This becomes especially important during the system's full-scale testing phase. Therefore, a means of dynamically updating the formal model of observed behavior becomes an important tool for monitoring system performance over time. Dynamic updating refers to the creation of a model using embedded tools during system operation.
Embedded systems can operate autonomously for long periods without communication. For this reason, methods that involve accumulating system event logs are often impossible due to the limited resources of the target platform. Therefore, it is important to develop a dynamic updating method capable of maintaining a model of
system processes during operation, with predictable memory consumption and the necessary computing power to ensure the resulting model is correct.
The goal of this dissertation is to reduce resource requirements for embedded system monitoring tools by developing a method and tools for dynamically updating the formal model of observed behavior. To achieve this goal, the following tasks were posed and solved within the dissertation:
1. Conducting an analysis of existing methods for restoring the formal model of the observed behavior of hardware and software systems, including determining the criteria and conditions for using methods for embedded systems.
2. Development of a method for updating the formal model of observable behavior, allowing for the observation of the behavior of embedded systems over long periods of continuous operation and implemented taking into account the limited resources of the systems.
3. Development of a method for analyzing the obtained formal model of the observed behavior of an embedded system, allowing to predict the next event, analyze behavior anomalies, as well as evaluate the functional coverage, the probability of the system being in given states, and determine the sequence of events that led to the failure.
4. Development of tools for automated analysis of embedded systems processes based on the developed method.
Research methods. The dissertation used methods of process mining, graph theory methods, and static data analysis methods.
Principal statements of the thesis, which are scientifically novel or has important practical significance:
1. A method for dynamically updating a formal model of the observed behavior of processes in embedded systems, based on the use of predefined transition tables, which, in contrast to approaches requiring the accumulation of a complete event log, provides fixed and predictable memory resource consumption (units of KB) and computing power requirements at the design stage, making it applicable for long-term autonomous monitoring of systems with limited resources.
2. A method for analyzing a formal model of observed behavior, including:
2.1 An algorithm for transforming event graphs of observed behavior into state graphs for subsequent analysis of system properties using temporal logic and graph analysis algorithms.
2.2 An approach to predicting the next event and detecting anomalies based on a heuristic algorithm, which allows reducing the requirements for the necessary resources for implementation based on the computing resources of microcontrollers.
2.3 An approach to next event prediction and anomaly detection using graph neural networks to improve the accuracy of behavior prediction.
3. Software tools for dynamic updating of the formal behavior model and its analysis, allowing to reduce the development time of monitoring tools and automate the verification process at the stage of full-scale testing of embedded systems.
The scientific novelty of the dissertation is reflected in the following points:
1. A method for dynamically updating formal behavior models for embedded systems is proposed. Unlike classical process mining approaches, it relies on predefined transition tables. This reduces the dependence on accumulating full log events and establishes fixed resource consumption at the design stage.
2. An algorithm for transforming event graphs of observed behavior into state graphs is proposed, which makes it possible to use the apparatus of temporal logic and graph analysis algorithms to verify the properties of a system in real time.
3. A hybrid approach to behavioral model analysis is proposed, combining a heuristic algorithm for working under extreme resource constraints and a graph neural network-based approach for improving forecasting accuracy. This allows for flexible selection of analysis tools depending on the tasks and available computing power.
4. A mechanism for processing parallel processes through interaction matrices has been introduced, which expands the class of systems under study from sequential to distributed and parallel ones.
The scientific and technical problem solved in the dissertation is to create a method for dynamically updating a formal model of the observed behavior of embedded systems, which allows for the autonomous observation of the behavior of the studied systems over long periods of continuous operation and is implemented considering the limited resources of the systems.
The object of the study is continuously operating autonomous embedded systems with limited resources.
The subject of the research is methods for restoring and analyzing the formal model of observed behavior for processes in embedded systems.
Theoretical and practical significance. The theoretical significance of the work lies in the development of a methodology for formal verification and monitoring of embedded systems:
1. The developed model and method substantiate the fundamental possibility and conditions for conducting a rigorous formal analysis of system behavior in real time, rather than post-factum. This contributes to the theory of dynamic verification, moving it from the field of historical data analysis to the field of current state analysis.
2. The obtained results allow us to theoretically determine and guarantee upper bounds on memory consumption and computational complexity for monitoring tasks at the system design stage. This forms the theoretical basis for developing deterministic, rather than empirical, methods for ensuring reliability in resource-constrained environments.
3. The proposed analysis methods set a new direction in the construction of "lightweight" intelligent diagnostic systems, theoretically formalizing the requirements for data and methods for the effective application of temporal logic and machine learning under severe constraints.
4. The transition from raw event streams to structured formal models as the basis for proactive monitoring is theoretically justified. This opens up opportunities for developing new classes of decision-making algorithms that operate not on data, but on the semantic states of the system.
The practical significance of the work is confirmed by the following results:
1. Based on the developed methods, software tools (C-language libraries) were created, which were successfully tested on debug boards (STM32F103) and implemented in projects at Special Technology Center LLC (as confirmed by an implementation certificate). This implementation allowed for the automation of the embedded software verification process during field testing, reducing its labor intensity.
2. The developed methods are aimed at a wide range of practical problems:
2.1. Long-term autonomous monitoring and predictive diagnostics of critical
systems (avionics, spacecraft, medical implants) where full log collection is not
possible due to memory and power consumption limitations.
2.2 Reducing the time and cost of developing embedded systems by automating
verification and anomaly detection at early stages of testing.
2.3. Improving the reliability of a wide range of IoT devices, industrial automation
systems, and robotics through portable and resource-efficient real-time behavior
analysis tools.
Reliability. Theoretical validity is ensured by the use of sound mathematical apparatus recognized by the scientific community, including finite automata theory, graph theory, temporal logic, and process mining methods. The developed methods and algorithms have a rigorous formal justification..
Experimental validity is confirmed by reproducible results obtained under controlled conditions on development boards (e.g., STM32F103). The experiments demonstrate stable and predictable metrics, such as fixed memory consumption (in KB) and processing time, which provides practical validation of the first thesis statement.
The validity and feasibility of the proposed approaches are further confirmed by a comparative analysis with existing methods. For example, the developed method of dynamic model updating, unlike classical Process Mining approaches, does not require the accumulation of a complete event log, confirming its advantages for resource-constrained systems.
The results were validated in 14 presentations at national and international conferences (including MICSECS 2020, CCIE2024, and the International Conference on Artificial Intelligence, Computer, Data Sciences, and Applications), where they received positive reviews from the scientific community. Key findings were published in three peer-reviewed scientific journals.
The final proof of the results' reliability and practical significance is their successful implementation in projects at the industrial company Special Technology Center LLC, as confirmed by a corresponding certificate. This implementation demonstrates the viability of the developed methods and software in real-world conditions.
Implementation of work results. The results were used in lectures and laboratory classes at ITMO University:
• "Embedded Systems" and "Input/Output Systems" for bachelors in the field 09.03.01 in the educational program "Computer Systems and Technologies".
• "Organization of Computing Systems" for master's students majoring in 09.04.01 of the Computer Systems and Technologies educational program.
Monitoring methods using dynamic model updating have been implemented in projects at STC, as reflected in the implementation report.
The results of the work were tested in 14 reports at 14 conferences:
1. 12th The Majorov International Conference on Software Engineering and Computer Systems (MICSECS 2020), St. Petersburg, December 10-11, 2020. (Goncharov A., Bykovskii S. «Panorama Stitching Method Using Sensor Fusion»)
2. The 50th Scientific and Educational-Methodological Conference 2021 of ITMO University, St. Petersburg, February 1-4, 2021. (Goncharov A.A., Bykovsky S.V. «Development of the architecture of a distributed operating environment for robotic systems based on microservices»)
3. Anniversary X Congress of Young Scientists, St. Petersburg, April 14-17, 2021. (Goncharov A.A. «Development of a typical distributed operating environment node architecture for cyber-physical systems based on microservices»)
4. Fifty-first (LI) scientific and educational-methodical conference of ITMO University, St. Petersburg, February 2-5, 2022. (Goncharov A.A., Bykovsky S.V. «A method for analyzing embedded systems processes based on observed behavior models»)
5. XI Congress of Young Scientists, St. Petersburg, April 4-8, 2022. (Goncharov A.A., Bykovsky S.V. «Development of a method for analyzing embedded systems processes based on observed behavior models»)
6. 52 Scientific and educational-methodical conference of ITMO University, St. Petersburg, January 31 - February 3, 2023. (Goncharov A.A., Bykovsky S.V. «Using process mining techniques to verify embedded systems»)
7. XII Congress of Young Scientists 2023, St. Petersburg, April 3-6, 2023. (Goncharov A.A., Bykovsky S.V. «A tool for dynamically updating a formal process model for microcontroller software»)
8. Fifty-third (LIII) scientific and educational-methodical conference of ITMO University, St. Petersburg, January 29 - February 2, 2024. (Shibaev A.L., Goncharov A.A. «Method for reconstructing a model of parallel processes in embedded systems»)
9. XIII Congress of Young Scientists of ITMO University, St. Petersburg, April 8-11, 2024. (Goncharov A.A., Bykovsky S.V., Shibaev A.L. «A tool for restoring a model of parallel processes in embedded systems»)
10. 8th International Conference on Computing, Control and Industrial Engineering (CCIE2024), Wuhan, China, 22 - 23 June 2024. (Goncharov A., Bykovskii S., Kustarev P., Zhdanov A. «Dynamic Actualization of Formal Model for Microcontrollers Software»)
11.I All-Russian Scientific Student Conference "Modern Science: Challenges, Prospects and Opportunities", St. Petersburg, November 18, 2024. (Shibaev A.L., Goncharov A.A. «Methods for constructing a formal model of observed behavior»)
12.Fifty-third (LIII) scientific and educational-methodical conference of ITMO University, St. Petersburg, January 27-31, 2025. (Goncharov A.A. «Analysis of process models of embedded systems»)
13.XIV ITMO Young Scientists Congress, St. Petersburg, April 7-11, 2025. (Goncharov A.A. «A tool for analyzing graph models of embedded systems»)
14. 2025 International Conference on Artificial Intelligence, Computer, Data Sciences and Applications (Aleksei Goncharov, Sergei Bykovskii, Alexander Belozubov, Andrey Shibaev «Heuristic Algorithm for event prediction in Embedded Systems»)
Publications. Based on the results presented in the dissertation, four articles were published, two of which were in journals indexed in the international databases Web of Science and Scopus and two publications in journals from the list of the Higher Attestation Commission..
1. A.A. Goncharov, S.V. Bykovskii A method of restoring models in embedded systems using the event log // Izvestiya vysshikh uchebnykh zavedeniy. Povolzhskiy region. Tekhnicheskie nauki = University proceedings. Volga region. Engineering sciences.2023;(3):5-17.
2. Goncharov A. A., Bykovsky S. V. Method of dynamic updating models of the interaction model of parallel processes in embedded systems. 2024. Vol. 67, N 9. P. 741-750.
Похожие диссертационные работы по специальности «Другие cпециальности», 00.00.00 шифр ВАК
Методы и инструменты повышения эффективности алгоритмов майнинга процессов2020 год, кандидат наук Шершаков Сергей Андреевич
Метод встроенного функционального мониторинга с динамической актуализацией модели поведения для систем на кристалле2015 год, кандидат наук Быковский Сергей Вячеславович
Разработка технологии синбиотического безалкогольного напитка, обогащенного инулином из корня подсолнечника2023 год, кандидат наук Коршунова Наталья Александровна
Совершенствование процесса и аппарата ультразвукового гидролиза кератинсодержащего сырья с использованием его в кормовых продуктах2024 год, кандидат наук Шанин Вячеслав Алексеевич
Идентификация параметров деформационного поведения материалов для задач проектирования технологических процессов сверхпластической формовки2022 год, кандидат наук Захарьев Иван Юрьевич
Список литературы диссертационного исследования кандидат наук Гончаров Алексей Андреевич, 2025 год
Список литературы
1. Leveson N. G. The Therac-25: 30 years later //Computer. - 2017. - Т. 50. - №2. 11. - С. 8-11.
2. Cruz B. S., de Oliveira Dias M. Crashed boeing 737-Max: fatalities or malpractice //GSJ. - 2020. - Т. 8. - №. 1. - С. 2615-2624.
3. Kneuper R. Software processes and life cycle models //Cham: Springer. - 2018.
4. IEEE Computer Society. Software Engineering Standards Committee. IEEE Standard for Software Verification and Validation. - IEEE, 1998. - Т. 1012. - №. 1998.
5. Pham H. Software reliability. - Springer Science & Business Media, 2000.
6. ISO/IEC 9126-1 Software engineering - Product quality - Part 1: Quality model. Geneva, Switzerland: ISO, 2001
7. ISO/IEC TR 9126-2 Software engineering - Product quality - Part 2: External metrics. Geneva, Switzerland: ISO, 2003
8. ISO/IEC TR 9126-3 Software engineering - Product quality - Part 3: Internal metrics. Geneva, Switzerland: ISO, 2003
9. ISO/IEC TR 9126-4 Software engineering - Product quality - Part 4: Quality in use metrics. Geneva, Switzerland: ISO, 2004
10.Benington H. D. Production of large computer programs //Annals of the History of Computing. - 1983. - Т. 5. - №. 4. - С. 350-361.
11.Royce W. W. Managing the development of large software systems (1970). - 2021.
12.Ball T. et al. Thorough static analysis of device drivers //ACM SIGOPS Operating Systems Review. - 2006. - Т. 40. - №. 4. - С. 73-85.
13.Heitmeyer C. On the need for practical formal methods //International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. - Berlin, Heidelberg : Springer Berlin Heidelberg, 1998. - С. 18-26.
14.Heitmeyer C. et al. Tools for constructing requirements specifications: The SCR toolset at the age of ten //International Journal of Computer Systems Science and Engineering. - 2005. - Т. 20. - №. 1. - С. 19-35.
15.Barnes J. G. P. High integrity software: the spark approach to safety and security: sample chapters. - Pearson Education, 2003.
16.Gupta A. Formal hardware verification methods: A survey //Formal Methods in System Design. - 1992. - T. 1. - C. 151-238.
17.Kern C., Greenstreet M. R. Formal verification in hardware design: a survey //ACM Transactions on Design Automation of Electronic Systems (TODAES). -1999. - T. 4. - №. 2. - C. 123-193.
18.Jacobi C., Berg C. Formal verification of the VAMP floating point unit //Formal Methods in System Design. - 2005. - T. 26. - C. 227-266.
19. Prasad M. R., Biere A., Gupta A. A survey of recent advances in SAT-based formal verification //International Journal on Software Tools for Technology Transfer. -2005. - T. 7. - C. 156-173.
20.Broy M. et al. Model-based testing of reactive systems //Volume 3472 of Springer LNCS. - 2005.
21.Boehm B., Basili V. R. Defect reduction top 10 list //Computer. - 2001. - T. 34. -№. 1. - C. 135-137.
22.Deimel L. Applying Program Comprehension Techniques to Improve Software Inspections //NINETEENTH ANNUAL SOFTWARE ENGINEERING WORKSHOP. - 1994. - C. 115.
23.Gilb T., Graham D. Software inspections. - Reading, Masachusetts : Addison-Wesley, 1993.
24.Porter A., Siy H., Votta L. A review of software inspections //Advances in Computers. - 1996. - T. 42. - C. 39-76.
25.Laitenberger O. A survey of software inspection technologies //Handbook of Software Engineering and Knowledge Engineering: Volume II: Emerging Technologies. - 2002. - C. 517-555.
26. Wong Y. K. Software Review History and Overview //Modern Software Review: Techniques and Technologies. - IGI Global, 2006. - C. 12-36.
27. ' 'IEEE Standard for Software Reviews and Audits," in IEEE Std 1028-2008 , vol., no., pp.1-53, 15 Aug. 2008, doi: 10.1109/IEEESTD.2008.4601584.,
28. Deutsch A. Static verification of dynamic properties //ACM SIGAda 2003 Conference. - 2003.
29.Almossawi A., Lim K., Sinha T. Analysis tool evaluation: Coverity prevent //Pittsburgh, PA: Carnegie Mellon University. - 2006. - С. 7-11.
30.Emanuelsson P., Nilsson U. A comparative study of industrial static analysis tools //Electronic notes in theoretical computer science. - 2008. - Т. 217. - С. 5-21.
31.Monin J. F. Understanding formal methods. - Springer Science & Business Media, 2012.
32.Котов В. Е., Черкасова Л. А. Исчисления процессов. I //Системы программирования. Теория и приложения. - 1993. - С. 6-38.
33.Hoare C. A. R. et al. Communicating sequential processes. - Englewood Cliffs : Prentice-hall, 1985. - Т. 178.
34.Milner R. (ed.). A calculus of communicating systems. - Berlin, Heidelberg : Springer Berlin Heidelberg, 1980.
35.Bergstra J. A., Klop J. W. Fixed point semantics in process algebras. - 1982.
36.Baeten J. C. M. (ed.). Applications of process algebra. - Cambridge : Cambridge university press, 1990. - Т. 4.
37.Milner R. Communicating and mobile systems: the pi calculus. - Cambridge university press, 1999.
38.Хопкрофт Д. Э., Мотвани Р., Ульман Д. Введение в теорию автоматов, языков и вычислений. - 2008.
39.Кузьмин Е., Соколов В. Структурированные системы переходов. - Litres, 2022.
40. Simon G. A., Kaufman D. J. An extended finite state machine approach to protocol specification //Proceedings of the IFIP WG6. 1 Second International Workshop on Protocol Specification, Testing and Verification. - 1982. - С. 113-133.
41.Dill D. L. Timing assumptions and verification of finite-state concurrent systems //Automatic Verification Methods for Finite State Systems: International Workshop, Grenoble, France June 12-14, 1989 Proceedings 1. - Springer Berlin Heidelberg, 1990. - С. 197-212.
42.Alur R., Dill D. L. A theory of timed automata //Theoretical computer science. -1994. - Т. 126. - №. 2. - С. 183-235.
43.Alur R. et al. The algorithmic analysis of hybrid systems //Theoretical computer science. - 1995. - Т. 138. - №. 1. - С. 3-34.
44.Henzinger T. A. The theory of hybrid automata //Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. - IEEE, 1996. - С. 278-292.
45. Дж П. Теория сетей Петри и моделирование систем. - 1984.
46.Гуревич Ю. Последовательные машины абстрактных состояний охватывают последовательные алгоритмы //Системная информатика. - 2004. - Т. 9. - С. 7-50.
47.Pratt V. R. Semantical considerations on Floyd-Hoare logic //17th Annual Symposium on Foundations of Computer Science (sfcs 1976). - IEEE, 1976. - С. 109-121.
48.Harel D., Kozen D., Tiuryn J. Dynamic logic //ACM SIGACT News. - 2001. - Т. 32. - №. 1. - С. 66-69.
49.Meyer B. Applying'design by contract' //Computer. - 1992. - Т. 25. - №. 10. - С. 40-51.
50.Floyd R. W. Assigning meanings to programs //Program Verification: Fundamental Issues in Computer Science. - Dordrecht : Springer Netherlands, 1993. - С. 65-81.
51.Dijkstra E. W. et al. A discipline of programming. - Englewood Cliffs : prentice-hall, 1976. - Т. 613924118.
52.Owicki S., Gries D. Verifying properties of parallel programs: An axiomatic approach //Communications of the ACM. - 1976. - Т. 19. - №. 5. - С. 279-285.
53. Clarke E. M., Emerson E. A. Design and synthesis of synchronization skeletons using branching time temporal logic //25 Years of Model Checking: History, Achievements, Perspectives. - 2008. - С. 196-215.
54.Browne A. et al. An improved algorithm for the evaluation of fixpoint expressions //Theoretical Computer Science. - 1997. - Т. 178. - №. 1-2. - С. 237-255.
55.Ben-Ari M., Manna Z., Pnueli A. The temporal logic of branching time //Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. - 1981. - С. 164-176.
56.Holzmann G. J. The SPIN model checker: Primer and reference manual. - Reading : Addison-Wesley, 2004. - Т. 1003.
57.Mateescu R., Sighireanu M. Efficient on-the-fly model-checking for regular alternation-free mu-calculus //Science of Computer Programming. - 2003. - Т. 46.
- №. 3. - С. 255-281.
58.Christensen S., J0rgensen J. B., Kristensen L. M. Design/CPN—A computer tool for coloured Petri nets //Tools and Algorithms for the Construction and Analysis of Systems: Third International Workshop, TACAS'97 Enschede, The Netherlands, April 2-4, 1997 Proceedings 3. - Springer Berlin Heidelberg, 1997.
- С. 209-223.
59.Nethercote N., Seward J. Valgrind: a framework for heavyweight dynamic binary instrumentation //ACM Sigplan notices. - 2007. - Т. 42. - №. 6. - С. 89-100.
60.Begik G. Testing J2EE Applications with IBM Rational PurifyPlus.
61.Reinders J. VTune performance analyzer essentials. - Santa Clara : Intel Press, 2005. - Т. 9.
62.Zhu H., Hall P. A. V., May J. H. R. Software unit test coverage and adequacy //Acm computing surveys (csur). - 1997. - Т. 29. - №. 4. - С. 366-427.
63.Utting M., Legeard B. Practical model-based testing: a tools approach. - Elsevier, 2010.
64. Ambert F. et al. BZ-TT: A tool-set for test generation from Z and B using constraint logic programming //Formal Approaches to Testing of Software, FATES 2002 workshop of CONCUR. - 2002. - Т. 2. - С. 105-120.
65.Tretmans J., Belinfante A. Automatic testing with formal methods. - 1999.
66.Кулямин В. В. и др. Подход UniTesK к разработке тестов //Программирование. - 2003. - Т. 29. - №. 6. - С. 25-43.
67.Engel C., Hahnle R. Generating unit tests from formal proofs //Tests and Proofs: First International Conference, TAP 2007, Zurich, Switzerland, February 12-13,
2007. Revised Papers 1. - Springer Berlin Heidelberg, 2007. - C. 169-188.
68.Rueher M. Automatic Test Data Generation using Constraint Solving Techniques.
- 1998.
69.Boyapati C., Khurshid S., Marinov D. Korat: Automated testing based on Java predicates //ACM SIGSOFT Software Engineering Notes. - 2002. - T. 27. - №. 4.
- C. 123-133.
70.Cavalli A., Gervy C., Prokopenko S. New approaches for passive testing using an extended finite state machine specification //Information and Software Technology. - 2003. - T. 45. - №. 12. - C. 837-852.
71.Barnett M., Schulte W. Runtime verification of. net contracts //Journal of Systems and Software. - 2003. - T. 65. - №. 3. - C. 199-208.
72.Barnett M. et al. Boogie: A modular reusable verifier for object-oriented programs //Formal Methods for Components and Objects: 4th International Symposium, FMCO 2005, Amsterdam, The Netherlands, November 1-4, 2005, Revised Lectures 4. - Springer Berlin Heidelberg, 2006. - C. 364-387.
73.Babic D., Hu A. J. Calysto: scalable and precise extended static checking //Proceedings of the 30th international conference on Software engineering. -
2008. - C. 211-220.
74.de Souza, Jovani Taveira, et al. "Data mining and machine learning in the context of sustainable evaluation: A literature review." IEEE Latin America Transactions 17.03 (2019): 372-382.
75.Taranto-Vera, Gilda, et al. "Algorithms and software for data mining and machine learning: a critical comparative view from a systematic review of the literature." The Journal of Supercomputing 77 (2021): 11481-11513.
76. Shekhar, Shashi, et al. "Spatial and spatiotemporal data mining." Gis Applications for Socio-Economics and Humanity. Elsevier Inc., 2017. 264-286.
77.Leemans, Sander JJ, Dirk Fahland, and Wil MP Van Der Aalst. "Discovering block-structured process models from event logs-a constructive approach." Application and Theory of Petri Nets and Concurrency: 34th International Conference, PETRI NETS 2013, Milan, Italy, June 24-28, 2013. Proceedings 34. Springer Berlin Heidelberg, 2013.
78.Leemans, Sander JJ, Dirk Fahland, and Wil MP Van Der Aalst. "Discovering block-structured process models from event logs containing infrequent behaviour." Business Process Management Workshops: BPM 2013 International Workshops, Beijing, China, August 26, 2013, Revised Papers 11. Springer International Publishing, 2014.
79.Leemans, Sander JJ, Dirk Fahland, and Wil MP Van der Aalst. "Scalable process discovery and conformance checking." Software & Systems Modeling 17 (2018): 599-631.
80. Weijters, A. J. M. M., Wil MP van Der Aalst, and AK Alves De Medeiros. "Process mining with the heuristics miner-algorithm." Technische Universiteit Eindhoven, Tech. Rep. WP 166.July 2017 (2006): 1-34.
81.Pourmirza, Shaya, Remco Dijkman, and Paul Grefen. "Correlation miner: mining business process models and event correlations without case identifiers." International Journal of Cooperative Information Systems 26.02 (2017): 1742002.
82.Przybylek, Michal R. "Skeletal algorithms in process mining." Computational Intelligence: Revised and Selected Papers of the International Joint Conference, IJCCI 2011, Paris, France, October 24-26, 2011. Springer Berlin Heidelberg, 2013.
83.Berti, Alessandro, and Wil MP van der Aalst. "A novel token-based replay technique to speed up conformance checking and process enhancement." Transactions on Petri Nets and Other Models of Concurrency XV. Berlin, Heidelberg: Springer Berlin Heidelberg, 2021. 1-26.
84.De Medeiros A. K. A. et al. Process mining: Extending the alpha-algorithm to mine short loops. - 2004.
85.Kwiatkowska M., Norman G., Parker D. Probabilistic model checking and autonomy //Annual Review of Control, Robotics, and Autonomous Systems. -2022. - T. 5. - pp. 385-410.
86.Karmakar R. Symbolic model checking: a comprehensive review for critical system design //Advances in Data and Information Sciences: Proceedings of ICDIS 2021. - 2022. - pp. 693-703.
87.O'Halloran B. M. et al. A graph theory approach to predicting functional failure propagation during conceptual systems design //Systems Engineering. - 2021. - T. 24. - №. 2. - pp. 100-121.
88.Zakarija I., Skopljanac-Macina F., Blaskovic B. Automated simulation and verification of process models discovered by process mining //Automatika: casopis za automatiku, mjerenje, elektroniku, racunarstvo i komunikacije. - 2020. - T. 61. - №. 2. - pp. 312-324.
89.Pasquadibisceglie V. et al. Using convolutional neural networks for predictive process analytics //2019 international conference on process mining (ICPM). -IEEE, 2019. - C. 129-136.
90.Weinzierl S. et al. An empirical comparison of deep-neural-network architectures for next activity prediction using context-enriched process event logs //arXiv preprint arXiv:2005.01194. - 2020.
91.Hanga K. M., Kovalchuk Y., Gaber M. M. A graph-based approach to interpreting recurrent neural networks in process mining //IEEE Access. - 2020. - T. 8. - C. 172923-172938.
92. Al-Jebrni A., Cai H., Jiang L. Predicting the next process event using convolutional neural networks //2018 IEEE International Conference on Progress in Informatics and Computing (PIC). - IEEE, 2018. - C. 332-338.
93.Nakano H. et al. Hardware-Accelerated Event-Graph Neural Networks for Low-Latency Time-Series Classification on SoC FPGA //International Symposium on Applied Reconfigurable Computing. - Cham : Springer Nature Switzerland, 2025. - C. 51-68.
94.Luo W. et al. Dynamic heterogeneous graph neural network for real-time event prediction //Proceedings of the 26th ACM SIGKDD international conference on knowledge discovery & data mining. - 2020. - C. 3213-3223.
95.Wein S. et al. Forecasting brain activity based on models of spatiotemporal brain dynamics: A comparison of graph neural network architectures //Network Neuroscience. - 2022. - T. 6. - №. 3. - C. 665-701.
96.Kose H. T. et al. Fully Quantized Graph Convolutional Networks for Embedded Applications //6th Workshop on Accelerated Machine Learning. - 2024.
97.Li A., Axhausen K. W. Short-term traffic demand prediction using graph convolutional neural networks //AGILE: GIScience Series. - 2020. - T. 1. - C. 12.
98. Jeziorek K. et al. Embedded graph convolutional networks for real-time event data processing on soc fpgas //arXiv preprint arXiv:2406.07318. - 2024.
99.Zoican S. et al. Graph-based neural networks' framework using microcontrollers for energy-efficient traffic forecasting //Applied Sciences. - 2024. - T. 14. - №. 1. - C. 412.
100. Zhou A. et al. Graph neural networks automated design and deployment on device-edge co-inference systems //Proceedings of the 61st ACM/IEEE Design Automation Conference. - 2024. - C. 1-6.
101. Cheng Y. et al. A survey of model compression and acceleration for deep neural networks //arXiv preprint arXiv: 1710.09282. - 2017.
102. Merone M. et al. A practical approach to the analysis and optimization of neural networks on embedded systems //Sensors. - 2022. - T. 22. - №. 20. - C. 7807.
103. Zhou A. et al. Graph neural networks automated design and deployment on device-edge co-inference systems //Proceedings of the 61st ACM/IEEE Design Automation Conference. - 2024. - C. 1-6.
104. Wu C. et al. A federated graph neural network framework for privacy-preserving personalization //Nature Communications. - 2022. - T. 13. - №. 1. -C. 3091.
105. Zhou A. et al. HGNAS: Hardware-Aware Graph Neural Architecture Search for Edge Devices //IEEE Transactions on Computers. - 2024.
106. Das A. et al. GraNNite: Enabling High-Performance Execution of Graph Neural Networks on Resource-Constrained Neural Processing Units //arXiv preprint arXiv:2502.06921. - 2025.
107. Zhang R. et al. Optimization Methods, Challenges, and Opportunities for Edge Inference: A Comprehensive Survey //Electronics. - 2025. - Т. 14. - №. 7. - С. 1345.
108. Shiri, Farhad Mortezapour, et al. "A comprehensive overview and comparative analysis on deep learning models: CNN, RNN, LSTM, GRU." arXiv preprint arXiv:2305.17473 (2023).
109. Xiao, Jue, Tingting Deng, and Shuochen Bi. "Comparative Analysis of LSTM, GRU, and Transformer Models for Stock Price Prediction." Proceedings of the International Conference on Digital Economy, Blockchain and Artificial Intelligence. 2024.
110. Peng, Hao, et al. "Dynamic graph convolutional network for long-term traffic flow prediction with reinforcement learning." Information Sciences 578 (2021): 401-416.
111. Zheng, Chuanpan, et al. "Spatio-temporal joint graph convolutional networks for traffic forecasting." IEEE Transactions on Knowledge and Data Engineering 36.1 (2023): 372-385.
112. Tay, Yi, et al. "Efficient transformers: A survey." ACM Computing Surveys 55.6 (2022): 1-28.
113. Fournier, Quentin, Gaétan Marceau Caron, and Daniel Aloise. "A practical survey on faster and lighter transformers." ACM Computing Surveys 55.14s (2023): 1-40.
114. Ravi Kumar, P., K. L. Alex Goh, and K. S. Ashutosh. "Application of Markov Chain in the PageRank Algorithm." Pertanika Journal of Science & Technology 21.2 (2013).
115. Burks, David J., and Rajeev K. Azad. "Higher-order Markov models for metagenomic sequence classification." Bioinformatics 36.14 (2020): 4130-4136.
116. Carletti, Timoteo, Duccio Fanelli, and Renaud Lambiotte. "Random walks and community detection in hypergraphs." Journal of Physics: Complexity 2.1 (2021): 015011.
117. Rahimi, Seyyed Mohammadreza, et al. "Optimized random walk with restart for recommendation systems." Canadian Conference on Artificial Intelligence. Cham: Springer International Publishing, 2019.
118. Table miner GitHub. URL: https://github.com/GoncharovAleshka/table_miner.
Приложение А. Акт внедрения результатов работы на практике
Акт о внедрении результатов работы по проекту «Ретранслятор ДМВ/МВ» в ООО «СТЦ»
Обтссгво с ограниченной ответственностью «Специальный Технологический Центр» (ООО «СТЦ»)
пр-кт Непокоренных, д. 17, к. 4, литера В. помет. ЗН,
Вй.тер.г. муниципальный округ Пнскаревка,
г. Ca нк!-Петербург, 19522(1 Тел. (812) 244-33-13, Тел./факс (812) 535-77-111), (812)535-58-16 E-maii: OfTice@stc-spb.ru
ОКНО 56234690, ОГРН 1037804018614 ИНН/КПП 7802170553/780401001
_.Nj_
на .Ys
УТВЕРЖДАЮ
Н ачал ьн и к н ап рав лен ия разработок беспилотных авиационных систем
Е.Д. Плужников
ь^щ&ш2025 г-
. _____
АКТ О ВНЕДРЕНИИ
результатов кандидатской диссертационной работы Гончарова Алексея Андреевича на тему «Методы восстановления и анализа формальной модели наблюдаемого поведения для процессов
во встроенных системах»
Настоящим подтверждается, что теоретические и практические решения, предложенные Гончаровым A.A.. в диссертационной работе, применялись в практической деятельности отдела разработки электроники Беспилотных Авиационных Систем и Целевого Оборудования в ходе работ по проекту «Ретранслятор ДМВ/МВ» в части средства динамической актуализации формальной модели наблюдаемого поведения встроенных систем.
Применение разработанных методов позволило наблюдать за поведением исследуемых встраиваемых систем с ограниченными ресурсами автономно на протяжении длительных периодов непрерывной работы (дни, недели), а также оценивать функциональное покрытие, вероятность пребывания системы в заданных состояниях, учитывать частотные характеристики состояний, определять последовательность событий, которая привела к отказу.
204 Публикации
1. Goncharov A., Bykovskii S., Belozubov A., Shibaev A. Heuristic Algorithm for event prediction in Embedded Systems // 2025 International Conference on Artificial Intelligence, Computer, Data Sciences and Applications (ACDSA) -2025, pp. 1-6
2. Goncharov A., Bykovskii S., Kustarev P., Zhdanov A. Dynamic Actualization of Formal Model for Microcontrollers Software // Lecture Notes in Electrical Engineering - 2024, Vol. 1253, pp. 611-618
3. Гончаров А.А., Быковский С.В. Метод динамической актуализации модели взаимодействия параллельных процессов во встроенных системах // Известия высших учебных заведений. Приборостроение - 2024. - Т. 67. - № 9. - С. 741-750
4. Гончаров А.А., Быковский С.В. Метод восстановления модели процессов во встроенных системах по журналу событий // Известия высших учебных заведений. Поволжский регион. Технические науки - 2023. - № 3(63). - С. 517
Proc. of International Conference on Artificial Intelligence, Computer, Data Sciences and Applications (ACDSA 2025)
7-9 August 2025, Antalya-Turkiye
Heuristic Algorithm for event prediction in Embedded
Systems
Alcksci Goncharov School of Computer Technologies and Control ITMO University St. Petersburg, Russia 0000-0001-8742-0961
Sergei Bykovskii School of Computer Technologies and Control ITMO University St. Petersburg, Russia 0000-0003-4163-9743
Alexander Belozubov School of Computer Technologies and Control ITMO University St. Petersburg, Russia 0000-0002-7594-5020
Andrey Shibaev School of Computer Technologies and Control ITMO University St. Petersburg, Russia 0009-0008-5207-4876
Abstract— This paper presents the results of a comparative analysis of methods without the use of neural networks (Weighted Random Walk, Specific Pattern Search, and 3rd order Markov chain), graph ^involutional neural network (GCN), and the proposed heuristic algorithm for the task of predicting the next node in weighted oriented matrices. A heuristic algorithm was also proposed that uses a combination of edge weights and node characteristics. For each potential next node, the following information is collected: edge weight, node outdegree (number of outgoing edges), node indegree (number of incoming edges). Based on this information, a prediction is made. The considered weighted matrix is the output information of the embedded system, representing an updated model of the processes of the embedded system itself. The analysis of the obtained data is assumed outside the system itself. The experiments use synthetic data, fn the study, matrix sizes from 5x5 to 300x300 with 20 iterations for each proposed algorithm are used as initial data. As a result of the comparison, the following metrics are obtained: prediction speed, accuracy, required memory, and training time. Recommendations for the application of the methods discussed are given, and the effectiveness of the proposed heuristic algorithm is also shown. The work serves as a practical guide to choosing an approach in the tasks of analyzing the structure of a graph built based on a weighted adjacency matrix.
Keywords— graph neural networks, next event prediction, embedded system, Markov chain, GCN, heuristic algorithm.
I. Introduction
Predicting the next node or event in a graph is a key problem in graph data mining [1]. This problem involves predicting which node or event is most likely to occur next in a sequence represented by a graph. The fundamental importance of this problem stems from its wide application in a variety of fields, including recommender systems [2], where the next product or service that a user may be interested in is predicted; social network analysis, where the next interaction between users or the dissemination of information is predicted; time series forecasting [3], where graphs are used to model dependencies between different time sequences; anomaly detection [4], where unexpected transitions or events in a graph may indicate abnormal behavior; and modeling biological processes [5], such as protein interactions or mctabolic pathways. The ability to determine the next state of a graph in advance enables proactive action, improved recommendations, optimized workflows, and deeper understanding of the dynamics of complex systems represented by a graph structure. The next node prediction
problem is closely related to the link prediction problem, which focuses on determining the probability of future edges between nodes, and the sequential recommendation problem, which takes into account the order of user interactions with items to predict the next preferred item, in turn, next event prediction can be considered as a special case of node prediction in time graphs, where events or changes in the graph themselves are represented by nodes.
Graphs used to model systems can have different characteristics [6]. They can be static, where the structure and properties of the graph do not change over time, or dynamic (temporal), where nodes, edges, and their attributes can evolve [7]. Graphs can also be weighted, with weights assigned to edges to reflect the strength or cost of the link, or unweighted, where all links are considered equal. Directed graphs have edges with a specific direction indicating a one-way link, while in undirected graphs the link between two nodes is reciprocal. In addition, graphs can be homogeneous, containing nodes and edges of the same type, or heterogeneous, including different types of nodes and edges with different properties. The type of graph has a significant impact on the choice of the most appropriate prediction method. Prediction problems can also be formulated in a variety of ways, including predicting the next node in a sequence of user actions in a static graph, predicting the cmcrgcnce of new links or nodes in evolving time graphs, predicting the next event in a cause-and-effect graph of events, and predicting specific properties of a future node or event.
This paper reviews existing methods for predicting the next node or event in graphs, including both classical algorithms and modern neural network-based approaches. The paper will cover in detail models using random walks, Markov chains and graph neural networks (GCNs). These approaches will be compared based on key criteria such as prediction accuracy, computational complexity, data requirements, applicability to different types of graphs, interpretability, and the ability to handle event sequences. The paper concludes by summarizing the main results.
The considered weighted matrix is the output information of the embedded system, representing an updated model of the processes of the embedded system itself. The analysis of the obtained data is assumed outside the system itself, although consideration of the issues of performance and memory requirements can allow us to understand the possibility of analyzing the adjacency matrix on the target model itself.
979-8-3315-3562-9/25/s31.00 ©2025 ieee
II. Problem statement
The input to the prediction is a weighted adjacency matrix, where the values represent the number of transitions between events. The rows and columns of the matrix are events, and the values in a cell represent the number of transitions between events. The main difficulty with prediction is the lack of explicit time stamps for events. The lack of time stamps means that the method or algorithm must implicitly infer temporal relationships from the transition patterns themselves. This may involve identifying frequent transition sequences or understanding the overall process flow through the graph structure defined by the weighted adjacency matrix. The method or algorithm must learn to recognize event patterns directly from the connectivity and weights.
III. Literature review
A. Approaches using neural networks
Recurrent neural networks (RNN: LSTM, GRU) are specialized for processing sequential data [8]. They consider the context due to the "memory" of previous elements of the sequence. To use a weighted adjaccncy matrix, it is necessary to first generate training sequences, for example, using random walks on the graph. The model learns to prcdict the next event based on the sequence of previous events fed to it. To predict chains of events, they can work in generative mode, predicting event after event [9].
Graph neural networks (GNN) are designed specifically to work with graph data. They consider both the properties of nodes and the structure of links and their weights [10]. They can work directly with the adjacency matrix. Predicting the next event can be formulated as a link prediction problem or classification of the next node based on the current state and structure of graph [11]. Predicting a chain of events requires additional mechanisms, such as combining GNN with RNN or using GNN to predict transition probabilities at each step and then generating a sequence.
Transformers are designed for natural language tasks but have been successfully applied to other sequential data due to an attention mechanism that allows the model to weigh the importance of different elements in the input sequence [12]. Like RNNs, they require graph-to-sequence transformations for training. Next-event and chain prediction are like RNNs but are potentially better for long dependencies. They are more complex and data- and resource-intensive [13].
For the given comparative analysis task presented in Table 1, we will choose GNN. GNNs are designed specifically for graph data and can directly work with the weighted adj acency matrix, considering the edge weights and graph topology. They are potentially capable of capturing complex dependencies. They are more natural for this task than RNNs or Transformers, which require preliminary transformation of the graph into sequences. GNNs provide a balance between the ability to model complex structures and direct work with the graph representation of the process.
The principle of operation of GNN for predicting the next event: at the training stage, the input is a fully weighted adjacency matrix defining the structure of the graph, node
features, and training examples - pairs of the form current event -> next event. Such pairs can be extracted from the adjacency matrix, for example, by randomly walking the graph taking into account the edge weights. The output at the training stage will be the prcdictcd probability distribution over all possible next events for each training example. At the prediction stage, the input to the trained model will be the current event for which a prediction must be made, and the output will be a probability distribution over all possible next events or one most likely next event. GNN is defined by the following set: GNN loss — (G, T), where G = (N, E) — a graph defined by sets of vertices N and connections/;, and T = (ft;, t;) - a set of pairs where n, — vertex of a set N, and t- the target variable associated with this node. Node embedding update formula v on the layer f +1 :
h^=f(wr
AGGREGATE ({ft®|u e neighbours(v)J^ where h[P -node embedding v. W[ layer weights, f - activation function.
TABLE I. Comparison of meurai-metwose methods
Method RNN GNN Transformers
Complex ity training High High Vciy high
use Medium Medium Medium
Memory requirements High High Very high
Predictio ii next event + + +
event chains + + +
Intcrpretabilitv Low Medium Medium
Accounting of weights Implicitly + Implicitly
B. Approaches without using neural networks
First-order Markov chains model a process as a sequence of random events, where the probability of transition to the next state depends only on the current state [14]. The adjacency matrix is directly used to determine the transition probabilities. The probability of each possible next event is determined by the corresponding value in the normalized transition matrix for the current state. To prcdict the chain, events can be generated by sequentially choosing the next state based on the transition probabilities from the current state.
Higher-order Markov chains take into account not only the current state, but also several previous states (chain order) to predict the next one, for example, a 2nd-order chain takes into account the last two events [15]. Predicting the next event depends on the combination of the last k states, where k is the chain order. Requires constructing a more complex state model. Predicting a chain of events is similar to lst-order chains, but based on transition probabilities for higher-order states.
Weighted Random Walks simulate a "trip" through a graph where the probability of moving from a node to its neighbor is proportional to the weight between them [15]. The probability of moving to a neighboring event j from the current i is proportional to the weight of the edge (£,/). Predicting a chain of events is modeled by simulating a random walk several steps ahead [16].
Frequent Pattern Mining algorithms: Methods like PrefixSpan, GSP can be adapted to find frequent transition sequences in data by generating a path (random walk) and searching for patterns in them [17]. Weights can be used to generate more probable paths. Based on the found partial sequences ending with the current event, the most probable next events can be predicted. The found partial sequences themselves are predicted chains of events.
TABLE II. Comparison of approaches without usinq neural networks
Method Markov chain of the first order Higher order Markov chain Weighted random walks Frequent Pattern Mining
Algorithmic complexity Low Medium Low Medium / High
Memory requirements Low Medium /High Low Medium
Prediction next event + + + + (limited)
event chains + + (simulation) +
Interpret ability High Medium High High
Accounting of weights + + + Indirectly
C. The proposed heuristic algorithm
A heuristic algorithm using a combination of edge weights and node characteristics was also proposed. A row corresponding to the current node is extracted from the adj acency matrix, and indices of nonzero elements in this row are found. For each potential next node, the following information is collected: edge weight, node outdegree (number of outgoing edges), node indegree (number of incoming edges). Then the candidates are sorted in descending order with priorities according to the list: edge weight, next node outdegree, next node indegree, and if all parameters match, a random selection occurs. The first element of the sorted list is selected as the expected next node.
Mathematical description: let G = (V, E, W) be a directed
weighted graph, where: V = {0,1.....n — 1} is the set of
vertices (nodes), with n = |V| . E V x V is the set of directed edges. W : E -» R+ is the weight function, where tv(i,y) is the weight of edge (i,j) E E. If (i,j) g E, then w(l,j) — 0. The graph is represented by an n xn adjacency matrix A , where ALj = w(i,j) if (i, j) F E , and Atj = 0 otherwise. Given a current node i E V, the heuristic algorithm predicts the next node j E V based on the weights of outgoing edges from i and the degrees of neighboring nodes. Algorithm description:
1. Input validation: if i is undefined, i < 0 or ! > n return 0 (no prediction).
2. Identify candidate nodes: define the set of candidate nodes as: C = {j E V \Ai s > 0}. If C = 0, return 0.
3. Compute node characteristics: for each j E C , compute:
• Edge weight: Wj — Atj.
• Outgoing degree: d* = ¡{/c e V\AjJc > 0j|.
• Incoming degree: dj = |{fc E V\Akj > 0}|. Form a tuple for each candidate: (j, Wj, df, dj).
4. Sort candidates: order the set of tuples {{j,Wj,df,dj)\j e C} lexicographically by: (—Wj, —df, — dj~,rj") , where Tj ~ Uniform (0,1) is random value used as a tiebreaker. The prioritization order (edge weight > out degree > in degree) is a critical design choice. Suboptimal prioritization in specific real-worid scenarios with complex dependencies could reduce accuracy.
5. Output: return the node j from the first tuple in the sorted list.
Therefore, algorithm returns j E V such that (i,j) £ E , prioritizing:
• Maximum edge weight w(£, j).
• Maximum outgoing degree d
• Maximum incoming degree dj.
• Random selection for ties. If no such j exists, it returns 0.
IV. Tests environment
In a test environment, a comparative analysis of several algorithms designed to predict the next node in a graph structure was conducted. The graph is represented as an adjacency matrix, where non-zero values in the cells indicate the presence of an edge from node to node with a certain weight. At the first stage, graphs of various sizes with random connections and weights are created synthetically. For each generated graph, correct predictions for each node are determined.
The following methods are compared:
- 3ld order Markov chain;
- Weighted Random Walk;
- Specific Pattern Search; -Neural Network (GCN). Algorithm SPS:
Formal model: Let G — (V, E) weighted directed graph, where:
• V - set of vertices (nodes)
• E c Vx V- set of edges
• w\ E -» R+ - edge weight function
The SPS algorithm is defined as a tuple (M,/p,/c), where:
1. Pattern model M Q V X V xV is built like:
M = {(u, v, w) I u = ar g ma x w(x, v) , w = label(v),x e V} where:
• label{v) - target vertex predicted by the base algorithm
• u - most likely predecessor V (maximum input weight)
2. Prediction function fp: V x V -» V:
Iw if (u, v, ivl e M
Where fc - fallback-function (2rd order Markov chain)
3. Correctness conditions:
• Vv 6 V, degi„(v~) > 0 - non-isolated vertices
• 3! u — arg max w(x, t?) - unique predecessor
A graph convolutional network with two layers. The input layer of the first layer is n, the output for the first layer is n x hidden layer multiplier as is the input for the second and, accordingly, the output of the second layer is n, where n is the number of rows or columns for an n X n matrix. The model is trained to predict labels based on the graph structure and node features (in this case, unit vectors are used as features). Tested with different numbers of neurons in the hidden layer.
The tests are performed for graphs of different sizes. Matrices from 5x5 to 300x300. For GCN, the following hidden layer multipliers are tested: 1, 3, and 5. For each combination of graph size and compared method, the tests are performed multiple times (20) to obtain more reliable results.
The mathematical description of the generation of test matrices can be described as follows:
Adjacency matrix A , where
если есть ребро i -> j 0
■ Uniform (1,2
,9}.
outcome
Matri ПсиИ 3"1 \VR SPS GCN GCN GCN
x size stic order Merk ov W k=l k=3 k=5
5 1.0 1.0 1.0 1.0 0.975 1.0 1.0
II) 1.0 11.940 (1.988 0.997 0.990 1.0 1.0
20 0.993 0.842 0.977 1.0 0.995 1.0 1.0
5(1 0.998 0.603 0.970 1.0 1.0 1.0 1.0
11» 0.998 (1.367 0.969 1.0 0.962 0.964 1.0
200 0.999 0.169 0.968 1,0 0.103 0.601 0.879
31Ю 0.99S (1.092 0.975 1.0 0.043 0.070 0.460
.DB
I
■г..
Comparison ol Diedlcllon accuracy
• Degree of node
i'degout{i) £ [max(l,~),max(21~)].
The execution time (model building/training and prediction/inference), prediction accuracy, and memory consumption for each algorithm are measured. The results of individual runs are collected and averaged, and 95% confidence intervals for Ihe metrics are calculated.
Thus, the test environment allows us to empirically compare the effectiveness of different approaches to the problem of predicting the next node in graphs of different complexity and size.
V. Expreimental results and recommendations
All experiments were conducted in the Google Colab cloud environment (free version) using a virtual machinc with an Intel Xeon processor, RAM, and an optional NVIDIA Tesla T4 graphics accelerator. The operating system was Ubuntu. The experiments utilized TensorFlow, PyTorch, NumPy, Pandas, Matplotlib, and standard Python 3 libraries pre-installed in the Colab environment for machine learning tasks.
Malri* rI'jiji.ir-ir,i wiilr j
. HeuNsuc algarltnm - 5p«Hii Pattern Meura Netwont [GCN}K*3,0
' 3rd erDur Markau chair Neural Wrrhworfc (GCN) k-1.0 Neural ffiCN) 0
Weights R&rwwr wtik
Fig. 1 Comparison of prediction accuracy
The graph shows how the algorithms maintain accuracy as the matrix size increases. Heuristics and SPS lead in accuracy, especially on large matrices. 3rd order Markov chains and neural networks are less effective for large graphs withoul additional tuning.
TABLE IV. Experimental results: Prediction/Inference time {seconds]
Ma h i Henri 3rd \VR SPS GC'N GCN GCN
x size Stic ordci Mark ov W k=l k=3 k=5
5 0.000 0.000 0.000 0.000 0.000 0.000 0.001
03333 Oil 14 06776 00816 60140 614S0 08453
10 0.000 0.000 0.000 0.000 0.000 0 000 O.OOO
25065 02310 10001 00216 49503 49763 96263
20 0.001 0.000 0.000 0.000 0.000 0.000 0.001
30507 05044 64131 00904 56637 56637 09440
50 0.008 0.000 0.003 0.000 0.000 0 000 0.001
92777 49881 61664 01003 80680 80680 45188
100 0.037 0.001 0.014 0.000 0.003 0.003 0.005
45736 06231 94975 02310 56100 56100 61333
200 0,125 0.003 0.062 0.000 0.021 0,021 0.035
78034 75895 84784 10032 11313 11313 34811
300 0284 0.011 0.137 0.000 0.088 0.088 0.148
43360 00779 34555 33283 00220 00220 99349
TABLE III.
Experimental results: Prediction Accuracy
s lo-1
£
¡10-s
ïli-
Comparison of predlctlon/lnlenence time
la rtstlt algunrhn ; i iiir i- MmkQN drain
I - I- 1 RanODm .'J- .
Neural '■ ">■■ art |r,r fj, h-^.p flcurnl NctwarkiGCtlHi-SO
Fig. 2. Comparison of prediction/inference time
The graph shows the speed of predictions. Heuristics are ideal for real-time applications. 3rd order Markov chains are the least suitable, and WRW and SPS offer a good balance of speed and accuracy.
In terms of the possibility of placement on the target platform itself, for example, on a microcontroller, the most attractive in terms of algorithmic complexity, judging by the data obtained, is SPS. SPS can potentially allow predictions to be made in real time. To clarify this possibility, experiments must be carried out on the target platform.
a problem and can be a critical drawback at runtime. The proposed heuristic algorithm is free from this drawback.
TABLE VI. Experimental results: Memory consumption (Bytes)
Matri Heuri 3rd Wit sps GCN GIN gcn
x size Stic order W k=l k=3 IFS
Mark
ov
5 200 S61 20(1 652 457 911 1347
to 800 4776 800 1520 1916 3568 5240
2(1 3200 42438 3200 4480 7624 14144 20732
50 20000 64916 8 20000 24544 47626 88136 I2S33 4
IM 80000 54752 80000 89392 18962 35128 51173
32 S 4 2
2(10 32000 42862 32000 33862 75795 14008 20429
0 384 0 4 6 34 94
311« 72000 1698Ï 72000 73862 17075 31437 45859
0 2392 0 4 80 60 40
Memory consumption comparison
TABLE V.
Experimental results: Buildint/training time
(seconds)
Matrix 3rd order SPS GCN GCN GCN
size Markov k=l k=3 k=5
5 0,00003335 0.00010072 0.21876 0.23732 0,23255
10 0.00065257 0.00011684 0.21876 0.23732 0.23268
2(1 0.00885948 0.00023324 0.23732 0.25588 0.25216
SO 0.35975821 0.00039953 0.34675 0.36562 0.35744
100 5.44221542 0.00097482 1.65476 1.72061 1.72663
200 88.74852 0.00165402 10.1586 10.5208 10.5700
300 453.43428 0.00301409 32.4506 38.2060 51.3372
comparison or mortel Biilldlng/lralning time
W.. II ». .Oi I l'i .11 .ll I
-» HQ onlcrMarKov chain -1 i fn pattern .. . I
Neural nework fGCNI H-3 :i
Matrix see (tooaritlthili: nrcc;
Fig. 3. Comparison of model building/training time
The graph estimates the time spent on preparing models. SPS stands out for its efficiency, while 3rd order Markov chains and neural networks require significant time costs, which limits their applicability. In terms of deployment and use on the target platform, the need to build a model for SPS can potentially be
Hni'-i^lt algorithm M WflCt M »-f. cTiiiri Weighted r.mu'.i Walk
Fig. 4. Memory consumption comparison
The graph shows how the algorithms scale in memory usage with increasing matrix size. Heuristics and SPS are the most memory efficient for large matrices, while 3rd order Markov chains become unacceptable due to exponential growth, neural networks require significant resources especially with a high hidden layer multiplier.
Narrow confidence intervals across all metrics for heuristics atid SPS indicate stable performance. Wide confidence intervals for the Markov chain and neural network may be a problem in production environments that require accuracy.
The choice of algorithm or method for application and placement requires more detailed analysis and testing on the target device. Of the methods and algorithms considered, SPS appears to be the most balanced in all characteristics, accurate, fast and relatively undemanding to memory resources, bul the need to build a model can be a critical drawback. The proposed heuristic algorithm does not require building a model and immediately works with the matrix, which can be a strong advantage for resource-limited systems.
The SPS algorithm requires a model building (pattern search) step that can be performed on a more powerful computing device and the model itself can be added to the embedded system by updating the device firmware or on demand. The resulting model (set of patterns) is then loaded
into the device memory (ROM/RAM) for fast prediction. The proposed heuristic algorithm, due to the absence of a training step and low memory/computation requirements, is ideal for direct integration into resource-constrained embedded systems. It can be implemented as a compact C library that takes as input the current adjacency matrix and returns a predicted node.
VI. Limitations of the Heuristic Approach
Limitations of the Heuristic Approach: While demonstrating strong performance in the evaluated synthetic scenarios, heuristic methods like the one proposed face inherent challenges:
• Accuracy in Complex Systems: Performance may degrade in environments with highly stochastic, nonlinear, or context-dependent event transitions that cannot be fully captured by local node/edge features alone.
• Parameter Sensitivity: The prioritization scheme (weight > out degree > in degree) is a fixed heuristic. Its optimality depends on the underlying proccss dynamics; different embedded system behaviors might benefit from alternative feature combinations or weighting schemes, requiring domain knowledge for hining.
VII. Conclusions
The results highlight the importance of choosing an algorithm based on specific requirements. For small matrices, all algorithms perform well, but heuristics and SPS are preferred due to their efficiency. Oil large matrices, heuristics and SPS can also be recommended due to their scalability and stability. Neural networks can be considered if resources are available but require further development for large matrices. Markov chains should be avoided due to their poor scalability.
Although the proposed heuristic algorithm demonstrates high accuracy on synthetic data, its effectiveness may decrease in real systems with stochastic processes, where transition patterns are less regular.
The current experiments are performed on synthetic data for a controlled scalability assessment. In future work, it is critical to validate the methods on real event logs from industrial embedded systems (e.g., IoT controller or ICS logs) to assess their applicability in practical conditions.
The developed heuristic algorithm demonstrated high accuracy comparable to the best algorithms considered, but was inferior in performance on large matrices, having the lowest memory requirements.
Issues related to the choice of algorithm or method for deployment and use on the target platform require separate
research. The developed heuristics looks most interesting due to the lack of need to build a model, but the prediction speed is inferior to SPS, which can be a problem for real-time systems, where accurate and fast prediction can be a key factor.
[1] Hamilton. William L. Graph representation learning. Morgan & Claypool Publishers, 2020.
[2] Ying. Rex, et al, "Graph convolutional neural networks for web-scale rccommcndcr systems." Proceedings of the 24th ACM SICiKDD international confcrcncc on knowledge discovery & data mining. 2018.
[3] Wu, Zonghan, et al. "Connecting the dots: Multivariate time series forecasting with graph neural networks." Proceedings of the 26th ACM S1GKDD international conference on knowledge discovery & data mining. 2020.
[4] Akoglu, Leman, Ilanghang Tong, and Dana: Koutra, "Graph based anomaly detection and description: a survey." Data mining and knowledge discovery 29 (2015): 626-688.
[5] Zitnik, Marinka, et al. "Machine learning for integrating data in biology and medicine; Principles, practice, and opportunities." Information Fusion 50(2019); 71-91.
[6] Zhou, .Tic, el al. "Graph neural networks: A review of methods and applications." AI open 1 (2020): 57-81.
[7] Kumar, Srijan, Xikun Zhang, and Jure Lcskovcc. "Predicting dynamic embedding trajectory in temporal interaction networks." Proceedings of the 25th ACM SIGKDD international conference on knowledge discovery & data mining, 2019
[8] Shiri, Farhad Mortezapour, et al "A comprehensive overview and comparative analysis on deep learning models: CNN, RNN, LSTM. GRU." arXiv preprint arXiv:2305.17473 (2023).
[9] Xiao, Jue, Tingting Deng, and Shuochen Bi. "Comparative Analysis of LSTM, GRU, and Transformer Models for Stock Price Prediction." Proceedings of the International Conference on Digital Ecunomy, Bloekehain and Artificial Intelligence. 2024.
[10] Peng, Hao, et al. "Dynamic graph convolutional network for long-term traffic flow prediction with rcinforccmcnt learning." Information Sciences 578 (2021): 40M16.
[11] Zheng, Chuanpan, et al. "Spatio-temporal joint graph convolutional networks for traffic forecasting." IEEE Transactions on Knowledge and Data Engineering 36.1 (2023): 372-385.
[12] Tay, Yi, et al. "Efficient transformers: A survey." ACM Computing Surveys 55.6 (2022): 1-28.
[13] Foumier, Quentin, Gaétan Marceau Caron, and Daniel Aloise. "A practical survey on faster and lighter transfonners." ACM Computing Surveys 55.14s (2023): 1-40.
[14] Ravi Kumar, P., K. L. Alex Goh, and K. S. Ashutosh. "Application of Markov Chain in the PagcRank Algorithm." Pcrtanika Journal of Scicnec & Technology 21.2 (2013 ).
[15] Burks, David I., and Rajecv K. Azad. "Higher-order Markov models for mctagcnomic scqucncc classification." Bioinformatics 36.14 (2020): 4130-4136.
[16] Carletti, Timoteo. Duccio Fanelli, and Renaud Lambïotte. "Random walks and community detection in hypergraphs." tournai of Physics: Complexity 2,1 (2021): 015011.
[17] Raili ini. Seyyed Mohammadreza, et al. "Optimized random walk with restart for recommendation systems." Canadian Conference on Artificial Intelligence. Cham; Springer International Publishing. 2019.
References
®
Check for updates
Dynamic Actualization of Formal Model for Microcontrollers Software
Aleksei Goncharov'®1, Sergei Bykovskii, Pavel Kustarev, and Andrei Zhdanov
ITMO University, 49 Kronverksky Pr„ St. Petersburg 197101, Russia
aagoncharovgitmo.ru
Abstract. The article proposes a method for dynamically updating a formal model of the process for debugging and verifying microcontroller software. The method is based on process mining technology and allows to record the observed behavior of the system in the form of a formal model, updating the process model in real time. This saves memory resources, preserves the cause-and-effect relationship between events, and allows to monitor systems with limited access. The effectiveness of the proposed method is demonstrated on a development board based on the STM32F103C8T microcontroller. The method is applicable for systems with memory of tens of KB and operating at a frequency of several MHz. The method is implemented as a library in C languages. A comparison is made with an approach based on the accumulation and post-processing of an event log. The lime to add an event to the system, the time to update the model, and the amounl of memory required to store information about the behavior of the system were estimated. Method allows to obtain models of processes in embedded systems in real time on limited resources, carry out software verification, determine the reachability of individual system states, and determine the causes of failures.
Keywords: Verification • Formal process model ■ Embedded systems ■ Microcontrollers • Process mining
1 Introduction
Microcontrollers are an integral part of many modern devices, including industrial control systems, household appliances, medical equipment and many others [1,2]. When developing software for microcontrollers, ensuring the correct operation of the device is critical, especially under severe resource constraints [3]. This can he a difficult task, as even small software errors can cause serious problems with the device.
Formal analysis methods, including formal verification, are effective ways to verify the correct operation of microcontroller software [4]. However, a formal process model drawn up at the design stage cannot reflect all the features of real operation. Thus, the current tasks are to obtain a formal model of the observed behavior during system operation and to verify the properties of the specification in relation to this model, including comparing it with the model of expected behavior. This becomes especially relevant at the stage of full-scale testing of the system. In this regard, a means of dynamically
© The Autbor(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2021 Y. S. Shmaliy (Ed ): CCIE 2024. LNEE 1253. pp. 611-618, 2024. https://doi.org/10.1007/97 8-981 -97-6937-7J75
updating a formal model ofobserved behavior becomes an important tool for monitoring system performance over time. Dynamic updating refers to the creation of a model using built-in tools during system operation.
Process mining is a business process analysis methodology basedon real process dala obtained from electronic document management systems, business process management (BPM). information systems (ERP and CRM) and other systems. This methodology allows to identify and analyze hidden processes of system behavior and performance, identify its problems, improve processes and increase business efficiency [5]. Using the result of data analysis, it is possible to restore formal models and visualize processes using graphs and diagrams that will reflect ongoing processes and help in making the right strategic decisions [6, 7]. Process mining is an important tool for modernizing, optimizing business processes and improving the quality of products and services.
The scientific literature presents various options for using process mining methods in relation for embedded systems. For example, the authors of article [8] present the possibility of using process mining methods for medical devices. Analysis of data received from devices occurs outside the systems in question. The possibility of using the above methods for process automation (Robotic Process Automation) is discussed in article [9], but the accumulation and analysis of data occurs outside the target platform.
The following work 110] examines the possibility of detecting cyberattacks in industrial systems through the use of data mining methods. In this work, data analysis also occurs outside the systems under consideration.
Works 111-131 demonstrate the use of process mining for compliance testing and performance analysis. The main result of these studies is the fact that the use of the proposed methods facilitates the evaluation and audit of software processes.
2 Proposed Methods for Dynamic Updating of a Formal Model
Based on the analysis of the previously discussed tools, the requirements for the tool being developed were determined: the tool should allow to create and update a formal process model in real time based on data received from the microcontroller and allow to obtain process model.
In [14], the authors developed a method for restoring a formal model from an event log for embedded systems. The developed method included the following steps: collecting event logs from system components; combining event logs into a single system event log; searching for common dependencies between actions using an inductive algorithm; detection of frequency characteristics using an equalization algorithm. Figure 1 shows the described method with all the steps, inputs and outputs.
Devices based on microcontrollers often operate autonomously for a long time. Thus, the event log collection subsystem will require a significant amount of memory to store information about all observed events during the entire period of autonomous operation. The presented method has a clear disadvantage in the use of memory resources, and also requires relatively high performance from the target platform. For example, when calculating a formal model of thousands of events, the required calculation time can reach hundreds of milliseconds, which can be a serious drawback for real-time systems. This approach does not pose a significant problem if use an external instrument computer to process and save data but is not applicable for implementation using microcontrollers.
Dynamic Actualization of Formal Model 613
»•........ ^SBl] i-- ii I-—•] I .rv
1 Virgin i,
MMJI »i«»i ..........
Обратите внимание, представленные выше научные тексты размещены для ознакомления и получены посредством распознавания оригинальных текстов диссертаций (OCR). В связи с чем, в них могут содержаться ошибки, связанные с несовершенством алгоритмов распознавания. В PDF файлах диссертаций и авторефератов, которые мы доставляем, подобных ошибок нет.