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

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

(Различия между версиями)
Перейти к: навигация, поиск
(/* Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени.)
(/* Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени.)
Строка 36: Строка 36:
=== Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.===
=== Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.===
-
Размеченная система переходов (LTS)
+
'''Размеченная система переходов (LTS)'''
<math>TS = <S, Act, \overset{a}{\rightarrow} ,s_0, AP, L></math>
<math>TS = <S, Act, \overset{a}{\rightarrow} ,s_0, AP, L></math>
-
* S -
+
* S - множество состояний
-
* Act -
+
* Act - множество действий
 +
* '' <math>\tau</math> - невидимое действие ''
* <math>\overset{a}{\rightarrow} \subseteq S \times Act \times S </math> - тотальное отношение переходов
* <math>\overset{a}{\rightarrow} \subseteq S \times Act \times S </math> - тотальное отношение переходов
* <math>s_0 \in S</math> - начальное состояние
* <math>s_0 \in S</math> - начальное состояние
Строка 51: Строка 52:
Пример LTS: Лекция 2, слайд 40-41
Пример LTS: Лекция 2, слайд 40-41
 +
 +
'''Прямые потомки'''
 +
* <math>Post(s, a) = \{s' \in S, s \overset{a}{\rightarrow} s'\}</math> - такие состояния s', которые <u>непосредственно вытекают</u> из s через переход a
 +
* <math>Post(s) = \bigcup_{a \in Act} Post(s, a)</math> - все возможные состояния s', которые <u>непосредственно вытекают</u> из s
 +
 +
Система <math>TS = <S, Act, \overset{a}{\rightarrow} ,s_0, AP, L></math> '''детерменирована''':
 +
* '''по действиям''' тогда и только тогда, когда
 +
** <math>|I| \leqslant 1</math>
 +
** <math>\forall s \in S, \forall a \in Act \Rightarrow |Post(s, a)| \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
=== Моделирование программ. Графы программ. Статическая и операционная семантика. ===
=== Моделирование программ. Графы программ. Статическая и операционная семантика. ===

Версия 10: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 === Моделирование программ. Графы программ. Статическая и операционная семантика. === === Параллелизм. Чередование систем переходов. === === Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными. === === Параллелизм. Синхронный параллелизм. Рандеву. === === Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. === === Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. === === Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. === === Абстракция. Абстракция графов программ. Отношение слабой симуляции. ===
Получено с http://esyr.org/wiki/%D0%92%D0%9F%D0%BD%D0%9C/%D0%A2%D0%B5%D0%BE%D1%80%D0%BC%D0%B8%D0%BD
Личные инструменты
Разделы