Верификация программного продукта

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

ПОНЯТИЕ ВЕРИФИКАЦИИ.
Жизненный цикл разработки ПО
Верификация - это процесс определения, выполняют ли программные средства и их компоненты требования, наложенные на них в последовательных этапах жизненного цикла разрабатываемой программной системы.
Жизненный цикл программного обеспечения - совокупность итерационных процедур, связанных с последовательным изменением состояния программного обеспечения от формирования исходных требований к нему до окончания его эксплуатации конечным пользователем.

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

Задачи верификации в рамках жизненного цикла ПО
Выявление наиболее критичных и наиболее подверженных ошибкам частей создаваемой или сопровождаемой системы
Контроль и оценка качества ПО во всех его аспектах
Предоставление всем заинтересованным лицам (руководителям, заказчикам, пользователям и пр.) информации о текущем состоянии проекта и характеристиках его результатов
Предоставление руководству проекта и разработчикам информации для планирования дальнейших работ, а также для принятия решений о продолжении проекта, его прекращении или передаче результатов заказчику

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

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

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