Дисертація доктора філософії. Нікітченко Максим Ігорович. Методи забезпечення консистентності моделей програмних систем в інкрементальних процесах розробки та засоби їх інтеграції з інструментальними середовищами.

Реєстраційний номер

0826U000667, Дисертація доктора філософії

На здобуття

Доктор філософії

Дата захисту

13-04-2026

Статус

Захищена

Назва роботи

Методи забезпечення консистентності моделей програмних систем в інкрементальних процесах розробки та засоби їх інтеграції з інструментальними середовищами.

Здобувач

Нікітченко Максим Ігорович, аспірант

Керівник Комлева Наталія Олегівна
Опонент Федорчук Володимир Анатолійович
Опонент Палагін Володимир Васильович
Рецензент Фомін Олександр Олексійович
Рецензент Павленко Віталій Данилович

Установа, організація, у вченій раді якої відбудеться/відбувся захист

Національний університет "Одеська політехніка"

Опис

Роботу присвячено вирішенню актуальної науково-прикладної задачі, яка полягає у підвищенні ефективності та достовірності процесу модельно-орієнтованої розробки складних програмних систем шляхом розробки науково-методичного апарату та інструментальних засобів для забезпечення гарантованої консистентності 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. Отримав подальший розвиток метод двосторонньої синхронізації, що реалізований через механізм інкрементальних оновлень та локалізованої перевірки консистентності, яка ґрунтується на формальному графі залежностей із запропонованою класифікацією його ребер на структурні, семантичні та трасувальні. Особливістю розробленого методу є поєднання автоматичного виявлення конфліктів, формалізованих правил трансформації моделей і підтримки взаємної актуальності обох подань у реальному часі. На відміну від існуючих підходів, що часто є односпрямованими або покладаються на ручне втручання, запропонований метод забезпечує проактивну підтримку узгодженості в обох напрямках, що дозволяє одночасно вносити зміни як з боку коду, так і з боку моделі, запобігаючи архітектурному дрейфу.

Дата реєстрації

2026-03-26

Додано/оновлено в НРАТ

2026-03-26 / 2026-07-01