Формальные методы верификации предназначены не для доказательства того, что в проектируемой системе НЕТ ошибок определенного вида.
Основные подходы к формальной проверке правильности сложных управляющих систем:
1)
2)
3)
2)
Термин дедуктивный анализ подразумивает применение аксиом и правил вывода для доказательства правильности функционирования системы. На ранних этапах исследований по дедуктивному анализу основное внимание уделялось обеспечению правильности работы ключевых систем, и такие доказательства строились исключительно вручную. Со временем исследователи осознали, что можно разработать программные средства, способные применять должным образом аксиомы и правила вывода.