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

Дисертація присвячена створенню алгоритмів та методів для підвищення ефективності верифікації формальних моделей. Розроблено метод оперативної побудови точних абстракцій станів формальної моделі для перевірки темпоральних властивостей. Головною відмінністю є те, що кожний абстрактний стан формується із підмножини атрибутів та їх реальних значень відповідного конкретного стану, якої достатньо для перевірки властивостей моделі. Абстрактні стани не відрізняють варіювання значень незначущих атрибутів, що дає можливість значно зменшити кількість станів, необхідних для перевірки властивостей моделі. Отримано подальший розвиток методів спрямованого пошуку поведінки моделі. Вперше як засоби спрямування використовуються спеціальні регулярні вирази над алфавітом імен переходів моделі, тим самим задання цілей тестування удосконалено. Метод дає можливість автоматизувати побудову тестових сценаріїв та аналіз поведінок формальних моделей.