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

Формальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства.

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

ОбоснованиеПравить

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

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

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

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

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

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

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

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

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

• формальная семантика языков программирования
• написание программ, которые верны по построению (см. зависимый тип, лямбда-куб, параметричность^[en])
• проверка моделей (model checking)
• логический вывод (logical inference)
• символьное выполнение  (англ.) (рус.
• абстрактная интерпретация  (англ.) (рус.
• систематический анализ алгоритмов и программ
• технологии доказательного программирования

Доказательное программированиеПравить

Доказательное программирование — использовавшаяся в 1980-х годах в академических кругах технология разработки программ для ЭВМ с доказательствами правильности — доказательствами отсутствия ошибок в программах (понимая, в рамках данной теории, ошибки как несоответствия между задуманным алгоритмом и фактическим алгоритмом, реализуемым программой).

Автоматическая проверка доказательстваПравить

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

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

См. такжеПравить

• Формальная верификация криптографических протоколов
• Контрактное программирование
• Логика Хоара
• Тестирование программного обеспечения
• Обеспечение безопасности посредством языка (англ. Language-based security)

ЛитератураПравить

• А. М. Миронов. Верификация программ. Часть 1: нерекурсивные программы.

• А. М. Миронов. Верификация программ методом model checking.

• А.С. Камкин Введение в формальные методы верификации программ: учебное пособие