Панченко Т. В. Композиційні методи специфікації та верифікації програмних систем

У дисертаційній роботі досліджено проблеми специфікації та верифікації прагматично важливих класів програмних систем методами композиційного програмування. Розроблено композиційні моделі та мови для специфікації програмних систем зі структурованими даними, виконано комплексний аналіз та розподіл структур даних і функцій над ними по рівнях абстракції. Доведено репрезентативну повноту номінативних даних комплексно-номінативного рівня. Розроблено композиційні методи для верифікації систем спеціального класу - моделі багатоекземплярного виконання програм у серверному середовищі з паралелізмом в режимі почергового виконання з переключенням із взаємодією через спільну пам'ять. Сформульовано два варіанти часткової коректності програм на введених композиційних мовах та запропоновано методологію верифікації, що включає метод з лінійною складністю замість експоненційної. Ключові слова: композиційне програмування, композиційно-номінативні системи, специфікація програмних систем, верифікація програм, моделі програм, модель виконання, доведення властивостей, часткова коректність, паралельне програмування, інваріант, транзиційні системи.