Формальная верификация

Материал из Seo Wiki - Поисковая Оптимизация и Программирование

Перейти к: навигация, поиск

В контексте программных и аппаратных систем формальная верификация — доказательство с помощью формальных методов корректности или некорректности (правильности или неправильности) алгоритмов, программ и систем в соответствии с формальным описанием их свойств.

Содержание

Обоснование

Тестирование программного обеспечения не может доказать, что система, алгоритм или программа не содержит никаких ошибок и дефектов и удовлетворяет определённому свойству. Это может сделать формальная верификация.

Области применения

Формальная верификация может использоваться для проверки таких систем, как программное обеспечение, представленное в виде исходных текстов, криптографические протоколы, комбинаторные логические схемы, цифровые схемы с внутренней памятью.

Теоретические основы

Верификация представляет собой формальное доказательство на абстрактной математической модели системы, в предположении о том, что соответствие между математической моделью и природой системы считается изначально заданным. Например, по построению модели либо математического анализа и доказательства правильности алгоритмов и программ.

Примерами математических объектов, часто используемых для моделирования и формальной верификации программ и систем являются:

Подходы к формальной верификации

Существуют следующие подходы к формальной верификации:

См. также


cs:Formální verifikace

da:Verifikation (bekræftelse) de:Verifizierung 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:形式验证

Личные инструменты

Served in 0.128 secs.