Применение ослабленных отношений симуляции в методе сетевых инвариантов для верификации параметризованных асинхронных моделей

Рассматривается задача верификации параметризованных моделей асинхронных распределённых систем (Parameterized Model Checking). Для решения задачи используется метод сетевых инвариантов. В разновидностях метода сетевых инвариантов используются отношения симуляции, бисимуляции и трассового включения на моделях. В случае асинхронных систем симуляция и бисимуляция оказываются слишком строгими для поиска инварианта и требуют применения методов абстракции.
Описываются три ослабленных отношения симуляции: квазиблочная, блочная и полублочная. Квазиблочная симуляция обладает всеми необходимыми свойствами для применения метода инвариантов. Блочная симуляция является частным случаем квазиблочной симуляции и используется при поиске инвариантов. Наличие полублочной симуляции между моделями является необходимым и достаточным условием существования блочной симуляции. Приводится схема алгоритма вычисления полублочной симуляции и описываются используемые в реализации подходы к оптимизации. Отношения применяются для проверки параметризованной модели протокола RSVP методом сетевых инвариантов.