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

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

Обоснование

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

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

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

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

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

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

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

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

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

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

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

См. также

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