Верификация

По стандарту PMBOK guide, включенному в систему стандартов IEEE, Верификация - это ответ на вопрос «Соответствует ли продукт спецификации?». Это проверяется формально.

Существуют следующие разновидности верификации:

• формальная верификация;

• на основе теории зависимых типов (специальные языки программирования, такие как Agda, Coq);

• статический и динамический анализ кода;

• проверка моделей.

Формальная верификация [56]предполагает наличие средств для составления спецификаций и правил вывода. Пользуясь этими правилами вывода, можно математически доказать, что программа соответствует спецификации. Однако это достаточно сложная и трудоёмкая задача, и поэтому формальная верификация мало распространена.

На формальную верификацию похож метод верификации на основе теории зависимых типов [57]. Этот метод основан на том, что в специальных языках программирования (таких как, Coqи Agda) можно одновременно и писать программы, и доказывать теоремы. Поэтому, теорема о том, что программа корректна и доказательство этой теоремы являются составными частями таких программ.

Под анализом кода автор понимает анализ, который проводится при помощи специальных инструментальных средств, например, Valgrind[58], Coverity[59], PVS Studio[60].

Анализ кода делится на статический и динамический. Динамический анализ - это анализ, выполняемый во время исполнения программы [61]. Он обладает теми же недостатками, что и тестирование: не проверяются все возможные пути исполнения программы. Кроме того, динамический анализ замедляет исследуемую программу (так как выполняется в ходе её выполнения) и, как следствие, непригоден либо ограниченно пригоден для проверки высоконагруженных систем.

Статический анализ - это анализ кода без его выполнения [62]. Он не обладает указанным выше недостатком, но методами статического анализа можно найти только некоторые классы ошибок.

Метод проверки моделей [1 -5]состоит в том, что для проверяемой программы или алгоритма строится модель (обычно это модель Крипке), спецификация к программе записывается на языке темпоральной логики, а затем специальные алгоритмы автоматически проверяют, соответствует ли модель спецификации. Если модель не соответствует спецификации, то автоматически строится контрпример.

Метод проверки моделей тесно связан со статическим анализом кода. Некоторые инструменты, например, Java Pathfinder[63], совместно используют методы проверки моделей и статического анализа кода.

Главным недостатком метода проверки моделей является то, что модель требуется построить вручную. При этом невозможно гарантировать, что если модель удовлетворяет спецификации, то и исходная программа соответствует этой спецификации.

И хотя предпринимаются попытки автоматизировать методы проверки моделей для программ общего вида (например, Java Pathfinder), но все они сводятся к тому, что ищутся ошибки из заранее заданных классов, либо проводится ограниченная проверка моделей [52] (как, например, в инструментальном средстве CBMC[64]).

Среди парадигм программирования всё чаще начинает использоваться автоматное программирование. Его наиболее целесообразно применять для ответственных систем. Именно для автоматных программ удаётся повысить уровень автоматизации процесса верификации за счёт формальных переходов от программы к модели и от модели к программе при наличии ошибки. В настоящей работе созданы инструментальные средства для верификации автоматных программ.

В ходе выполнения работы по государственному контракту [65 -69]был выполнен обзор существующих инструментальных средств для проведения верификации [69], который показал, что для автоматных программ рассматриваемого в диссертации типа (сложные условия на переходах автоматов, выходные воздействия и т. д.) - структурных автоматов [42]эффективные решения отсутствуют. Настоящая работа призвана восполнить указанный пробел.

1.5.