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

  Скачати повний текст