Подробное описание документа
Горохова А. С.
Разработка методов верификации элементов дискретно-событийной модели / Горохова А. С., Завадская Л. А., Новичкова М. А. // Политехнический молодежный журнал МГТУ им. Н. Э. Баумана. - 2024. - № 4. -
Рассмотрено моделирование процессов в дискретно-событийной системе (ДСС) для управления группой мобильных роботов, методы верификации модели объекта управления и спецификации ДСС. Поскольку при построении модели могут возникать ошибки, дальнейшее моделирование на некорректно построенной модели может приводить к дополнительному объему работы, излишней трате вычислительных ресурсов и иметь недопустимый результат. Предложена возможность повысить качество системы за счет применения валидации элементов ДСС с использованием программных инструментов анализа сети Петри и корректности спецификации. Представлена двухэтапная проверка ДСС: на уровне построения модели объекта управления в целом и на уровне конкретной спецификации поведения системы. На первом этапе моделируемую систему представляют в виде сети Петри и с помощью построения и анализа дерева достижимости, ограниченного до конечного размера, проверяют сеть на соответствие свойствам безопасности, живости, достижимости и связности. На втором этапе модель поведения системы проверяют на корректность переходов между событиями и контролируют связность цепочки событий. Предложена практическая реализация системы верификации, выполненная на языке программирования С++. Результаты могут служить основой для разработки системы, позволяющей автоматизировать процесс проектирования систем группового управления роботами.
