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

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