Для автоматных программ существует метод создания таких
программ в целом [58]. Поэтому, во-первых, автоматные программы
можно проектировать, а, во-вторых, можно создавать программы в
той же последовательности, как и другие образцы техники: сначала
разрабатывается модель поведения, по которой формально, а часто и
автоматически, она реализуется, а параллельно с реализацией по
модели проводится верификация. При обнаружении ошибки модель
корректируется, и вновь параллельно осуществляются реализация и
верификация. В настоящее время ведутся работы по верификации
автоматных программ в целом (включая функции входных
воздействий и объектов управления) [59] и созданию формализмов
для записи требований на языках, близких к естественному [60].
Отметим, что излагаемые в книге подходы к проверке моделей
автоматных программ особенно актуальны для встраиваемых систем,
для которых характерно использование около 98% процессоров и всех
микроконтроллеров, выпускаемых в мире ежегодно. Значительную
долю из них составляют 8-разрядные устройства, программируемые
командами из одного-двух человек [61, 62].
В рамках работ по государственному контракту по теме
«Верификация автоматных программ» в СПбГУ ИТМО разработано
несколько верификаторов автоматных программ [63–67]. Созданные
верификаторы используют разные подходы, но есть общие вопросы,
которые решались при создании каждого верификатора.
Первый из них – использовать существующий верификатор программ,
или реализовывать алгоритм верификации заново? Выбор
существующего верификатора определяет темпоральную логику, с
помощью которой можно формулировать свойства автоматной
системы. При этом отметим, что наиболее известные верификаторы,
например SPIN, работают лишь с одной разновидностью
темпоральной логики. При использовании существующего
верификатора возникает необходимость в разработке автоматического
преобразователя автоматной программы во входной язык
верификатора, что, в отличие от неавтоматных программ,
осуществимо с небольшими трудозатратами.
Второй вопрос, решаемый каждым верификатором – выделение
элементарных состояний автоматной программы или, другими
словами, преобразование исходной программы в модель Крипке. Во
время работы автоматной программы автоматы переходят из одних
состояний в другие, обрабатываются события, вызываются выходные
воздействия, управление передается другим автоматам. При этом