Формальная верификация

В контексте программных и аппаратных систем формальная верификация — доказательство с помощью формальных методов корректности или некорректности (правильности или неправильности) алгоритмов, программ и систем в соответствии с формальным описанием их свойств.

Обоснование

Тестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация.

Области применения

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

Теоретические основы

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

Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:

• формальная семантика языков программирования, например операционная семантика, денотационная семантика, аксиоматическая семантика (логика Хоара), [математическая семантика программ].
• конечный автомат
• помеченная модель состояний и переходов
• сеть Петри
• временной автомат
• гибридный автомат
• алгебра процессов
• структурированные алгоритмы
• структурированные программы

Подходы к формальной верификации

Существуют следующие подходы к формальной верификации:

• формальная семантика языков программирования
• проверка моделей (model checking)
• логический вывод (logical inference)
• cимвольное выполнение (symbolic execution)
• абстрактная интерпретация (abstract interpretation)
• систематический анализ алгоритмов и программ
• технологии доказательного программирования

См. также

• Тестирование программного обеспечения
• Контрактное программирование
• Логика Хоара