Математические методы верификации схем и программ
Лекции по верификации от Савенкова
Адекватная подсветка синтаксиса для Vim
Модель описывается на языке Promela (PROcess MEta LAnguage). Для верификации Spin генерирует программу на C.
Получить все контрпримеры (error trails) не получится, только один.
Отрицание свойства называется never claim.
Верифицировать:
spin -run main.pml
Если модель не соответствует спецификации, то контрпример будет записан в файл
с расширением .trail. Чтобы выполнить на нем симуляцию с выводом
диаграммы последовательности:
spin -t -M main.pml
Функции для генерации случайных значений нет. Ее наличие бы значительно усложнило верификацию, так как проверяются все варианты работы системы.