Редактирование: ВПнМ/Теормин

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

Перейти к: навигация, поиск

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 92 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

Текущая версия Ваш текст
Строка 3: Строка 3:
[[Изображение:Verif1.png|400px|thumb|right|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
[[Изображение:Verif1.png|400px|thumb|right|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
-
'''Состояние программы''' - совокупность значений объектов данных и счётчика управления, связанных с некоторой моделью программы.
+
'''Состояние программы''' - совокупность значений переменных и управления, связанных с некоторой моделью программы.
'''Модель''' - упрощённое описание реальности, выполненное с определенной целью.
'''Модель''' - упрощённое описание реальности, выполненное с определенной целью.
Строка 74: Строка 74:
'''Reach(TS)''' - множество всех достижимых состояний в TS
'''Reach(TS)''' - множество всех достижимых состояний в TS
-
'''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math>; <math>~\omega</math> означает, что трасса может быть бесконечной
+
'''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math>
====Свойства линейного времени====
====Свойства линейного времени====
Строка 90: Строка 90:
** <math> dom(v) = D_p^v \subseteq D_p</math> -- каждая переменная принадлежит какому-либо домену
** <math> dom(v) = D_p^v \subseteq D_p</math> -- каждая переменная принадлежит какому-либо домену
* <math>n</math> -- подстановка. <math>n: V_p \rightarrow D_p, \forall v \in Var</math> <math>n(v) \in D_p^v</math>
* <math>n</math> -- подстановка. <math>n: V_p \rightarrow D_p, \forall v \in Var</math> <math>n(v) \in D_p^v</math>
-
* <math>~ Cond(V_p)</math> -- Набор булевых условий над <math>V_p</math>
+
* <math>Cond(V_p)</math> -- Набор булевых условий над <math>V_p</math>
-
** формулы пропозициональной логики (<math>p1 \or p2</math>)
+
** формулы пропозициональной логики
-
** условия на переменные вида <math>x \in X</math> (p1: 3<=y<18, p2: f=4)
+
** условия на переменные
-
* <math>~ Eval(Var)</math> -- множество значений переменных. Собственно, это и есть подстановка.
+
* <math>Eval(Var)</math> -- множество значений переменных. Собственно, это и есть подстановка.
* Эффект операторов: <math>Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math>
* Эффект операторов: <math>Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math>
Строка 100: Строка 100:
<math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math>
<math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math>
-
* <math>~ Loc</math> -- множество точек
+
* <math>Loc</math> -- множество точек
** <math>Loc_0 \in Loc</math> -- множество начальных точек
** <math>Loc_0 \in Loc</math> -- множество начальных точек
-
* <math>~ Act</math> -- множество действий
+
* <math>Act</math> -- множество действий
* <math>\rightarrow \subseteq Loc \times (Cond(V_p) \times Act) \times Loc </math> -- отношение перехода (<math>Cond(V_p) </math> -- это фактически страж оператора )
* <math>\rightarrow \subseteq Loc \times (Cond(V_p) \times Act) \times Loc </math> -- отношение перехода (<math>Cond(V_p) </math> -- это фактически страж оператора )
-
* <math>~ Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math> -- функция эффекта
+
* <math>Effect</math> -- функция эффекта
* <math>g_0 \in Cond(V_p)</math> -- начальное условие
* <math>g_0 \in Cond(V_p)</math> -- начальное условие
Строка 113: Строка 113:
** находимся в точке программы l
** находимся в точке программы l
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
-
* Состояния <math>\langle l,n \rangle</math> размечаются высказыванием о том, что мы находимся в точке программы <math>~ l</math> и всеми высказываниями, истинными в <math>~ n</math>
+
* Состояния <math>\langle l,n \rangle</math> размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
-
* Если в графе программы есть дуга из <math>~ l</math> в <math>~ l'</math> со стражем <math>~ g</math> и действием <math>~ a</math> и в некоторой подстановке <math>~n</math> выполняется страж <math>~ g</math>, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния <math>\langle l,n\rangle</math> в состояние <math>\langle l', Effect(a,n)\rangle</math> по действию <math>~ a</math>.
+
* Если в графе программы есть дуга из l в <math>l'</math> со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния <math>\langle l,n\rangle</math> в состояние <math>\langle l', Effect(a,n)\rangle</math> по действию a.
'''Системы переходов графов программ'''
'''Системы переходов графов программ'''
Строка 216: Строка 216:
Тогда <math>TS_1 \times TS_2 = \langle S_1 \times S_2, Act, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle </math>, где
Тогда <math>TS_1 \times TS_2 = \langle S_1 \times S_2, Act, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle </math>, где
* <math>L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)</math>
* <math>L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)</math>
-
* <math>\rightarrow</math> определяется как: <math>\frac{s_1 \overset{\alpha}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{\beta}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{\alpha * \beta}{\rightarrow} \langle s_1', s_2' \rangle}</math>
+
* <math>\rightarrow</math> определяется как: <math>\frac{s_1 \overset{\alpha}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{\beta}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{\alpha * \beta}{\rightarrow} \langle s_1', s_2 \rangle}</math>
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
Строка 585: Строка 585:
** '''Слабый Until:'''
** '''Слабый Until:'''
*** всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e)
*** всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e)
-
*** <math>s_i \models e W f ~~ \Leftrightarrow ~~ s_i \models f \vee (s_i \models e \wedge s_{i+1} \models e W f)</math>
+
*** <math>s_i \models e \cup f ~~ \Leftrightarrow ~~ s_i \models f \vee (s_i \models e \wedge s_{i+1} \models e \cup f)</math>
** '''Сильный Until:'''
** '''Сильный Until:'''
*** всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
*** всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
Строка 884: Строка 884:
* Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний),
* Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний),
* Варди и Вольпер, 1986 – новая техника model checking (анализ конформности),
* Варди и Вольпер, 1986 – новая техника model checking (анализ конформности),
-
* Хольцман, 1989 – верификатор SPIN.
+
* Хольцман, 1981 – верификатор SPIN.
* Бриан, 1989 – Двоичные решающие диаграммы (BDD),
* Бриан, 1989 – Двоичные решающие диаграммы (BDD),
* МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD),
* МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD),

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Шаблоны, использованные на этой странице:

Личные инструменты
Разделы