Редактирование: ВПнМ, 02 лекция (от 15 февраля)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 4: | Строка 4: | ||
Можно либо изначально построить модель, либо в процессе разработки. | Можно либо изначально построить модель, либо в процессе разработки. | ||
- | На первом этапе выделяем из требований классы свойств, и по описанию системы и классам св-в строим модель. после этого описываем конкретные свойства, которые проверяем в процессе верификации. Подаём модель и св-ва на вход верификатора и | + | На первом этапе выделяем из требований классы свойств, и по описанию системы и классам св-в строим модель. после этого описываем конкретные свойства, которые проверяем в процессе верификации. Подаём модель и св-ва на вход верификатора и о проверяет. Дальше может быть несколько вариантов: |
* Свойство выполняется. Если модель корректна, то программа корректна. | * Свойство выполняется. Если модель корректна, то программа корректна. | ||
* Верификация не останавливается тогда, когда мы этого хотим. Это означает, что слишком сложная модель. Надо останавливать процесс вериф. и модернизировать модель | * Верификация не останавливается тогда, когда мы этого хотим. Это означает, что слишком сложная модель. Надо останавливать процесс вериф. и модернизировать модель |