Редактирование: ВПнМ, 01 лекция (от 08 февраля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 95: | Строка 95: | ||
* ПЯ: большой размер покрытия, растёт экспоненциально с размером | * ПЯ: большой размер покрытия, растёт экспоненциально с размером | ||
* Часто невозможно построение 100% покрытия, например, в случае наличия недостижимого кода. | * Часто невозможно построение 100% покрытия, например, в случае наличия недостижимого кода. | ||
- | * Полное покрытие не гарантирует отсутствие | + | * Полное покрытие не гарантирует отсутствие ошибков. |
Пример: полное покрытие для ЧЯ: | Пример: полное покрытие для ЧЯ: | ||
Строка 243: | Строка 243: | ||
* Варди и Вольпер, 1986 -- анализ конформности в model checking, это снимает ограничение на конечность числа состояний. | * Варди и Вольпер, 1986 -- анализ конформности в model checking, это снимает ограничение на конечность числа состояний. | ||
В основном курсе будет уделять ся первому моделчекингу | В основном курсе будет уделять ся первому моделчекингу | ||
- | * Хольцман, | + | * Хольцман, 1981. Построен верификатор Spin |
=== Проблема комбинаторного взрыва === | === Проблема комбинаторного взрыва === |