Формальная верификация программного обеспечения¶

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

¶Основные подходы

¶Дедуктивная верификация

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

¶Проверка моделей (model checking)

Состояние системы представляется конечным автоматом, а свойство — формулой темпоральной логики (LTL, CTL). Алгоритм систематически обходит пространство состояний и либо подтверждает свойство, либо предъявляет контрпример — траекторию, нарушающую требование. Метод автоматизирован, но страдает от проблемы комбинаторного взрыва состояний; для борьбы с ним применяют символьное представление (BDD, SAT/SMT-решатели) и абстракцию.

¶Абстрактная интерпретация

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

¶Инструменты

¶Применение

Формальная верификация востребована там, где цена отказа высока: авионика, космические системы, железнодорожная автоматика, ядра операционных систем, криптографические протоколы, компиляторы и микропроцессоры. Известные примеры — верифицированное ядро seL4, компилятор CompCert, статический анализатор Astrée, применённый к программному обеспечению Airbus A340.

¶Ограничения

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