Формальная верификация: различия между версиями
[отпатрулированная версия] | [отпатрулированная версия] |
YurikBot (обсуждение | вклад) |
EmausBot (обсуждение | вклад) м Перемещение 17 интервики-ссылок в Викиданные (d:Q173326) |
||
Строка 62: | Строка 62: | ||
[[Категория:Информатика]] |
[[Категория:Информатика]] |
||
[[Категория:Формальные методы]] |
[[Категория:Формальные методы]] |
||
[[cs:Formální verifikace]] |
|||
[[da:Verifikation (bekræftelse)]] |
|||
[[de:Verifizierung]] |
|||
[[el:Τυπική επαλήθευση]] |
|||
[[en:Formal verification]] |
|||
[[es:Verificación formal]] |
|||
[[fr:Vérification formelle]] |
|||
[[he:אימות תוכנה]] |
|||
[[ja:形式的検証]] |
|||
[[lt:Verifikacija]] |
|||
[[no:Verifikasjon]] |
|||
[[pl:Weryfikacja formalna]] |
|||
[[pt:Verificação formal]] |
|||
[[sk:Verifikácia]] |
|||
[[sr:Верификација]] |
|||
[[uk:Формальна верифікація]] |
|||
[[zh:形式验证]] |
Версия от 02:30, 13 марта 2013
Формальная верификация — формальное доказательство соответствия или несоответствия формального предмета верификации его формальному описанию. Предметом выступают алгоритмы, программы и другие доказательства.
Из-за рутинности даже простой формальной верификации и теоретической возможности их полной автоматизации под формальной верификацией обычно подразумевают автоматическую верификацию с помощью программы.
Обоснование
Тестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация.
Области применения
Формальная верификация может использоваться для проверки таких систем, как программное обеспечение, представленное в виде исходных текстов, криптографические протоколы, комбинаторные логические схемы, цифровые схемы с внутренней памятью.
Теоретические основы
Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ.
Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:
- формальная семантика языков программирования, например операционная семантика, денотационная семантика, аксиоматическая семантика (логика Хоара), [математическая семантика программ].
- конечный автомат
- помеченная модель состояний и переходов
- сеть Петри
- временной автомат
- гибридный автомат
- исчисление процессов
- структурированные алгоритмы
- структурированные программы
Подходы к формальной верификации
Существуют следующие подходы к формальной верификации:
- формальная семантика языков программирования
- проверка моделей (model checking)
- логический вывод (logical inference)
- символьное выполнение (symbolic execution)
- абстрактная интерпретация (abstract interpretation)
- систематический анализ алгоритмов и программ
- технологии доказательного программирования
Доказательное программирование
Доказательное программирование — использовавшаяся в 1980-х годах в академических кругах технология разработки программ для ЭВМ с доказательствами правильности — доказательствами отсутствия ошибок в программах (понимая, в рамках данной теории, ошибки как несоответствия между программой и реализуемым ею алгоритмом).
Автоматическая проверка доказательства
Доказательство может быть автоматизировано полностью лишь для очень небольшого круга простых теорий, поэтому важное значение получает его автоматическая проверка и для этого преобразование к проверяемому виду.
Для поддержания строгости при проверке доказательства верификатором следует проверить ещё и верификатор, для чего нужен ещё один верификатор и так далее. Получившуюся бесконечную цепь верификаторов можно было бы свернуть, построив верифицирующий себя верификатор, обладающий способностью развернуться до применимого на практике.
См. также
Литература
- П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация).
Для улучшения этой статьи желательно:
|