Формальная верификация: различия между версиями
[непроверенная версия] | [непроверенная версия] |
Tim2 (обсуждение | вклад) |
Xqbot (обсуждение | вклад) м робот изменил: uk:Формальна верифікація; косметические изменения |
||
Строка 37: | Строка 37: | ||
* [[технологии доказательного программирования]] |
* [[технологии доказательного программирования]] |
||
==См. также== |
== См. также == |
||
* [[Доказательное программирование]] |
* [[Доказательное программирование]] |
||
Строка 44: | Строка 44: | ||
* [[Тестирование программного обеспечения]] |
* [[Тестирование программного обеспечения]] |
||
==Литература== |
== Литература == |
||
* П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация). |
* П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация). |
||
Строка 68: | Строка 68: | ||
[[sk:Verifikácia]] |
[[sk:Verifikácia]] |
||
[[sr:Верификација]] |
[[sr:Верификација]] |
||
[[uk:Формальна верифікація]] |
|||
[[uk:Верифікація формальна]] |
|||
[[zh:形式验证]] |
[[zh:形式验证]] |
Версия от 13:13, 21 ноября 2010
В контексте программных и аппаратных систем формальная верификация — доказательство с помощью формальных методов корректности или некорректности (правильности или неправильности) алгоритмов, программ и систем в соответствии с формальным описанием их свойств.
Обоснование
Тестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация.
Области применения
Формальная верификация может использоваться для проверки таких систем, как программное обеспечение, представленное в виде исходных текстов, криптографические протоколы, комбинаторные логические схемы, цифровые схемы с внутренней памятью.
Теоретические основы
Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ.
Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:
- формальная семантика языков программирования, например операционная семантика, денотационная семантика, аксиоматическая семантика (логика Хоара), [математическая семантика программ].
- конечный автомат
- помеченная модель состояний и переходов
- сеть Петри
- временной автомат
- гибридный автомат
- алгебра процессов
- структурированные алгоритмы
- структурированные программы
Подходы к формальной верификации
Существуют следующие подходы к формальной верификации:
- формальная семантика языков программирования
- проверка моделей (model checking)
- логический вывод (logical inference)
- cимвольное выполнение (symbolic execution)
- абстрактная интерпретация (abstract interpretation)
- систематический анализ алгоритмов и программ
- технологии доказательного программирования
См. также
- Доказательное программирование
- Контрактное программирование
- Логика Хоара
- Тестирование программного обеспечения
Литература
- П.Грогоно, Программирование на языке Pascal, М.:Мир, 1982, с.295, (Тестирование и верификация).
Для улучшения этой статьи желательно:
|