Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 93 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 475: | Строка 475: | ||
* если какое-то утверждение неизбежно, то обратное — невозможно | * если какое-то утверждение неизбежно, то обратное — невозможно | ||
* при помощи логики от одного можно переходить к другому при помощи отрицания | * при помощи логики от одного можно переходить к другому при помощи отрицания | ||
+ | |||
+ | ''Схема верификации на модели: Лекция 2, слайд 3'' | ||
+ | |||
+ | <u>Примеры классов свойств:</u> | ||
+ | * Стандартные | ||
+ | ** [http://en.wikipedia.org/wiki/Deadlock deadlocks] ([http://ru.wikipedia.org/wiki/%D0%92%D0%B7%D0%B0%D0%B8%D0%BC%D0%BD%D0%B0%D1%8F_%D0%B1%D0%BB%D0%BE%D0%BA%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0 взаимная блокировка]) | ||
+ | ** [http://en.wikipedia.org/wiki/Race_condition Race condition] ([http://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%81%D1%82%D0%BE%D1%8F%D0%BD%D0%B8%D0%B5_%D0%B3%D0%BE%D0%BD%D0%BA%D0%B8 состояние гонки]) | ||
+ | * Специфичные для конкретного приложения | ||
+ | ** требования справедливости | ||
+ | ** корректная завершаемость | ||
+ | ** причинно-следственный и темпоральный порядок состояний системы | ||
<u>Способы описания свойств правильности:</u> | <u>Способы описания свойств правильности:</u> |