Летичевський О. О. Верифікація та тестування інтерактивних систем, специфікованих за допомогою базових протоколів

Дисертація присвячена побудові методів роботи з вимогами, що складають технологію, яка є складовою частиною процесу створення програмних систем з великою кількістю станів. Розглянуто п’ять складових частин цієї технології: формалізація вимог у вигляді базових протоколів; пошук суперечливостей та неповноти; генерація тестових наборів з множини вимог; синтез та аналіз динамічних властивостей моделі. В розробці методів використовуються методи алгебраїчного та інерційного програмування. Визначено клас базових протоколів, для якого задачі технології вирішуються без експонентного вибуху. За допомогою розробленого у роботі формалізму будуються алгоритми верифікації базових протоколів з використанням машини доведення, а також синтез моделі за базовими протоколами. На основі створених методів символьного моделювання розглядаються різні критерії генерації тестів та їх застосування до генерації тестів за специфікаціями, записаними сучасними інженерними мовами, – MSC, SDL, UML.