• A
  • A
  • A
  • АБB
  • АБB
  • АБB
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта

Статья

Адаптивная редукция симметричных моделей в задаче верификации моделей программ для логики линейного времени

Захаров В. А., Коннов И. В.
Наиболее значительную трудность для всех инструментальных средств верификации моделей программ создает эффект комбинаторного взрыва. Один из способов сократить размер проверяемой модели $M$ --- выбрать подходящую группу автоморфизмов $G$ размеченной системы переходов $M$ и построить фактор-модель $M/G$. Состояниями фактор-модели $M/G$ служат орбиты состояний модели $M$ относительно группы $G$; также известно, что модели $M/G$ и $M$ находятся в отношении бисимуляции. К сожалению, поиск нетривиальной группы автоморфизмов $G$ произвольной конечной системы переходов $M$ является вычислительно трудной задачей. Для преодоления этой трудности был предложен метод адаптивного упрощения модели на основе симметрии. Этот метод позволяет воспользоваться преимуществами симметричного устройства модели $M$, не обращаясь явно к орбитам ее состояний. В самом начале решения задачи проверки достижимости состояний предполагается, что модель является абсолютно симметричной; далее это предположение корректируется по мере того, как обнаруживаются переходы, несовместные со сложившимся представлением о симметрии в модели. Пространство состояний модели оказывается разбитым на классы эквивалентности, которые называются мета-состояниями; на каждом шаге вычисления при рассмотрении очередного перехода мета-состояния могут подвергаться расщеплению. Мы обнаружили, что метод адаптивного упрощения модели на основе симметрии может быть с равным успехом применен для проверки выполнимости формул LTL. Основной результат работы --- новый теоретико-автоматный подход к верификации моделей программ, сочетающий метод адаптивного упрощения модели на основе симметрии и алгоритм двойного поиска в глубину для проверки пустоты автоматов Бюхи.