Лучшие вопросы
Таймлайн
Чат
Перспективы

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

Из Википедии, свободной энциклопедии

Remove ads

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

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

Remove ads

Обоснование

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

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

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

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

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

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

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

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

Remove ads

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

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

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

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

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

Remove ads

Примеры интерактивного доказательства

Код аутентификации HMAC от OpenSSL из 134 строк на языке C был верифицирован с использованием 2832 строк на Coq.

Еще одним примером является файловая система FSCQ. Код и его верификация выполнялись на Coq, занимая 31 тысяч строк доказательства и кода в сумме. Для сравнения, непроверенная файловая система написана на C и занимает всего 3 тысяч строк. Несмотря на то что первоначальные работы, включая создание логического каркаса для Coq, требовали нескольких человеко-лет, эксперименты выявили поэтапное снижение стоимости при внесении изменений в код и доказательство.[1]

Remove ads

См. также

Литература

  • А. М. Миронов. Методы верификации программ.
  • А. С. Камкин. Введение в формальные методы верификации программ: учебное пособие.
  • Lathouwers, Sophie; Zaytsev, Vadim (2022). Modelling Program Verification Tools for Software Engineers. Proceedings of the 25th International Conference on Model Driven Engineering Languages and Systems. MODELS '22. Montreal, Quebec, Canada: Association for Computing Machinery. pp. 98–108. doi:10.1145/3550355.3552426. ISBN 9781450394666.

Примечания

Ссылки

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.

Remove ads