Исследовательская группа

Лаборатория киберфизических систем

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

October 15

15 октября 2021 г. (пятница), 10:00 МСК (14:00 НСК)

Максим Нейзов (Проектный институт АвтоПромТермоОбработка, Курган)

Доклад посвящен подходу к дедуктивной верификации управляющих программ, который заключается в построении автоматной модели программы и задании на её основе системы аксиом. При построении аксиоматики одной из ключевых задач является задача формализации структурных свойств автоматной модели. В качестве решения в докладе будет представлена модификация автоматной модели, которая получила название "сдвиговый автомат".  Свойства модели демонстрируются и обсуждаются на примерах.