Верификация

[hedgeov]

Вот есть неплохой язык описания систем — Promela. Используется как входной для The SPIN model checker. И есть опять же неплохой верификатор, использующий символьную верификацию, SMV (ну или NuSMV). Минус жтого верификатора — заточка под железо. Поведение системы описывается набором конечных автоматов.

А вот почему, интересно, никто не скрестил "ужа с ежом" — Promela с NuSMV? Пока нигде статей на эту нему не вижу :(