Search academic texts

Information × Registration Number 0826U000667, PhD dissertation Status Доктор філософії Date 13-04-2026 popup.evolution o 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 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 Close