Научные методы исследования

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

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

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

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

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

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

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

  • Современные технологии
  • Обработка данных
  • Разработка программного обеспечения