Проверка моделей
Формальная верификация · model checking
создано · обновлено
Метод, при котором программа автоматически обходит состояния описанной системы и проверяет, что в каждом из них правила соблюдены. Если правило нарушается, метод выдаёт точную цепочку шагов, которой это достигается. Например, модель магазина находит ход «оплата, сбой связи», после которого деньги списаны, а заказа нет: покупатель заплатил и ничего не получил. В отличие от теста, метод не ограничен сценариями, которые придумал человек, но ограничен размером выбранного мира.
Источник: Википедия: проверка моделей
Подробнее: Как найти гонки и потерянные данные моделями на Quint
Где встречается · 4
- Vitest или Jest · Спеки и контекст
- Как найти состояние гонки (race condition) в коде · Спеки и контекст
- Чем model checking отличается от тестов · Спеки и контекст
- Какой язык формальной верификации выбрать · Спеки и контекст