Летичевський О.О. Верифікація та тестування інтерактивних систем, специфікованих за допомогою базових протоколів. - Рукопис. Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 - математичне та програмне забезпечення обчислювальних машин і систем. - Інститут кібернетики ім.В.М.Глушкова НАН України. - Київ, 2005. Дисертація присвячена побудові методів роботи з вимогами, що складають технологію, яка є складовою частиною процесу створення програмних систем з великою кількістю станів. Розглянуто п'ять складових частин цієї технології: формалізація вимог у вигляді базових протоколів; пошук суперечливостей та неповноти; генерація тестових наборів з множини вимог; синтез та аналіз динамічних властивостей моделі. В розробці методів використовуються методи алгебраїчного та інерційного програмування, а також формалізм алгебри процесів, зокрема властивості атрибутних транзиційних систем. Вимоги до інтерактивних систем представляються у вигляді формальних специфікацій - базових протоколів. Визначено клас базових протоколів, для якого задачі технології вирішуються без експонентного вибуху. За допомогою розробленого у роботі формалізму будуються алгоритми верифікації базових протоколів з використанням машини доведення, а також синтез моделі за базовими протоколами. На основі створених методів символьного моделювання розглядаються різні критерії генерації тестів та їх застосування до генерації тестів за специфікаціями, записаними сучасними інженерними мовами, - MSC, SDL, UML. Ключові слова: атрибута транзиційні системи, агенти та середовища, алгебра процесів, вимоги до програмного забезпечення, базові протоколи, верифікація, символьне моделювання, суперечливість та неповнота специфікацій, автоматичне доведення теорем, генерація тестів.