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

Потієнко С.В. Алгебраїчні методи верифікації асинхронних паралельних систем. –
Рукопис.

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

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

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

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

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

1) запропоновано формалізм базових протоколів для роботи з вимогами та надано можливості використання мов специфікацій MSC, SDL, UML як засобів створення і верифікації формальних моделей та вимог:

2) сформульовано визначення таких властивостей системи базових протоколів як несуперечливість, повнота та властивості цілісності. Розроблено алгоритми статичної перевірки
цих властивостей. Доведено коректність побудованих алгоритмів, зокрема, доведено їх
достатність для перевірки того, що проаналізована система володіє сформульованими
властивостями;

3) запропоновано підходи до розв’язання проблеми досяжності заданих станів системи. Побудовано метод статичної фільтрації станів на базі алгоритмів статичної перевірки та доведено його достатність для заперечення досяжності. Для невідфільтрованих станів побудовано метод абстракцій, що дозволяє використовувати методи спрямованого пошуку в перевірці на моделі;

4) розроблено алгоритми прямого та зворотного предикатних перетворювачів як функцій перетворення однієї множини станів в іншу під дією заданого базового протоколу. Множини станів задаються формулами базової мови, яка є мовою багатосортного числення предикатів першого порядку з наступними типами змінних і констант: прості типи – числові (цілий та дійсний), символьні (булевський, злічений та довільний символьний), а також масиви елементів простих типів з цілими та зліченими індексами, функціональні типи (функції від аргументів простих типів, які повертають значення простого типу), списки елементів простих
типів;

5) розроблено алгоритми трансляції певних підмножин інженерних мов специфікацій MSC, SDL та UML в мову базових протоколів з метою подальшої автоматичної верифікації. Підмножини цих мов було виділено виходячи з практичної необхідності в застосованих індустріальних проектах. Також було запропоновано розширення обраних мов для застосування методів верифікації у повній мірі: передумови, постумови та анотації у вигляді формул базової мови;

6) розроблено наступні алгоритми аналізу формальних вимог:

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

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

– алгоритм трансляції обраних підмножин мов MSC, SDL та UML Statecharts із запропонованими розширеннями в мову базових протоклів.

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