д.т.н., профессор, заведующий кафедрой технологии программирования СПбГУ ИТМО

Большинство ответственных технических систем являются событийными, а используемое в них управление является автоматным. Для таких систем может осуществляться ко-дизайн – поведение как аппаратной. так и программной части может быть описано с помощью автоматов. Автоматы могут быть либо построены эвристически, либо выращены с помощью эволюционных алгоритмов. Программы, реализующие поведение рассматриваемого класса систем, называются автоматными. Такие программы могут быть эффективно верифицированы на основе метода Model Checking.