абстракции проверяемых моделей. В настоящее время технологии
проверки моделей позволяют верифицировать программы примерно
из 10 000 строк кода [89].
Наиболее впечатляющим примером, демонстрирующим способности
символьной проверки моделей, является верификация протокола
когерентности кэш-памяти стандарта шины IEEE Futurebus+
(стандарт IEЕЕ 896.1–1991). Хотя разработка этого протокола была
начата в 1988 г., все прежние попытки обосновать его правильность
основывались исключительно на неформальных рассуждениях. Летом
1992 г. исследовательская группа из университета Карнеги-Меллона
[92] построила точную модель протокола на языке SMV и затем,
применяя систему верификации SMV, показала, что полученная
система переходов удовлетворяет формальной спецификации. Им
удалось также обнаружить ряд ранее не замеченных ошибок и
локализовать потенциально ошибочные участки в проекте протокола.
Особое значение верификация имеет для программных систем со
сложным поведением. Для этого класса систем технологию создания и
верификации следует выбирать уже на этапе проектирования.
Удачным выбором для таких задач является технология автоматного
программирования [2, 51]. В первую очередь, автоматное
программирование дает возможность успешно выполнить
декомпозицию управляющей логики и вычислений на этапе создания
программной системы. Оно позволяет использовать наглядную
графическую нотацию для описания сложного поведения, сделав тем
самым систему менее подверженной ошибкам. С другой стороны, при
применении model checking к автоматным программам построение
модели программы по ее спецификации значительно упрощается по
сравнению с традиционными подходами к программированию. При
использовании автоматного подхода модель программы, пригодная к
верификации, строится уже на этапе проектирования. Наконец,
автоматное программирование, как уже отмечалось, позволяет
декомпозировать процесс верификации программы на верификацию
ее поведенческой (управляющей) модели, которая выполняется
методом model checking, и независимую верификацию атомарных
вычислительных воздействий. Если система успешно спроектирована
на основе автоматного подхода, и входные и выходные воздействия
представляют собой небольшие относительно простые участки кода,
то их можно проверить и формальной верификацией, оперирующей
зависимостями выходных данных алгоритма от его входных данных.
Выходные воздействия в автоматных программах могут также быть
проверены на основе подхода, изложенного в работе [59].