Краткое сравнение формальных методов (модельная проверка, доказательство корректности) и тестирования по классам ошибок, стоимости и применимости.
1) Что каждое средство действительно обнаруживает
- Тестирование:
- Находит фактические ошибки при выполнении: баги в логике реализации, регрессы, неправильная обработка реальных входных данных, ошибки интеграции, проблемы с производительностью и утечки ресурсов.
- Хорошо ловит ошибки, зависящие от окружения и неконтролируемых внешних факторов (файловая система, сеть, библиотеки).
- Ограничение: покрывает только те сценарии, которые были исполнены (нет гарантии отсутствия скрытых ошибок).
- Модельная проверка:
- Находит контрпримеры к формальным свойствам (безопасность, ливелоки, дедлоки, инварианты, временные свойства) в пределах заданной модели/размера.
- Даёт исчерпывающее покрытие модели: если модель полностью соответствует системе и размер конечен, ошибки в модели будут найдены.
- Ограничение: чувствительна к абстракции модели; ошибки моделирования (несоответствие спецификации реализации) не будут пойманы.
- Доказательство корректности (теоремные доказательства, SMT/инварианты):
- Может дать математическое доказательство отсутствия конкретного класса ошибок (например, арифметических нарушений, нарушение инвариантов, корректность алгоритма) для всех входов.
- Подходит для критических свойств и алгоритмов; даёт наивысшую степень уверенности при корректности спецификации и формализации.
- Ограничение: трудоёмко, требует спецификации и человеческих усилий; ошибки в спецификации сводят на нет пользу доказательства.
2) Типичные классы ошибок по методике
- Тестирование: функциональные отклонения, API-ошибки, парсинг, граничные значения, race, concur-ошибки иногда воспроизводятся, проблемы интеграции, деградация производительности.
- Модельная проверка: дедлоки, потеря свойств безопасности, нарушения инвариантов, неверные переходы состояний, нарушения временных требований (LTL/CTL).
- Доказательство корректности: логические ошибки алгоритма, неверные предположения о данных, арифметические переполнения, целостность инвариантов, корректность алгебраических свойств.
3) Стоимость (временные и человеческие ресурсы, инструментальная сложность)
- Тестирование: низкая/средняя стоимость на старте; автоматизация (юнит/интеграция, CI) снижает стоимость в долгом периоде. Требуются тестовые среды, наборы данных и время на написание тестов.
- Модельная проверка: средняя/высокая стоимость. Автоматизированные чекеры дают быстрые результаты для небольших моделей; масштабирование ограничено из-за «взрыва состояний». Зачастую требуется моделирование упрощённой версии компонента.
- Доказательство корректности: высокая/очень высокая стоимость (эксперты, время на формализацию и подсказки для автоматов доказательства). Подходит для ключевых компонентов, не для всего кода.
4) Масштабируемость и применимость в ограниченных ресурсах
- Тестирование: легко масштабируется, применимо на всех этапах. В проектах с ограниченным временем — основной инструмент.
- Модельная проверка: применима для критичных небольших модулей (протоколов, синхронизации) либо после абстрагирования/композиции. В больших системах — применять локально (на узких местах).
- Доказательство: применять селективно — к ядру критической логики (криптография, расчёты безопасности, алгоритмы маршрутизации). Для остального — слишком дорого.
5) Практические рекомендации для проектов с ограниченным временем/ресурсами
- Делайте приоритет: тестирование + автоматическая статическая проверка + выборочная формальная верификация критичных модулей.
- Используйте лёгкие формальные техники: статический анализ, bounded model checking, property-based testing (QuickCheck), fuzzing — они дают соотношение эффект/затраты лучше полного доказательства.
- Модельную проверку применять для протоколов, распределённых алгоритмов, управления состояниями; ограничивать модель по состояниям/параметрам.
- Доказательства применять только при высокой критичности; комбинировать с ревью спецификаций (ошибки в спецификации — главный риск формализации).
- Интеграция в CI: автоматические тесты + фазы fuzzing / BMC на каждый PR; тяжелые доказательства ведутся отдельно для релизов/критических компонентов.
6) Краткая сводка
- Тестирование: дешёво, практично, находит реальные проявления багов, но не даёт доказательств их отсутствия.
- Модельная проверка: даёт исчерпывающие результаты для модели/границ, хороша для ошибок, связанных с состоянием/параллелизмом; ограничена масштабом и качеством модели.
- Доказательство корректности: наиболее сильная гарантия при высокой стоимости и требовании корректной спецификации.
Полезная формула для оценки взрыва состояний (очень упрощённо): если система имеет $n$ независимых переменных, каждая с $b$ значениями, число состояний примерно $$S\approx b^n.$$ Это иллюстрирует, почему модельная проверка быстро становится неуправляемой.