ISSN 1818-1015 · EISSN 2313-5417
Язык: ru

МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ

ВЕРИФИКАЦИЯ ДЕКЛАРАТИВНОЙ LTL-СПЕЦИФИКАЦИИ ПОВЕДЕНИЯ УПРАВЛЯЮЩИХ ПРОГРАММ (2024)

Статья продолжает цикл трудов по разработке и верификации управляющих программ на основе LTL-спецификаций специального вида. Ранее была предложена декларативная LTL-спецификация, позволяющая описывать поведение управляющих программ и выполнять построение по ней программного кода на императивном языке ST для программируемых логических контроллеров. Данная LTL-спецификация может быть непосредственно верифицирована на предмет соответствия заданным темпоральным свойствам методом проверки модели (model checking) с помощью инструмента символьной верификации nuXmv. При этом не требуется переводить LTL-формулы спецификации в другой формализм - SMV-спецификацию (код на входном языке инструмента nuXmv). Цель настоящей работы состоит в исследовании альтернативных способов представления модели поведения программы, соответствующей декларативной LTL-спецификации, при её верификации в рамках инструментального средства nuXmv. В статье выполняются преобразования декларативной LTL-спецификации в различные SMV-спецификации с сопутствующими изменениями постановки задачи верификации, что приводит к значительному снижению временных затрат при проверке темпоральных свойств с использованием инструмента nuXmv. Ускорение верификации обусловлено сокращением пространства состояний проверяемой модели. Полученные в результате предложенных преобразований SMV-спецификации задают одинаковые или бисимуляционно эквивалентные системы переходов, обеспечивая неизменность результатов верификации при замене одной SMV-спецификации на другую.

Тип: Статья
Автор (ы): Нейзов Максим Вячеславович, Кузьмин Егор Владимирович
Ключевые фразы: УПРАВЛЯЮЩЕЕ ПРОГРАММНОЕ ОБЕСПЕЧЕНИЕ, ПЛК-ПРОГРАММА, ДЕКЛАРАТИВНАЯ LTL-СПЕЦИФИКАЦИЯ, ИМПЕРАТИВНАЯ LTL-СПЕЦИФИКАЦИЯ, ПОЛНАЯ СИСТЕМА ПЕРЕХОДОВ, ПСЕВДОПОЛНАЯ СИСТЕМА ПЕРЕХОДОВ, ПРОСТРАНСТВО СОСТОЯНИЙ, ПРОВЕРКА МОДЕЛИ, ВЕРИФИКАТОР NUXMV, SMV-СПЕЦИФИКАЦИЯ, БИСИМУЛЯЦИОННАЯ ЭКВИВАЛЕНТНОСТЬ, БИСИМУЛЯЦИЯ

Идентификаторы и классификаторы

УДК
004.424. Методы программирования
519.683.8. Специальные приемы программирования
eLIBRARY ID
67856514
Текстовый фрагмент статьи