ВПнМ/Теормин

Материал из eSyr's wiki.

(Различия между версиями)
Перейти к: навигация, поиск
(→Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.)
(→Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.)
Строка 100: Строка 100:
Представим трассу в форме интерпретации I: <math>I(tr) = <N, \leqslant, \xi></math>
Представим трассу в форме интерпретации I: <math>I(tr) = <N, \leqslant, \xi></math>
-
* N - множество натуральных чисел
+
* <math>N</math> - множество натуральных чисел
-
* <math>\leqslant</math> - отношение порядка на N
+
* <math>\leqslant</math> - отношение порядка на <math>N</math>
* <math>\xi: N \times AP \rightarrow \{true, false\}, ~~ \forall n>0, p \in AP ~~ \Rightarrow ~~ \xi(n, p) = true \Leftrightarrow p \in L(s)</math>
* <math>\xi: N \times AP \rightarrow \{true, false\}, ~~ \forall n>0, p \in AP ~~ \Rightarrow ~~ \xi(n, p) = true \Leftrightarrow p \in L(s)</math>
Строка 108: Строка 108:
* <math>I(tr) = <N, \leqslant, \xi'>, ~~ \xi: N \times AP' = \{true, false\}</math>
* <math>I(tr) = <N, \leqslant, \xi'>, ~~ \xi: N \times AP' = \{true, false\}</math>
-
Будем говорить, что tr' является '''абстракцией''' tr, если
+
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr, если
# <math>AP' \subseteq AP</math>
# <math>AP' \subseteq AP</math>
# <math>\exists \alpha : N \rightarrow N</math> такое, что <math>\forall n,k \in N, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k) </math>
# <math>\exists \alpha : N \rightarrow N</math> такое, что <math>\forall n,k \in N, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k) </math>
# <math>\forall n \in N, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(n, p)</math>
# <math>\forall n \in N, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(n, p)</math>
 +
 +
Пример абстракции трассы: Лекция 2, слайд 53
 +
 +
''' Условие корректности модели ''' - <math>\forall tr \in Traces(TS(P)) \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr'</math>, где
 +
* <math>P</math> - система
 +
* <math>M</math> - модель этой системы
 +
 +
При этом, если <math>\varphi</math> - некоторое свойство системы, то <math>M \models \varphi ~ \Rightarrow ~ P \models \varphi</math> выполняется тогда и только тогда, когда верно условие корректности модели.
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. ===
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. ===
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. ===
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. ===

Версия 11:28, 20 мая 2009

Содержание

Лекция 1

Валидация - исследование и обоснование того, что спецификация ПО и само ПО через реализованную в нём функциональность удовлетворяет ребованиям пользователей.

Верификация - исследование и обоснование того, что программа соответствует своей спецификации.

Верификация в общем случае алгоритмически неразрешима.

Методы верификации:

  • "Полное" тестирование (слайды 14-22)
  • Имитационное моделирование
  • Доказательство теорем (27-29)
  • Статический анализ (30-33)
  • Верификация на моделях (34-38)

Моделирование и абстракция

Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.

Схема верификации на моделях (Лекция 2, слайд 3)

Состояние программы - совокупность значений переменных и управления, связанных с некоторой моделью программы.

Модель - упрощённое описание реальности, выполненное с определенной целью.

  • с каждым объектом может быть связано несколько моделей
  • каждая модель отражает свой аспект реальности

Аспекты модели:

  • простота - модель должна быть проще, чем реальность
  • корректность - не расходиться с реальностью
  • адекватность - соответствовать решаемой задаче

Построение модели

  1. формализация требований (постановка задачи моделирования)
  2. выбор языка моделирования
  3. абстракция системы до модели с учётом требований

Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.

Размеченная система переходов (LTS)

TS = <S, Act, \overset{a}{\rightarrow} ,s_0, AP, L>

  • S - множество состояний
  • Act - множество действий
  • τ - невидимое действие
  • \overset{a}{\rightarrow} \subseteq S \times Act \times S - тотальное отношение переходов
  • s_0 \in S - начальное состояние
  • AP - множество атомарных высказываний
  • L:S \rightarrow 2^{AP} - функция разметки

S, Act - конечные или счётные множества

<s, a, s'> \in \overset{a}{\rightarrow} \equiv s \overset{a}{\rightarrow} s'

Пример LTS: Лекция 2, слайд 40-41

Прямые потомки

  • Post(s, a) = \{s' \in S, s \overset{a}{\rightarrow} s'\} - такие состояния s', которые непосредственно вытекают из s через переход a
  • Post(s) = \bigcup_{a \in Act} Post(s, a) - все возможные состояния s', которые непосредственно вытекают из s

Система TS = <S, Act, \overset{a}{\rightarrow} ,s_0, AP, L> детерменирована:

  • по действиям тогда и только тогда, когда
    • |I| \leqslant 1
    • \forall s \in S, \forall a \in Act \Rightarrow |Post(s, a)| \leqslant 1
  • по атомарным высказываниям
    • |I| \leqslant 1
    • \forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 1 ( количество одинаково размеченных потомков не больше одного )


Недетерменизм - это фича! Полезен для:

  • моделирования параллельного выполнения в режиме чередования (интерливинга)
    • позволяет не указывать скорость выполнения процессов
  • моделирования прототипа системы
    • не ограничивает реализацию заданным порядком выполнения операторов
  • построения абстракции реальной системы
    • модель может быть построена по неполной информации

Вычисления

  1. Конечный фрагмент вычисления σ системы переходов TS называется конечная последовательность чередующихся состояний и действий \sigma = s_0 a_1 s_1 a_2 s_2 \dots a_n s_n, \forall i \in [0,n] \Rightarrow s_i \overset{a_{i+1}}{\rightarrow} s_{i+1}
  2. Бесконечный (максимальный) фрагмент вычисления ρ - \rho = s_0 a_1 s_1 a_2 s_2 \dots, \forall i \geqslant 0 \Rightarrow s_i \overset{a_{i+1}}{\rightarrow} s_{i+1}
  3. Начальный фрагмент вычисления - фрагмент вычисления, для которого s_0 \in I
  4. Вычисление - начальный максимальный фрагмент вычисления

Достижимое состояние (из начального) в системе переходов TS - такое состояние s \in S, для которого существует конечный фрагмент вычисления s_0 a_1 s_1 a_2 s_2 \dots a_n s_n = s

Rich(TS) - множество всех достижимых состояний в TS

Трасса tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega

Свойства линейного времени

  • Свойство \varphi определяет набор допустимых трасс: \varphi \in (2^{AP})^\omega
  • Система переходов TS удовлетворяет свойству линейного времени \varphi
    • TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi
    • TS(P) \models \varphi ~~ \equiv ~~ P \models \varphi

Моделирование программ. Графы программ. Статическая и операционная семантика.

Параллелизм. Чередование систем переходов.

Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.

Параллелизм. Синхронный параллелизм. Рандеву.

Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.

Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.

Представим трассу в форме интерпретации I: I(tr) = <N, \leqslant, \xi>

  • N - множество натуральных чисел
  • \leqslant - отношение порядка на N
  • \xi: N \times AP \rightarrow \{true, false\}, ~~ \forall n>0, p \in AP ~~ \Rightarrow ~~ \xi(n, p) = true \Leftrightarrow p \in L(s)

Рассмотрим трассы tr и tr' такие, что

  • I(tr) = <N, \leqslant, \xi>, ~~ \xi: N \times AP = \{true, false\}
  • I(tr) = <N, \leqslant, \xi'>, ~~ \xi: N \times AP' = \{true, false\}

Будем говорить, что трасса tr' является абстракцией трассы tr, если

  1. AP' \subseteq AP
  2. \exists \alpha : N \rightarrow N такое, что \forall n,k \in N, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k)
  3. \forall n \in N, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(n, p)

Пример абстракции трассы: Лекция 2, слайд 53

Условие корректности модели - \forall tr \in Traces(TS(P)) \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr', где

  • P - система
  • M - модель этой системы

При этом, если \varphi - некоторое свойство системы, то M \models \varphi ~ \Rightarrow ~ P \models \varphi выполняется тогда и только тогда, когда верно условие корректности модели.

Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.

Абстракция. Абстракция графов программ. Отношение слабой симуляции.

Получено с http://esyr.us/wiki/%D0%92%D0%9F%D0%BD%D0%9C/%D0%A2%D0%B5%D0%BE%D1%80%D0%BC%D0%B8%D0%BD
Личные инструменты
Разделы