Генерація багатоцільових формальних моделей із успадкованого коду

• Видавець: Інститут програмних систем НАН України
• Дата: 2022
• Автори: Потієнко, С.В., Колчин, О.В.
• Формат: Стаття
• Мова: Ukrainian
• Опубліковано: Інститут програмних систем НАН України 2022
• Назва видання: Проблеми програмування
• Теми: Теоретичні і методологічні основи програмування
• Онлайн доступ: http://dspace.nbuv.gov.ua/handle/123456789/188627
• Цитувати: Генерація багатоцільових формальних моделей із успадкованого коду / С.В. Потієнко, О.В. Колчин // Проблеми програмування. — 2022. — № 3-4. — С. 42-50. — Бібліогр.: 16 назв. — укр.

У роботі запропоновано метод генерації формальних моделей із коду успадкованих систем. Призначення таких моделей полягає в можливості застосування в різних задачах, таких як автоматична генерація виконуваних тестів, трансляція в сучасні мови програмування, зворотня інженерія. Робота переслідує цілі зменшення складності пошуку в просторі станів та перевірки виконуваності формул по відношенню до прямого моделювання коду, а також допомоги в розумінні успадкованих систем та їх імплементації в сучасних технологіях. Основна увага приділена формалізації моделі пам’яті мови Cobol, адже це найбільш поширена мова в успадкованих системах. Формальна модель є атрибутною транзиційною системою з потоком керування. Запропоновано алгоритм побудови перелічуваних типів для будь-яких змінних, використання яких відповідає певним умовам, в тому числі наведена процедура трансляції числових змінних в перелічувані. Розглянута проблема трансляції неспівставних структур даних, що перетинаються в пам’яті (оператор redefines мови Cobol), копіюються чи порівнюються між собою. На відміну від поширеного підходу використання семантики об’єднань (подібного до конструкції union в С++), розроблено метод, що полягає в розбитті полів структур і не має недоліків об’єднань та сприяє мінімізації побайтного підходу. Створений метод розглянуто на прикладах структур як з простими полями так і з масивами. Наведені приклади реалізації побайтного підходу в мовах Java та C++ для тих змінних, що неможливо представити у вигляді атрибутів перелічуваних або числових типів. Робота була випробувана для генерації тестів на проєктах середнього розміру (до 100 000 рядків коду), що показало ефективність розробленого методу, а згенеровані формальні моделі також були використані для відлагодження транслятору Cobol в Java та видобутку бізнес правил.