Статья

В статье рассматривается сущность метода верификации программ на моделях. Приводится описание процесса верификации программ на моделях, согласно которому составлена упрощенная схема процесса. Выделяются основные этапы рассматриваемого метода верификации, приводится их характеристика. Особое внимание уделяется практической реализации метода. Представлены инструменты для описания моделей и верифицируемых свойств на языке Promela. С помощью верификатора SPIN произведена проверка модели протокола голосования, описанная на языке Promela, результаты которой позволили сделать выводы о правильности составленной модели. В ходе анализа контрпримера измененной модели найдены допущенные ошибки. Составлена таблица преимуществ и недостатков метода верификации программ на моделях. Приведена сравнительная характеристика ранее рассмотренных методов тестирования и метода верификации программ на моделях.