ВПнМ/Теормин
Материал из eSyr's wiki.
(→Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.) |
(→Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.) |
||
Строка 209: | Строка 209: | ||
** Каждому переходу из системы должен соответствовать переход в модели: <math>s^1_1 \rightarrow_1 s^1_2 => a(s^1_1) \rightarrow_2 a(s^1_2)</math> | ** Каждому переходу из системы должен соответствовать переход в модели: <math>s^1_1 \rightarrow_1 s^1_2 => a(s^1_1) \rightarrow_2 a(s^1_2)</math> | ||
* Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap AP^1</math> | * Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap AP^1</math> | ||
+ | |||
+ | '''Достаточное условие адекватности модели свойствам правильность ''' : | ||
+ | |||
+ | Алфавит предикатов свойств правильности включен в алфавит предикатов модели. | ||
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. === | === Абстракция. Абстракция графов программ. Отношение слабой симуляции. === |
Версия 12:43, 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
Система детерменирована:
- по действиям тогда и только тогда, когда
- по атомарным высказываниям
- ( количество одинаково размеченных потомков не больше одного )
Недетерменизм - это фича! Полезен для:
- моделирования параллельного выполнения в режиме чередования (интерливинга)
- позволяет не указывать скорость выполнения процессов
- моделирования прототипа системы
- не ограничивает реализацию заданным порядком выполнения операторов
- построения абстракции реальной системы
- модель может быть построена по неполной информации
Вычисления
- Конечный фрагмент вычисления σ системы переходов TS называется конечная последовательность чередующихся состояний и действий
- Бесконечный (максимальный) фрагмент вычисления ρ -
- Начальный фрагмент вычисления - фрагмент вычисления, для которого
- Вычисление - начальный максимальный фрагмент вычисления
Достижимое состояние (из начального) в системе переходов TS - такое состояние , для которого существует конечный фрагмент вычисления
Rich(TS) - множество всех достижимых состояний в TS
Трасса
Свойства линейного времени
- Свойство определяет набор допустимых трасс:
- Система переходов TS удовлетворяет свойству линейного времени
Моделирование программ. Графы программ. Статическая и операционная семантика.
Граф программы – формальное описание текста программы.
- Dp -- единый абстрактный домен данных.
- P -- программа.
- Vp -- множество переменных программы(Var).
-
- -- каждая переменная принадлежит какому-либо домену
- n -- подстановка.
- Cond(Vp) -- Набор булевых условий над Vp
- формулы пропозициональной логики
- условия на переменные
- Эффект операторов:
Граф программы:
- Loc -- множество точек
- -- множество начальных точек
- Act -- множество действий
- -- отношение перехода
- Effect -- функция эффекта
- -- начальное условие
Системы переходов графов программ TS(PG) -- система переходов графа программы задается сигнатурой
Пример: Лекция 4, слайд 16
Параллелизм. Чередование систем переходов.
Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.
Параллелизм. Синхронный параллелизм. Рандеву.
- распределённые программы выполняются параллельно
- в распределённой программе нет разделяемых переменных
Передача сообщений в распределённых программах:
- cинхронная передача сообщений (рандеву)
- асинхронная передача сообщений (кналы)
Синхронный обмен сообщенийями:
- Процессы вместе выполняют синхронизированные действия
- Взаимодействие процессов - одновременно
Рандеву
Тогда , где
- определяется как:
- интерливинг для и
- рандеву для
Пример рандеву: Лекция 4, слайд 32
Синхронный параллелизм
Тогда , где
- определяется как:
Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.
Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.
Представим трассу в форме интерпретации I:
- N - множество натуральных чисел
- - отношение порядка на N
Рассмотрим трассы tr и tr' такие, что
Будем говорить, что трасса tr' является абстракцией трассы tr, если
- такое, что
Пример абстракции трассы: Лекция 2, слайд 53
Необходимое условие корректности модели - , где
- P - система
- M - модель этой системы
При этом, если - некоторое свойство системы, то выполняется тогда и только тогда, когда верно условие корректности модели.
Достаточное условие корректности модели :
- такая, что
- s0' = α(s0)
Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.
Абстракция системы переходов -- картинка на 4 слайде 3-й лекции.
Достаточное условие корректности LTS модели.
Пусть у нас имеются две системы переходов, TS1 и TS2 -- для системы и модели соответственно:
Достаточное условие корректности:
- Алфавит предикатов модели включен в алафвит предикатов системы:
- Задано отображение . На отображение накладываются следующие условия:
- Оно преобразует начальное состояние системы в начальное состояние модели:
- Каждому переходу из системы должен соответствовать переход в модели:
- Метки на состояниях модели должны состоять только из предикатов модели:
Достаточное условие адекватности модели свойствам правильность :
Алфавит предикатов свойств правильности включен в алфавит предикатов модели.