Анотація до роботи:

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

Дисертація на здобуття наукового ступеня кандидата фізико-математичних наук за спеціальністю 01.05.03 – математичне та програмне забезпечення обчислювальних машин і систем. – Інститут кібернетики ім.В.М.Глушкова НАН України. – Київ, 2005.

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

У дисертаційній роботі отримані наступні результати:

1. Сформульовано технологію роботи з вимогами до інтерактивних систем. Вимоги формалізуються у вигляді базових протоколів, що можуть бути записані у формі діаграм однією з інженерних мов – MSC, SDL, UML. Сформульовано чотири основні задачі роботи з вимогами – верифікація, генерація тестів, синтез моделі, аналіз властивостей. Представлено схему використання результатів даних задач у загальному процесі створення програмного забезпечення. Використання даної технології забезпечить скорочення циклу розробки програмного забезпечення і підвищення якості програмного забезпечення за рахунок виявлення помилок на стадії збору вимог, автоматичної генерації тестового набору, автоматичним синтезом неповної архітектурної моделі продукту, перевірки динамічних властивостей моделі.

2. Виділено клас K-протоколів як клас, що покриває основну множину телекомунікаційних задач, і в якому задачі верифікації, аналізу та тестування вирішуються зі значним зниженням рівня експоненційного вибуху. Це відбувається за рахунок виключення паралелізму у функціонуванні всіх агентів. Задачі розглядаються стосовно одного ключового агента, що є тестований.

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

4. Побудовано алгоритм символьного моделювання поводжень агента, що породжує множину трас, використовуваних надалі як тестовий набір для тестування ключового агента. В алгоритмі використовується доказова машина, що дозволяє абстрагуватися від можливих переборів значень атрибутів агента і середовища.

5. Сформульовано різні критерії покриття вимог тестовими наборами. Зокрема, одним із критеріїв є використання факторизації множини станів агента, що дозволяє значно скоротити набір тестів, необхідний для тестування ключового агента. Це досягається за допомогою конструювання трас із представників класів, у яких окремо будується повний набір трас методом зворотного символьного моделювання. Даний критерій гарантує повне покриття вимог і поводжень усередині кожного класу.

6. Побудовано алгоритм синтезу неповної архітектурної моделі, пред-ставленої у вигляді SDL-системи, з множини К-протоколів. Використання даного алгоритму може скоротити фазу розробки, а також запобігти частині помилок на етапі кодування.

7. Розроблено програму перевірки динамічних властивостей SDL-моделі, що формулюються за допомогою анотацій. Програма розроблена методом інсерційного програмування і дозволяє перевірити правильність властивостей моделі за допомогою моделювання і звертання до доказової машини.

8. Створено прототипи програм роботи з вимогами:

– програма підготовки вимог у вигляді формальних специфікацій за допомогою редактора MSC-діаграм;

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

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

– програма перевірки динамічних властивостей SDL-моделей.

9. Створені автором прототипи є основою системи верифікації вимог, розробленої і впровадженої для роботи з вимогами у промислових телекомунікаційних моделях у кампанії Motorola, а також у кампанії "Інформаційні програмні системи". Результати використання системи викладені в таблиці.