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