Автоматная программа состоит из конечного автомата и набора объектов управления, с которыми взаимодействует модель. Наиболее распространенным способом проверки автоматных программ является Model Checking, так как для автоматных программ высока степень автоматизации. Однако проверка моделей позволяет верифицировать только автомат, но не всю систему в целом. В работе описан подход к тестированию автоматных программ. В предлагаемом подходе тестирование используется для проверки соответствия спецификации системы ее реализации. Для формализации требований спецификации к модели и объектам управления предлагается использовать контракты. Тест описывается как последовательность переходов в модели. В работе показаны преимущества использования расширенных конечных автоматов и контрактов для построения модели и разработан метод нахождения входных параметров для выполнения заданного сценария в автоматной модели при помощи использования генетических алгоритмов. Это и многое другое вы найдете в книге Применение генетических алгоритмов к генерации тестов (Андрей Законов)