ВПнМ/Теормин
Материал из eSyr's wiki.
(Различия между версиями)
м (/* Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени.) |
м (/* Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени.) |
||
Строка 63: | Строка 63: | ||
* '''по атомарным высказываниям''' | * '''по атомарным высказываниям''' | ||
** <math>|I| \leqslant 1</math> | ** <math>|I| \leqslant 1</math> | ||
- | ** <math>\forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 1</math> | + | ** <math>\forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 1</math> ( количество одинаково размеченных потомков не больше одного ) |
=== Моделирование программ. Графы программ. Статическая и операционная семантика. === | === Моделирование программ. Графы программ. Статическая и операционная семантика. === |
Версия 10:31, 20 мая 2009
Лекция 1
Валидация - исследование и обоснование того, что спецификация ПО и само ПО через реализованную в нём функциональность удовлетворяет ребованиям пользователей.
Верификация - исследование и обоснование того, что программа соответствует своей спецификации.
Верификация в общем случае алгоритмически неразрешима.
Методы верификации:
- "Полное" тестирование (слайды 14-22)
- Имитационное моделирование
- Доказательство теорем (27-29)
- Статический анализ (30-33)
- Верификация на моделях (34-38)
Моделирование и абстракция
Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.
Схема верификации на моделях (Лекция 2, слайд 3)
Состояние программы - совокупность значений переменных и управления, связанных с некоторой моделью программы.
Модель - упрощённое описание реальности, выполненное с определенной целью.
- с каждым объектом может быть связано несколько моделей
- каждая модель отражает свой аспект реальности
Аспекты модели:
- простота - модель должна быть проще, чем реальность
- корректность - не расходиться с реальностью
- адекватность - соответствовать решаемой задаче
Построение модели
- формализация требований (постановка задачи моделирования)
- выбор языка моделирования
- абстракция системы до модели с учётом требований
Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.
Размеченная система переходов (LTS)
- S - множество состояний
- Act - множество действий
- τ - невидимое действие
- - тотальное отношение переходов
- - начальное состояние
- AP - множество атомарных высказываний
- - функция разметки
S, Act - конечные или счётные множества
Пример LTS: Лекция 2, слайд 40-41
Прямые потомки
- - такие состояния s', которые непосредственно вытекают из s через переход a
- - все возможные состояния s', которые непосредственно вытекают из s
Система детерменирована:
- по действиям тогда и только тогда, когда
- по атомарным высказываниям
- ( количество одинаково размеченных потомков не больше одного )