Кратко и по делу — где что применимо и какие у каждого метода главные ограничения.
Hoare‑логика (дедуктивная верификация)
- Суть: спецификация в виде троек $\{P\}C\{Q\}$; доказательство корректности через вычисление слабейших предусловий $wp(C,Q)$ или генерацию проверочных условий (VC).
- Практическое применение: модульная проверка алгоритмической корректности, проверка безопасности указателей и инвариантов циклов; инструменты/практики — SPARK (Ada), Frama‑C/WP, Dafny, VCC, VeriFast.
- Сильные стороны: точная функциональная спецификация, модульность, хорошо работает для сложных алгебраических свойств.
- Ограничения: требуются инварианты/аннотации (ручная работа), автоматизация ограничена — сложные арифметические и индуктивные свойства часто требуют интерактивных доказательств; масштабирование к большим системам затруднено без абстракций; поведение среды/реал‑временные аспекты нужно моделировать отдельно.
SMT‑решатели
- Суть: автоматическое решение логических формул богато поддерживающих теориями (биты, целые/реальные числа, массивы, строки). Используются для развязки VC, BMC, софт‑верификации.
- Практическое применение: автоматическая проверка VC от Hoare‑проверяющих, статический анализ, bounded model checking, тест‑генерация, проверка свойств в коде (Z3, CVC5).
- Сильные стороны: высокая автоматизация, хороши для больших наборов арифметики/битовых операций/массивов; быстро дают контрпримеры.
- Ограничения: не всегда решают нелинейную арифметику и сложные индуктивные структуры; решения иногда эвристичны (приближённые), могут выдавать "unknown"; доверие к решениям зависит от детектируемости багов и репутации солвера; полностью автоматическое доказывание сложных свойств обычно невозможно.
Модельная проверка
- Суть: исчерпывающий перебор состояний модели (явный/символический/SMT‑базированный) для свойств временной логики (LTL/CTL) или конечных свойств.
- Практическое применение: проверка протоколов, аппаратных схем, встроенных систем, свойств конкуренции и дедлоков; инструменты — SPIN, NuSMV, UPPAAL (таймед‑автоматы), PRISM (стохастические модели).
- Сильные стороны: даёт контрпример (trace), мощна для логики поведения (безопасность/жизнь), автоматична для конечных моделей.
- Ограничения: state‑space explosion — сложна для больших/неограниченных структур; требуется абстракция модели (потеря точности); проверка свойств реального кода требует адекватной трансляции в модель; ограничения в выражении непрерывного времени/детерминистичности/случайности требуют специализированных инструментов.
Интерактивные теоремы‑помощники (Coq, Isabelle/HOL)
- Суть: выражение спецификаций и доказательств в мощных логиках (интуиционистская типизированная логика в Coq, HOL в Isabelle); поддержка тактик, автоматизации, extraction в код.
- Практическое применение: проекты высочайшей надёжности — CompCert (верифицированный компилятор), seL4 (верифицированное ядро), формальные библиотеки криптографии; создание машинно проверяемых доказательств требований и проверка транзитивной цепочки (спецификация → реализация → компилятор).
- Сильные стороны: очень высокий уровень доверия (мелкое ядро проверки), можно выразить почти любые свойства, возможность извлечения корректного исполняемого кода, формализация методологий и доказательств.
- Ограничения: большой объём ручной работы и высокая квалификация; длительные сроки разработки; поддержание и изменение доказательств дорогостояще; частичная автоматизация (sledgehammer, SMT‑интеграция), но полная автоматизация невозможна для сложных систем.
Сравнение, сочетания и практические рекомендации
- Автоматизация vs доверие: SMT/модельная проверка — более автоматичны, но менее всеобъемлющи; Coq/Isabelle — максимально надёжны, но трудоёмки.
- Масштабирование: для больших систем применяют многоуровневую стратегию — моделирование и model checking для архитектурных свойств, SMT/Hoare‑проверка для модулей и автоматической разрядки VC, интерактивные доказательства для критичных ядер (валидированные компиляторы, ядро ОС, криптопримитивы).
- Спецификация и среда: формальные методы работают только так хорошо, как хороша спецификация и модель окружения; важно моделировать предположения об окружении и проверять их.
- Временные/реал‑тайм требования: UPPAAL/Timed Automata для детальных временных свойств; доказательные системы требуют дополнительной формализации тайминга и реализации.
- Соответствие стандартам: для авиации (DO‑178C/DO‑333), автопромышленности (ISO 26262) — формальные методы могут использоваться как облегчение валидации/верификации при соблюдении процессов.
Ключевые ограничения, о которых нельзя забывать
- требуемые аннотации и инварианты;
- state‑space explosion и необходимость абстракций;
- трудности с нелинейной арифметикой, неограниченными структурами, динамической памятью и сложной средой;
- высокая цена в человеко‑часах и квалификации для полноформальных доказательств;
- доверие к инструментам (необходимы небольшие проверяемые ядра или независимая проверка доказательств).
Короткое практическое правило выбора
- проверяемые свойства поведения/сочетания состояний на уровне модели → модельная проверка;
- автоматическая проверка имплементации и VC → SMT + Hoare‑аннотации (Frama‑C, SPARK, Dafny);
- критичные ядра/структурно сложные спецификации и полностью формальная гарантия → Coq/Isabelle и проверяемые инструментальные цепочки (CompCert, извлечение кода);
- комбинируйте: model checking для быстрых контрпримеров, SMT для автоматического дисчарджа VC, интерактивные доказчики для оставшихся трудных свойств и доверенных компонентов.
Если нужно, могу кратко привести типовые инструменты для каждой категории или пример типового процесса верификации критической подсистемы.