Формальная верификация
Формальная верификация или формальное доказательство — формальное доказательство соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства.
Из-за рутинности даже простой формальной верификации и теоретической возможности их полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы.
Содержание
Обоснование
Тестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация.
Области применения
Формальная верификация может использоваться для проверки таких систем, как программное обеспечение, представленное в виде исходных текстов, криптографические протоколы, комбинаторные логические схемы, цифровые схемы с внутренней памятью.
Теоретические основы
Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ.
Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:
- формальная семантика языков программирования, например операционная семантика[en], денотационная семантика[en], аксиоматическая семантика[en] (логика Хоара), математическая семантика программ
- теории и системы типов — в первую очередь, системы с зависимыми типами (см. лямбда-куб)
- логика разделения (расширение логики Хоара)
- конечный автомат
- помеченная модель состояний и переходов
- сеть Петри
- временной автомат
- гибридный автомат
- исчисление процессов
- структурированные алгоритмы
- структурированные программы
Подходы к формальной верификации
Существуют следующие подходы к формальной верификации:
- формальная семантика языков программирования
- написание программ, которые верны по построению (см. зависимый тип, лямбда-куб, параметричность[en])
- проверка моделей (model checking)
- логический вывод (logical inference)
- символьное выполнение
- абстрактная интерпретация
- систематический анализ алгоритмов и программ
- технологии доказательного программирования
Доказательное программирование
Доказательное программирование — использовавшаяся в 1980-х годах в академических кругах технология разработки программ для ЭВМ с доказательствами правильности — доказательствами отсутствия ошибок в программах (понимая, в рамках данной теории, ошибки как несоответствия между программой и реализуемым ею алгоритмом).
Автоматическая проверка доказательства
Доказательство может быть автоматизировано полностью лишь для очень небольшого круга простых теорий, поэтому важное значение получает его автоматическая проверка и для этого преобразование к проверяемому виду.
Для поддержания строгости при проверке доказательства верификатором следует проверить ещё и верификатор, для чего нужен ещё один верификатор и так далее. Получившуюся бесконечную цепь верификаторов можно было бы свернуть, построив верифицирующий себя верификатор, обладающий способностью развернуться до применимого на практике.
См. также
- Формальная верификация криптографических протоколов
- Контрактное программирование
- Логика Хоара
- Тестирование программного обеспечения
- Обеспечение безопасности посредством языка (англ. Language-based security)
Напишите отзыв о статье "Формальная верификация"
Литература
- П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация).
<imagemap>: неверное или отсутствующее изображение |
Для улучшения этой статьи желательно?:
|
Отрывок, характеризующий Формальная верификация
Курносое и черноволосатое лицо Васьки Денисова и вся его маленькая сбитая фигурка с его жилистою (с короткими пальцами, покрытыми волосами) кистью руки, в которой он держал ефес вынутой наголо сабли, было точно такое же, как и всегда, особенно к вечеру, после выпитых двух бутылок. Он был только более обыкновенного красен и, задрав свою мохнатую голову кверху, как птицы, когда они пьют, безжалостно вдавив своими маленькими ногами шпоры в бока доброго Бедуина, он, будто падая назад, поскакал к другому флангу эскадрона и хриплым голосом закричал, чтоб осмотрели пистолеты. Он подъехал к Кирстену. Штаб ротмистр, на широкой и степенной кобыле, шагом ехал навстречу Денисову. Штаб ротмистр, с своими длинными усами, был серьезен, как и всегда, только глаза его блестели больше обыкновенного.– Да что? – сказал он Денисову, – не дойдет дело до драки. Вот увидишь, назад уйдем.
– Чог'т их знает, что делают – проворчал Денисов. – А! Г'остов! – крикнул он юнкеру, заметив его веселое лицо. – Ну, дождался.
И он улыбнулся одобрительно, видимо радуясь на юнкера.
Ростов почувствовал себя совершенно счастливым. В это время начальник показался на мосту. Денисов поскакал к нему.
– Ваше пг'евосходительство! позвольте атаковать! я их опг'окину.
– Какие тут атаки, – сказал начальник скучливым голосом, морщась, как от докучливой мухи. – И зачем вы тут стоите? Видите, фланкеры отступают. Ведите назад эскадрон.
Эскадрон перешел мост и вышел из под выстрелов, не потеряв ни одного человека. Вслед за ним перешел и второй эскадрон, бывший в цепи, и последние казаки очистили ту сторону.
Два эскадрона павлоградцев, перейдя мост, один за другим, пошли назад на гору. Полковой командир Карл Богданович Шуберт подъехал к эскадрону Денисова и ехал шагом недалеко от Ростова, не обращая на него никакого внимания, несмотря на то, что после бывшего столкновения за Телянина, они виделись теперь в первый раз. Ростов, чувствуя себя во фронте во власти человека, перед которым он теперь считал себя виноватым, не спускал глаз с атлетической спины, белокурого затылка и красной шеи полкового командира. Ростову то казалось, что Богданыч только притворяется невнимательным, и что вся цель его теперь состоит в том, чтоб испытать храбрость юнкера, и он выпрямлялся и весело оглядывался; то ему казалось, что Богданыч нарочно едет близко, чтобы показать Ростову свою храбрость. То ему думалось, что враг его теперь нарочно пошлет эскадрон в отчаянную атаку, чтобы наказать его, Ростова. То думалось, что после атаки он подойдет к нему и великодушно протянет ему, раненому, руку примирения.
Знакомая павлоградцам, с высокоподнятыми плечами, фигура Жеркова (он недавно выбыл из их полка) подъехала к полковому командиру. Жерков, после своего изгнания из главного штаба, не остался в полку, говоря, что он не дурак во фронте лямку тянуть, когда он при штабе, ничего не делая, получит наград больше, и умел пристроиться ординарцем к князю Багратиону. Он приехал к своему бывшему начальнику с приказанием от начальника ариергарда.
– Полковник, – сказал он с своею мрачною серьезностью, обращаясь ко врагу Ростова и оглядывая товарищей, – велено остановиться, мост зажечь.
– Кто велено? – угрюмо спросил полковник.
– Уж я и не знаю, полковник, кто велено , – серьезно отвечал корнет, – но только мне князь приказал: «Поезжай и скажи полковнику, чтобы гусары вернулись скорей и зажгли бы мост».
Вслед за Жерковым к гусарскому полковнику подъехал свитский офицер с тем же приказанием. Вслед за свитским офицером на казачьей лошади, которая насилу несла его галопом, подъехал толстый Несвицкий.
– Как же, полковник, – кричал он еще на езде, – я вам говорил мост зажечь, а теперь кто то переврал; там все с ума сходят, ничего не разберешь.
Полковник неторопливо остановил полк и обратился к Несвицкому:
– Вы мне говорили про горючие вещества, – сказал он, – а про то, чтобы зажигать, вы мне ничего не говорили.