RUS  ENG
Полная версия
ЖУРНАЛЫ // Системы и средства информатики // Архив

Системы и средства информ., 2010, том 20, выпуск 3, страницы 4–16 (Mi ssi221)

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

С. Л. Френкель, А. Л. Курц, Д. Л. Либуркин, H. A. Фандюшина, Б. Н. Андерс


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

Ключевые слова: формальная верификация, конечные автома-ты.

УДК: 004.054



© МИАН, 2024