Registration Number
0826U000667, PhD dissertation
Status
Доктор філософії
Date
13-04-2026
popup.evolution
.
Title
Methods for ensuring the consistency of software system models in incremental development processes and means of their integration with tool environments.
Author
Maksym I. Nikitchenko, аспірант
popup.head Nataliia O. Komleva
popup.opponent Volodymyr Fedorchuk
popup.opponent Volodymyr Palagin
popup.review Oleksandr Fomin
popup.review Vitalii Pavlenko
popup.rada
Odesa Polytechnic National University
Description
Роботу присвячено вирішенню актуальної науково-прикладної задачі, яка полягає у підвищенні ефективності та достовірності процесу модельно-орієнтованої розробки складних програмних систем шляхом розробки науково-методичного апарату та інструментальних засобів для забезпечення гарантованої консистентності UML-моделей. Актуальність теми дослідження визначається наявним протиріччям між вимогами до формальної строгості моделей UML, яка традиційно забезпечується стандартом ХМІ, та потребою у гнучкості й інтеграції з сучасними ітеративними процесами розробки, де перевагу мають легковагові формати, такі як JSON. Цей конфлікт призводить до розриву між проектною моделлю та її реалізацією, провокуючи архітектурний дрейф та накопичення прихованих архітектурних дефектів, що експоненційно збільшує вартість супроводу програмного забезпечення. Встановлене протиріччя долається шляхом розробки нового підходу, що поєднує гнучкість формату JSON для опису статичної структури та формальну строгість ХМІ для поведінкової семантики в рамках єдиної, цілісної та гарантовано узгодженої моделі з двома поданнями. Метою роботи є підвищення ефективності та достовірності процесу модельно-орієнтованої розробки складних програмних систем шляхом розробки науково-методичного апарату та інструментальних засобів для забезпечення гарантованої консистентності UML-моделей з двома поданнями (структурним у форматі JSON та поведінковим у форматі ХМІ).
Наукова новизна одержаних результатів, які виносяться на захист, полягає у наступному.
Вперше розроблено формальну метамодель UML, яка охоплює структурне та поведінкове подання, реалізовані на основі комбінованого використання форматів JSON та XMI відповідно, які логічно пов’язані між собою через формально визначене відношення відповідності; для цих подань сформульовано та узагальнено підходи до їх формалізації (для JSON) та правил представлення й валідації (для XMI). На відміну від існуючих підходів, що використовують монолітні або пропрієтарні формати, запропонована метамодель одночасно забезпечує компактне та VCS-дружнє зберігання статичної структури, адаптовану до частих і швидких змін, та підтримку стандартного XMI-представлення для динамічних аспектів, що забезпечує як сумісність із існуючими інструментами моделювання, так і ефективну інтеграцію в сучасні ітеративні процеси розробки.
Вперше запропоновано метод автоматизованого забезпечення консистентності UML-моделі, побудованої за принципом двох подань. Метод функціонує на основі формально визначеного відношення відповідності між структурними та поведінковими елементами та базується на застосуванні OCL-інваріантів для верифікації локальної та глобальної узгодженості моделей при інкрементальному редагуванні. Для подолання обмежень OCL, він також включає двоступеневий підхід з трансформацією моделі у специфікацію Alloy для глибокої верифікації за допомогою SAT-вирішувачів. На відміну від відомих методів валідації, запропонований метод дозволяє проводити глибоку формальну верифікацію складних транзитивних властивостей та автоматично генерувати контрприклади для дефектів, що підвищує точність і повноту виявлення семантичних неузгодженостей.
Вперше сформульовано та доведено теорему інкрементальної консистентності, яка гарантує, що будь-яка послідовність допустимих змін над структурним або поведінковим поданням, за умови виконання локалізованих перевірок OCL-інваріантів, зберігає глобальну узгодженість моделі в межах формального відношення відповідності. На відміну від традиційних підходів повної перевірки (зі складністю O(N)), це дозволяє теоретично обґрунтувати коректність та обчислювальну ефективність (зі складністю O(k·d)) інкрементальних методів валідації, завдяки чому можливе створення інструментів, придатних для інтеграції в CI/CD та IDE.
Отримав подальший розвиток метод двосторонньої синхронізації, що реалізований через механізм інкрементальних оновлень та локалізованої перевірки консистентності, яка ґрунтується на формальному графі залежностей із запропонованою класифікацією його ребер на структурні, семантичні та трасувальні. Особливістю розробленого методу є поєднання автоматичного виявлення конфліктів, формалізованих правил трансформації моделей і підтримки взаємної актуальності обох подань у реальному часі. На відміну від існуючих підходів, що часто є односпрямованими або покладаються на ручне втручання, запропонований метод забезпечує проактивну підтримку узгодженості в обох напрямках, що дозволяє одночасно вносити зміни як з боку коду, так і з боку моделі, запобігаючи архітектурному дрейфу.
Registration Date
2026-03-26
popup.nrat_date
2026-03-26 / 2026-07-01
