Верификация (в информатике)

ВЕРИФИКАЦИЯ в информатике, процесс определения того, удовлетворяют ли результаты текущего этапа разработки объекта (например, программно-аппаратной системы) требованиям, установленным для них на предыдущем этапе; процесс проверки выполнения заданных свойств объекта. Верификацией называют и любые действия, выполняемые в ходе этого процесса.

Проверяемый в ходе верификации объект часто называют реализацией, а проверяемые свойства - спецификацией. Верификация может относиться к программному или аппаратному обеспечению, а также к программно-аппаратному комплексу в целом. Верификация бывает статической и динамической в зависимости от того, проводится ли она без функционирования проверяемой реализации (модели) или в ходе её работы.

Верификация может осуществляться путём построения формального доказательства (или опровержения) соответствия реализации спецификациям. В этом случае говорят о формальной верификации. Формальная статическая верификация возможна, когда формально определены проверяемые свойства и модель, представляющая реализацию. Например, проверяемым свойством может быть наступление какого-либо события при определённых условиях в рамках конечного автомата, описывающего реализацию. Среди методов формальной статической верификации выделяют аналитическую верификацию, с помощью которой проверяемые свойства доказываются или опровергаются на основе какого-либо логического исчисления, и метод проверки на моделях (model checking), сводящий исследование этих свойств к проверке их на конечном множестве состояний реализации.

Неформальная статическая верификация сводится к совместному анализу документов, кода программ, моделей или схем, представляющих спецификацию и реализацию. Например, одним из таких подходов является инспекция программ.

Основной и наиболее широко применяемый вид динамической верификации - тестирование. Формальное тестирование основывается на некоторых гипотезах о реализации и, исходя из них и фактических результатов функционирования реализации, доказывает или опровергает её соответствие спецификации. Различные виды формальных моделей и исчислений, используемые для формальной верификации, могут быть классифицированы следующим образом: исполняемые модели (автоматы и их различные расширения, системы переходов и их расширения, системы взаимодействующих автоматов или системы переходов, сети Петри); логические и алгебраические исчисления (логика Хоара и контрактные модели, алгебраические описания абстрактных типов данных, временные логики, реляционные алгебры); промежуточные модели (алгебры процессов, машины с абстрактными состояниями, ламбда-исчисление и его расширения).

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

Лит.: Meyer А. S. Principles of functional verification. Amst., 2003.