Лекция №14Верификация и валидация
Верификация и валидация — два связанных процесса разработки ПО. Верификация отвечает на вопрос «Правильно ли разрабатывается продукт?» (Are we building the product right?); валидация — на вопрос «Правильный ли продукт разрабатывается?» (Are we building the right product?). Верификация проверяет ПО на соответствие спецификациям, заданным при проектировании; валидация проверяет, соответствует ли продукт ожиданиям заказчика и потребителей. Исходя из определения, тестирование — частный случай валидации.
Для простых программ тестирования вполне достаточно для того, чтобы определить, правильно ли работает ПО или нет. Однако тестирование (практически) всегда производится на ограниченном множестве наборов входных данных, то есть с помощью тестирования можно выявить и устранить существующие ошибки, но нельзя доказать, что ошибок в системе нет. Для систем с высокими требованиями к отказоустойчивости и/или надежности необходимы именно такие доказательства. Ошибка в ПО, сохранившаяся из-за ограничений тестирования, привела к аварии ракеты Ariane и обошлась в 350 млн. долларов.
Для дополнения процесса тестирования разработаны статические методы, которые анализируют код программы, не выполняя ее. Существуют неформальные статические методы (например, инспекции кода и проверщики типа lint) и формальные методы, основанные на строгих математических моделях.
Формальные методы могут использоваться для автоматизированного доказательства корректности и других свойств программ; ключевая часть такого подхода — логика Хоара. Другой вид формальных методов — проверка моделей (model checking), позволяющая перебрать все различные способы выполнения программы, например, с помощью теории конечных автоматов, и выявить ошибки, ускользнувшие при тестировании.