Формальная верификация: различия между версиями
| [непроверенная версия] | [отпатрулированная версия] |
Tveditor (обсуждение | вклад) Нет описания правки |
|||
| Строка 1: | Строка 1: | ||
| ⚫ | |||
{{орисс}} |
|||
| ⚫ | |||
== Обоснование == |
== Обоснование == |
||
[[Тестирование программного обеспечения]] не может доказать, что система, алгоритм или программа не содержит никаких |
[[Тестирование программного обеспечения]] не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать ''формальная'' верификация. |
||
Только процесс ''формальной'' верификации может доказать, что система, алгоритм или программа не содержит определенных дефектов или удовлетворяет определенным свойствам. |
|||
Все, что можно сделать - это доказать, что система не имеет никаких дефектов из тех, что можно определить, а также обладает всеми строго определяемыми свойствами, которые вместе делают ее функциональной и полезной. |
|||
== Области применения == |
== Области применения == |
||
Формальная верификация может использоваться для проверки таких систем, как [[криптографические протоколы]], [[комбинаторные логические схемы]], [[цифровые схемы]] с внутренней памятью |
Формальная верификация может использоваться для проверки таких систем, как программное обеспечение, представленное в виде исходных текстов, [[криптографические протоколы]], [[комбинаторные логические схемы]], [[цифровые схемы]] с внутренней памятью. |
||
== Теоретические основы == |
== Теоретические основы == |
||
Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие |
Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ. |
||
между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ. |
|||
Примерами математических объектов, часто используемых для моделирования и формальной верификации систем являются: |
Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются: |
||
| ⚫ | |||
* [[конечный автомат]] |
* [[конечный автомат]] |
||
* помеченная [[модель состояний и переходов]] |
* помеченная [[модель состояний и переходов]] |
||
| Строка 27: | Строка 24: | ||
* [[структурированные алгоритмы]] |
* [[структурированные алгоритмы]] |
||
* [[структурированные программы]] |
* [[структурированные программы]] |
||
| ⚫ | |||
== Подходы к формальной верификации == |
== Подходы к формальной верификации == |
||
| Строка 33: | Строка 29: | ||
Существуют следующие подходы к формальной верификации: |
Существуют следующие подходы к формальной верификации: |
||
* формальная семантика языков программирования |
|||
* [[проверка моделей]] (model checking) |
* [[проверка моделей]] (model checking) |
||
* [[логический вывод]] (logical inference) |
* [[логический вывод]] (logical inference) |
||
| Строка 41: | Строка 38: | ||
==См. также== |
==См. также== |
||
* [[Тестирование программного обеспечения]] |
* [[Тестирование программного обеспечения]] |
||
* [[Контрактное программирование]] |
* [[Контрактное программирование]] |
||
| Строка 48: | Строка 46: | ||
[[Категория:Математическая логика]] |
[[Категория:Математическая логика]] |
||
[[Категория:Информатика]] |
|||
[[cs:Formální verifikace]] |
[[cs:Formální verifikace]] |
||
Версия от 14:34, 21 марта 2009
В контексте программных и аппаратных систем формальная верификация — доказательство с помощью формальных методов корректности или некорректности (правильности или неправильности) алгоритмов, программ и систем в соответствии с формальным описанием их свойств.
Обоснование
Тестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация.
Области применения
Формальная верификация может использоваться для проверки таких систем, как программное обеспечение, представленное в виде исходных текстов, криптографические протоколы, комбинаторные логические схемы, цифровые схемы с внутренней памятью.
Теоретические основы
Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ.
Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:
- формальная семантика языков программирования, например операционная семантика, денотационная семантика, аксиоматическая семантика (логика Хоара), [математическая семантика программ].
- конечный автомат
- помеченная модель состояний и переходов
- сеть Петри
- временной автомат
- гибридный автомат
- алгебра процессов
- структурированные алгоритмы
- структурированные программы
Подходы к формальной верификации
Существуют следующие подходы к формальной верификации:
- формальная семантика языков программирования
- проверка моделей (model checking)
- логический вывод (logical inference)
- cимвольное выполнение (symbolic execution)
- абстрактная интерпретация (abstract interpretation)
- систематический анализ алгоритмов и программ
- технологии доказательного программирования
См. также
 | Для улучшения этой статьи желательно:
|