Формальная верификацияФормальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства. Из-за рутинности даже простой формальной верификации и теоретической возможности их полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы. ОбоснованиеТестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация. Области примененияФормальная верификация может использоваться для проверки таких систем, как программное обеспечение, представленное в виде исходных текстов, криптографические протоколы, комбинаторные логические схемы, цифровые схемы с внутренней памятью. Теоретические основыВерификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ. Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:
Подходы к формальной верификацииСуществуют следующие подходы к формальной верификации:
Доказательное программированиеДоказательное программирование — использовавшаяся в 1980-х годах в академических кругах технология разработки программ для ЭВМ с доказательствами правильности — доказательствами отсутствия ошибок в программах (понимая, в рамках данной теории, ошибки как несоответствия между задуманным алгоритмом и фактическим алгоритмом, реализуемым программой). Автоматическая проверка доказательстваДоказательство может быть автоматизировано полностью лишь для очень небольшого круга простых теорий, поэтому важное значение получает его автоматическая проверка и для этого преобразование к проверяемому виду. [источник не указан 1580 дней] Значительное количество практически важных задач, в том числе, например, задача остановки, является алгоритмически неразрешимыми. Для поддержания строгости при проверке доказательства верификатором следует проверить ещё и верификатор, для чего нужен ещё один верификатор и так далее. Получившуюся бесконечную цепь верификаторов можно было бы свернуть, построив верифицирующий себя верификатор, обладающий способностью развернуться до применимого на практике. [источник не указан 1580 дней] Примеры интерактивного доказательстваКод аутентификации HMAC от OpenSSL из 134 строк на языке C был верифицирован с использованием 2832 строк на Coq. Еще одним примером является файловая система FSCQ. Код и его верификация выполнялись на Coq, занимая 31 тысяч строк доказательства и кода в сумме. Для сравнения, непроверенная файловая система написана на C и занимает всего 3 тысяч строк. Несмотря на то что первоначальные работы, включая создание логического каркаса для Coq, требовали нескольких человеко-лет, эксперименты выявили поэтапное снижение стоимости при внесении изменений в код и доказательство.[1] См. также
Литература
Примечания
Ссылки
|
Portal di Ensiklopedia Dunia
