Транслятор табличных представлений автоматов Мили в программы на языке SMV для автоматизации верификации проектов вычислительных устройств на основе Проверки Моделей

Данная работа посвящена разработке программных средств для использования ASM (Algorithmic state machine) диаграмм описаний конечных автоматов для верификации проектов цифровых систем в процессе их разработки. Разработана программа mealy2smv, написанная на языке C++, осуществляющая преобразование описания конечного автомата (Finite State Machine), заданного таблицей переходов, в его описание на языке SMV как структуры Крипке, что позволяет существенно снизить трудоемкость подготовки заданий на формальную верификацию.