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

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

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

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

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

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

Текущая версия Ваш текст
Строка 1: Строка 1:
== Моделирование и абстракция ==
== Моделирование и абстракция ==
=== Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели. ===
=== Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели. ===
-
[[Изображение:Verif1.png|400px|thumb|right|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
+
Схема верификации на моделях (Лекция 2, слайд 3)
-
'''Состояние программы''' - совокупность значений объектов данных и счётчика управления, связанных с некоторой моделью программы.
+
'''Состояние программы''' - совокупность значений переменных и управления, связанных с некоторой моделью программы.
'''Модель''' - упрощённое описание реальности, выполненное с определенной целью.
'''Модель''' - упрощённое описание реальности, выполненное с определенной целью.
Строка 18: Строка 18:
# выбор языка моделирования
# выбор языка моделирования
# абстракция системы до модели с учётом требований
# абстракция системы до модели с учётом требований
-
[[Изображение:Verif2.png|400px|thumb|center|<u>Построение модели</u> в строгом смысле (''Лекция 2, слайд 38'')]]
 
- 
-
Состояние называется <u>достижимым</u>, если существует вычисление программы, в котором оно присутствует
 
=== Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.===
=== Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.===
Строка 32: Строка 29:
* Act - множество действий
* Act - множество действий
* '' <math>\tau</math> - невидимое действие ''
* '' <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>I</math> - множество начальных состояний
+
* <math>s_0 \in S</math> - начальное состояние
* AP - множество атомарных высказываний
* AP - множество атомарных высказываний
* <math>L:S \rightarrow 2^{AP}</math> - функция разметки
* <math>L:S \rightarrow 2^{AP}</math> - функция разметки
Строка 50: Строка 47:
* '''по действиям''' тогда и только тогда, когда
* '''по действиям''' тогда и только тогда, когда
** <math>|I| \leqslant 1</math>
** <math>|I| \leqslant 1</math>
-
** <math>\forall s \in S, \forall a \in Act \Rightarrow |Post(s, a)| \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>|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> ( количество одинаково размеченных потомков не больше одного )
Строка 68: Строка 65:
# '''Бесконечный (максимальный) фрагмент вычисления <math>\rho</math>''' - <math>\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}</math>
# '''Бесконечный (максимальный) фрагмент вычисления <math>\rho</math>''' - <math>\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}</math>
# '''Начальный фрагмент вычисления''' - фрагмент вычисления, для которого <math>s_0 \in I</math>
# '''Начальный фрагмент вычисления''' - фрагмент вычисления, для которого <math>s_0 \in I</math>
-
# '''Вычисление''' - начальный максимальный фрагмент вычисления (описывает последовательность состояний и действий)
+
# '''Вычисление''' - начальный максимальный фрагмент вычисления
'''Достижимое состояние''' (из начального) в системе переходов TS - такое состояние <math>s \in S</math>, для которого существует конечный фрагмент вычисления <math>s_0 a_1 s_1 a_2 s_2 \dots a_n s_n = s</math>
'''Достижимое состояние''' (из начального) в системе переходов TS - такое состояние <math>s \in S</math>, для которого существует конечный фрагмент вычисления <math>s_0 a_1 s_1 a_2 s_2 \dots a_n s_n = s</math>
Строка 74: Строка 71:
'''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>
====Свойства линейного времени====
====Свойства линейного времени====
* Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \subseteq (2^{AP})^\omega</math>
* Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \subseteq (2^{AP})^\omega</math>
-
* Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</math>, если: <math>TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi</math>
+
* Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</math>
-
* по определению программа удовлетворяет свойству &phi;, если её система переходов удовлетворяет этому свойству: <math>P \models \varphi ~~ \equiv ~~ TS(P) \models \varphi </math> -
+
** <math>TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi</math>
 +
** <math>P \models \varphi ~~ \equiv ~~ TS(P) \models \varphi </math> - по определению программа удовлетворяет свойству &phi;, если её система переходов удовлетворяет этому свойству
=== Моделирование программ. Графы программ. Статическая и операционная семантика. ===
=== Моделирование программ. Графы программ. Статическая и операционная семантика. ===
Строка 90: Строка 88:
** <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: Строка 98:
<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: Строка 111:
** находимся в точке программы 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.
'''Системы переходов графов программ'''
'''Системы переходов графов программ'''
Строка 121: Строка 119:
* <math>S = Loc \times Eval(V_p)</math> (декартово произведение точек программы на всевозможные подстановки)
* <math>S = Loc \times Eval(V_p)</math> (декартово произведение точек программы на всевозможные подстановки)
-
* <math>\rightarrow : S \times Act \times S </math> с соответствующим правилом вывода <math> \frac{l \overset{g:a}{\rightarrow} l' \and (n \models g) }{\langle l,n \rangle \overset{a}{\rightarrow} \langle l',Effect(a,n) \rangle }</math>
+
* <math>\rightarrow : S \times Act \times S </math> с соответствующим правилом вывода <math> \frac{l \overset{g:a}{\rightarrow} l \and (n \models g) }{\langle l,n \rangle \overset{a}{\rightarrow} \langle l',Effect(a,n) \rangle }</math>
* Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы:
* Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы:
-
** <math>I=\{\langle l , n \rangle : l \in Loc_0 , n \models g_0 \}</math>
+
** <math>I={\langle l , n \rangle : l \in Loc_0 , n \models g_0 }</math>
* Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы:
* Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы:
** <math>AP=Loc \cup Cond(V_P) </math>
** <math>AP=Loc \cup Cond(V_P) </math>
* Состояния вида <math>\langle l,n \rangle</math> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
* Состояния вида <math>\langle l,n \rangle</math> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
-
** <math>L(\langle l , n \rangle)= \{l\} \cup \{g \in Cond(V_P): n \models g \}.</math>
+
** <math>L(\langle l , n \rangle)= (l) \cup (g \in Cond(V_P): n \models g ).</math>
-
'''Пример: Лекция 4, слайд 16'''
+
''Пример: Лекция 4, слайд 16''
-
 
+
-
 
+
-
'''Статическая и операционная семантика'''
+
-
 
+
-
'''Cтатическая семантика''' – набор ограничений, которым должна удовлетворять структура программы;
+
-
'''Операционная семантика''' – понятие состояния программы и изменение состояния в ходе работы программы; то, как по графу строится LTS.
+
-
(См. Л.5, сл. 15, 2010 )
+
=== Параллелизм. Чередование систем переходов. ===
=== Параллелизм. Чередование систем переходов. ===
Строка 168: Строка 159:
'' Лекция 4, слайды 25—28 ''
'' Лекция 4, слайды 25—28 ''
-
Для графов программ <math>PG_1</math> (над <math>V_1</math>) и <math>PG_2</math> (над <math>V_2</math>) без разделяемых переменных (т. е. <math>V_1 \cap V_2 = \varnothing</math>):
+
Для графов программ <math>PG_1</math> (над <math>V_1</math>) и <math>PG_2</math> (над <math>V_2</math>) без разделяемых переменных (т. е. <math>V_1 \cap V_2 = \emptyset</math>), формула
-
* формула <math>TS(PG_1)~|||~TS(PG_2)</math> достоверно описывает параллельную композицию <math>PG_1</math> и <math>PG_2</math>
+
:<math>TS(PG_1)~|||~TS(PG_2)</math>
-
* в случае с разделяемыми переменными это не так (см. лекцию 4, слайд 26).
+
достоверно описывает параллельную композицию <math>PG_1</math> и <math>PG_2</math>. В случае с разделяемыми переменными это не так (см. лекцию 4, слайд 26).
Пусть
Пусть
Строка 177: Строка 168:
:<math>PG_1~|||~PG_2 = \langle Loc_1 \times Loc_2, Act_1 \cup Act_2, Effect, \rightarrow, Loc_{0,1} \times Loc_{0,2}, g_{0,1} \land g_{0,2} \rangle,</math>
:<math>PG_1~|||~PG_2 = \langle Loc_1 \times Loc_2, Act_1 \cup Act_2, Effect, \rightarrow, Loc_{0,1} \times Loc_{0,2}, g_{0,1} \land g_{0,2} \rangle,</math>
где отношение перехода <math>\rightarrow</math> определяется следующими правилами вывода:
где отношение перехода <math>\rightarrow</math> определяется следующими правилами вывода:
-
:<math>l_1 \overset{g:\alpha}{\rightarrow}_1 l'_1 \over \langle l_1, l_2 \rangle \overset{g:\alpha}{\rightarrow} \langle l'_1, l_2 \rangle</math> и <math>l_2 \overset{g:\alpha}{\rightarrow}_2 l'_2 \over \langle l_1, l_2 \rangle \overset{g:\alpha}{\rightarrow} \langle l_1, l'_2 \rangle,</math>
+
:<math>l_1 \overset{g:a}{\rightarrow}_1 l'_1 \over \langle l_1, l_2 \rangle \overset{g:a}{\rightarrow} \langle l'_1, l_2 \rangle</math> и <math>l_2 \overset{g:a}{\rightarrow}_2 l'_2 \over \langle l_1, l_2 \rangle \overset{g:a}{\rightarrow} \langle l_1, l'_2 \rangle,</math>
а <math>Effect(\alpha,~\eta) = Effect_i(\alpha,~\eta),</math> если <math>\alpha \in Act_i.</math>
а <math>Effect(\alpha,~\eta) = Effect_i(\alpha,~\eta),</math> если <math>\alpha \in Act_i.</math>
Строка 216: Строка 207:
Тогда <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>
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
Строка 231: Строка 222:
<u>Системы с каналами.</u>
<u>Системы с каналами.</u>
-
* Граф программы <math>PG</math> над <math>(Var, Chan)</math> задаётся <math>PG = \langle Loc, Act, Effect, \rightarrow, Log_0, g_0 \rangle</math>, где <math>\rightarrow \subseteq Loc \times (Cond(Var) \times Act) \times Loc ~ \cup ~ Loc \times Comm \times Loc</math>
+
* Граф программы задаётся <math>PG = \langle Loc, Act, Effect, \rightarrow, Log_0, g_0 \rangle</math>, где <math>\rightarrow \subseteq Loc \times (Cond(Var) \times Act) \times Loc ~ \cup ~ Loc \times Comm \times Loc</math>
-
* Система с каналами <math>CS</math> над <math>\left(\cup_{1 \leqslant i \leqslant n} PG_i, Chan\right)</math> задаётся как <math>CS = \left[PG_1 | PG_2 | \dots | PG_n\right]</math>, где <math>PG_i</math> граф программы над <math>(Var_i, Chan)</math>
+
* Система с каналами CS над <math>\bigcup_{1 \leqslant i \leqslant n} PG_i, Chan</math> задаётся как <math>\left[PG_1, PG_2, \dots, PG_n \right]</math>, где <math>PG_i</math> -- граф программы над <math>(Var_i, Chan)</math>
-
 
+
-
При асинхронной передаче сообщений (при <math>cap(c) > 0</math>):
+
-
* процесс <math>P_i</math> может выполнить <math>l_i \overset{c!v}{\rightarrow} l'_i</math>, только если в <math>c</math> хранится меньше <math>cap(c)</math> сообщений;
+
-
* процесс <math>P_j</math> может выполнить <math>l_j \overset{c?x}{\rightarrow} l'_j</math>, только если <math>c</math> не пуст, после чего первый элемент <math>v</math> извлекается из <math>c</math> и присваивается <math>x</math> (атомарно).
+
-
 
+
-
'''Оценка <math>\xi</math> значения канала''' <math>c</math> — это отображение канала на последовательность значений <math>\xi: Chan \rightarrow dom(c)^*</math>, такое что длина последовательности не превосходит ёмкости канала <math>len(\xi(c)) \leq cap(c)</math>, и при этом <math>\xi(c)=v_1 v_2 \dots v_k</math> означает, что <math>v_1</math> — верхнее сообщение в буфере.
+
-
:<math>\xi[c = v_1 v_2 \dots v_k](c') = \left\{ \begin{array}{cc}
+
-
\xi(c'), & c \neq c' \\
+
-
v_1 v_2 \dots v_k, & c = c' \\
+
-
\end{array} \right.</math> ''Кто понимает смысл этой хренотени, опишите, плз. [[Участник:Overrider|Overrider]] 18:28, 22 мая 2009 (UTC)''
+
-
 
+
-
Исходная оценка <math>\xi_0(c) = \epsilon, \forall c \in Chan</math>
+
-
 
+
-
''Операционная семантика: лекция 4, слайды 44—46''
+
-
 
+
-
====операционная семантика====
+
-
 
+
-
Пусть <math>CS = \left[PG_1 | PG_2 | \dots | PG_n\right]</math> – система с каналами над <math>(Chan, Var)</math>, и
+
-
 
+
-
<math>PG = \langle Loc, Act, Effect, \rightarrow, Log_0, g_0 \rangle</math>
+
-
 
+
-
Система переходов <math>TS(CS)</math> описывается сигнатурой
+
-
 
+
-
<math>TS(CS) = \langle S, Act, \rightarrow, I , AP, L \rangle </math>, где
+
-
 
+
-
<math>S = ( Loc_1 \times \dots \times Loc_n ) \times Eval(Var) \times Eval(Chan)</math>
+
-
 
+
-
<math>Act = ( \cup_{0 \leqslant i \leqslant n} Act_i ) ~ \cup ~ \tau </math>
+
-
 
+
-
<math>I = \{
+
-
\langle
+
-
l_1, \dots, l_n, \eta, \xi
+
-
\rangle
+
-
|
+
-
\forall i ( l_i \in Loc_{0i} \and \eta \models g_0 ) \and \forall c ( \xi_0(c) = \epsilon )
+
-
\}</math>
+
-
 
+
-
<math>AP = ( \cup_{0 \leqslant i \leqslant n} Loc_i ) \cup Cond(Var)</math>
+
-
 
+
-
<math>L(
+
-
\langle
+
-
l_1, \dots, l_n, \eta, \xi
+
-
\rangle
+
-
) =
+
-
\{
+
-
l_1, \dots, l_n
+
-
\}
+
-
\cup
+
-
\{
+
-
g \in Cond( Var ) | \eta \models g
+
-
\}</math>
+
-
 
+
-
'''Правила вывода'''
+
-
<ul>
+
-
<li> <p> интерливинг для <math> \alpha \in Act_i </math> </p>
+
-
<p><math>
+
-
\frac
+
-
{l_i \overset{g:\alpha}{\rightarrow} l_i' \and n \models g }
+
-
{
+
-
\langle
+
-
l_1, \dots , l_i, \dots , l_n , \eta, \xi
+
-
\rangle
+
-
\overset{\alpha}{\rightarrow}
+
-
\langle
+
-
l_1, \dots, l_i', \dots, l_n , \eta', \xi
+
-
\rangle
+
-
}
+
-
</math></p>
+
-
 
+
-
</li>
+
-
<li> <p>Синхронная передача сообщений через <math>c \in Chan, cap(c) = 0</math></p>
+
-
 
+
-
<p>
+
-
<math>
+
-
\frac
+
-
{
+
-
l_i \overset{c?x}{\rightarrow} l_i' \and
+
-
l_j \overset{c!v}{\rightarrow} l_j' \and
+
-
i \neq j
+
-
}
+
-
{
+
-
\langle
+
-
l_1, \dots , l_i, \dots, l_j, \dots , l_n , \eta, \xi
+
-
\rangle
+
-
\overset{\alpha}{\rightarrow}
+
-
\langle
+
-
l_1, \dots, l_i', \dots, l_j', \dots , l_n , \eta', \xi
+
-
\rangle
+
-
}
+
-
</math>
+
-
</p>
+
-
</li>
+
-
<li>
+
-
<p>
+
-
Асинхронная передача сообщений через <math>c \in Chan, cap(c) \neq 0</math>
+
-
</p>
+
-
<ul>
+
-
<li>
+
-
<p>
+
-
получить значение по каналу c и присвоить переменной x:
+
-
</p>
+
-
 
+
-
<p>
+
-
<math>
+
-
\frac
+
-
{
+
-
l_i \overset{c?x}{\rightarrow} l_i' \and
+
-
len(\xi(c))=k>0) \and
+
-
\xi(c)=v_1 \dots vk
+
-
}
+
-
{
+
-
\langle
+
-
l_1, \dots , l_i, \dots , l_n , \eta, \xi
+
-
\rangle
+
-
\overset{c?x}{\rightarrow}
+
-
\langle
+
-
l_1, \dots, l_i', \dots, l_n , \eta', \xi'
+
-
\rangle
+
-
}
+
-
</math>,
+
-
</p>
+
-
 
+
-
<p>
+
-
где
+
-
<math>
+
-
\eta' = \eta[x=v_1], \xi'=\xi[c=v_2 \dots v_k ]
+
-
</math>
+
-
</p>
+
-
 
+
-
</li>
+
-
 
+
-
<li>
+
-
<p>
+
-
передать значение <math>v \in dom(c) </math> по каналу c:
+
-
</p>
+
-
<p>
+
-
<math>
+
-
\frac
+
-
{
+
-
l_i \overset{c!v}{\rightarrow} l_i' \and
+
-
len(\xi(c))=k<cap(c)) \and
+
-
\xi(c)=v_1 \dots vk
+
-
}
+
-
{
+
-
\langle
+
-
l_1, \dots , l_i, \dots , l_n , \eta, \xi
+
-
\rangle
+
-
\overset{c!v}{\rightarrow}
+
-
\langle
+
-
l_1, \dots, l_i', \dots, l_n , \eta, \xi'
+
-
\rangle
+
-
}
+
-
</math>,
+
-
</p>
+
-
<p>
+
-
где
+
-
<math>
+
-
\xi'=\xi[c=v_1 \dots v_k v ]
+
-
</math>
+
-
</p>
+
-
</li>
+
-
</ul>
+
-
</li>
+
-
</ul>
+
-
 
+
-
<math></math>
+
-
<math></math>
+
=== Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. ===
=== Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. ===
-
Представим трассу в форме интерпретации I: <math>I(tr) = \langle\mathbb{N}, \leqslant, \xi\rangle</math>
+
Представим трассу в форме интерпретации I: <math>I(tr) = <\mathbb{N}, \leqslant, \xi></math>
* <math>\mathbb{N}</math> - множество натуральных чисел
* <math>\mathbb{N}</math> - множество натуральных чисел
* <math>\leqslant</math> - отношение порядка на <math>\mathbb{N}</math>
* <math>\leqslant</math> - отношение порядка на <math>\mathbb{N}</math>
Строка 409: Строка 233:
Рассмотрим трассы tr и tr' такие, что
Рассмотрим трассы tr и tr' такие, что
-
* <math>I(tr) = \langle\mathbb{N}, \leqslant, \xi\rangle, ~~ \xi: \mathbb{N} \times AP = \{true, false\}</math>
+
* <math>I(tr) = <\mathbb{N}, \leqslant, \xi>, ~~ \xi: \mathbb{N} \times AP = \{true, false\}</math>
-
* <math>I(tr') = \langle\mathbb{N}, \leqslant, \xi'\rangle, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math>
+
* <math>I(tr) = <\mathbb{N}, \leqslant, \xi'>, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math>
-
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \prec tr'</math>), если
+
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \leqslant tr'</math>), если
# <math>AP' \subseteq AP</math>
# <math>AP' \subseteq AP</math>
# <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что
# <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что
Строка 420: Строка 244:
Пример абстракции трассы: Лекция 2, слайд 53
Пример абстракции трассы: Лекция 2, слайд 53
-
'''Определение.''' Пусть P – система, φ – произвольное свойство линейного времени. '''Корректной моделью ''' P называется такая М, что:
+
''' Необходимое условие корректности модели ''' - <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr'</math>, где
-
<math> M \models \phi \Rightarrow P \models \phi </math>.
+
* <math>P</math> - система
-
''(позволяет проверять свойства программы на её модели )''
+
* <math>M</math> - модель этой системы
-
''' Необходимое и достаточное условие корректности модели:'''
+
При этом, если <math>\varphi</math> - некоторое свойство системы, то <math>M \models \varphi ~ \Rightarrow ~ P \models \varphi</math> выполняется тогда и только тогда, когда верно условие корректности модели.
-
Модель <math>M</math> системы <math>P</math> корректна тогда и только тогда, когда <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \prec tr'</math>.
+
-
''(для проверки такого условия нужно рассмотреть все трассы исходной системы, допускает, что в модели
+
-
больше состояний )''
+
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. ===
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. ===
Строка 445: Строка 266:
* Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap 2^{AP^2}</math>
* Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap 2^{AP^2}</math>
-
Модель называется '''адекватной''', если:
+
'''Необходимое (но не достаточное) [?] условие адекватности модели свойствам правильности''' :
-
* Атомарные высказывания, в терминах которых задаются свойства, присутствуют в разметке модели. ''(Необходимое условие)''
+
-
* Из нарушения свойства на модели следует, что оно нарушается и на исходной системе. ''(Достаточное условие)''
+
-
'''Необходимое условие адекватности модели свойствам правильности''': алфавит предикатов свойств правильности включен в алфавит предикатов модели — <math>AP_\phi \subseteq AP_M</math>. Условие не является достаточным (см. примеры, лекция 3, слайды 4—5).
+
Алфавит предикатов свойств правильности включен в алфавит предикатов модели.
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. ===
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. ===
Строка 467: Строка 286:
=== Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. ===
=== Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. ===
-
''Лекция 5, слайды 2-14.''
 
-
'''Требования правильности''' утверждения о возможных и невозможных вариантах выполнения программы.
+
'''Требования правильности''' -- утверждения о возможных и невозможных вариантах выполнения программы.
<u>Двойственность</u> :
<u>Двойственность</u> :
-
* если какое-то утверждение невозможно, то обратное неизбежно
+
* если какое-то утверждение невозможно, то обратное -- неизбежно
-
* если какое-то утверждение неизбежно, то обратное невозможно
+
* если какое-то утверждение неизбежно, то обратное -- невозможно
* при помощи логики от одного можно переходить к другому при помощи отрицания
* при помощи логики от одного можно переходить к другому при помощи отрицания
Строка 481: Строка 299:
* в Promela:
* в Promela:
** свойства состояний
** свойства состояний
-
*** [http://en.wikipedia.org/wiki/Assertion_%28computing%29 asserts]:
+
*** asserts
**** локальные ассерты процессов
**** локальные ассерты процессов
-
**** [http://ru.wikipedia.org/wiki/%D0%98%D0%BD%D0%B2%D0%B0%D1%80%D0%B8%D0%B0%D0%BD%D1%82#.D0.98.D0.BD.D0.B2.D0.B0.D1.80.D0.B8.D0.B0.D0.BD.D1.82.D1.8B_.D0.B2_.D0.BF.D1.80.D0.BE.D0.B3.D1.80.D0.B0.D0.BC.D0.BC.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.B8.D0.B8 инварианты] системы процессов
+
**** инварианты системы процессов
*** метки терминальных состояний
*** метки терминальных состояний
**** задаём допустимые точки останова прочесса
**** задаём допустимые точки останова прочесса
** свойства последовательностей состояний
** свойства последовательностей состояний
-
*** метки прогресса чтобы найти циклы бездействия
+
*** метки прогресса - чтобы найти циклы бездействия
-
*** утверждения о невозможности (never claims) например, LTL формулы
+
*** утверждения о невозможности (never claims) - например, LTL формулы
-
*** трассовые ассерты используются для описания правильных последовательностей выполнения операторов отправки и приема сообщения
+
*** трассовые ассерты - используются для описания правильных последовательностей выполнения операторов отправки и приема сообщения
=== Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств. ===
=== Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств. ===
Строка 502: Строка 320:
** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.
** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.
-
'''ps'''. автор терминов – Лесли Лампорт; см. ''Лекция 5, слайд 4''.
 
=== Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. ===
=== Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. ===
Строка 557: Строка 374:
<u>Формула в LTL '''f::='''</u>
<u>Формула в LTL '''f::='''</u>
-
* '''p, q, ... ''' свойства состояний, включая '''true''' и '''false'''
+
* '''p, q, ... ''' -- свойства состояний, включая '''true''' и '''false'''
-
* '''(f)''' группировка при помощи скобок
+
* '''(f)''' -- группировка при помощи скобок
-
* '''<math>\alpha ~ f</math>''' унарные операторы
+
* '''<math>\alpha ~ f</math>''' -- унарные операторы
-
* '''<math>f_1 ~ \beta ~ f_2</math>''' бинарные операторы
+
* '''<math>f_1 ~ \beta ~ f_2</math>''' -- бинарные операторы
<u>Операторы в LTL</u>
<u>Операторы в LTL</u>
* унарные
* унарные
-
** <math>\Box</math> ([]) всегда в будущем, т.е. <math>s_j \models \Box f ~~~ \Leftrightarrow ~~~ \forall j, j \geqslant i: ~ s_j \models f</math>
+
** <math>\Box</math> ([]) -- всегда в будущем
-
** <math>\Diamond</math> (<>) в конце концов, т.е. <math>s_j \models \Diamond f ~~~ \Leftrightarrow ~~~ \exists j, j \geqslant i: ~ s_j \models f</math>
+
** <math>\diamond</math> (<>) -- в конце концов
-
** <math>X</math> (X) в следующем состоянии, т.е. <math>s_j \models X f ~~~ \Leftrightarrow ~~~ i: ~ s_{j+1} \models f</math>
+
** <math>X</math> (X) -- в следующем состоянии
-
** <math>\neg</math> (!) логическое отрицание
+
** <math>\neg</math> (!) -- логическое отрицание
* бинарные
* бинарные
-
** <math>\wedge</math> (&&) логическое И
+
** <math>U</math> (U) -- до тех пор, пока
-
** <math>\vee</math> (||) логическое ИЛИ
+
** <math>\wedge</math> (&&) -- логическое И
-
** <math>\rightarrow</math> (->) логическая импликация
+
** <math>\vee</math> (||) -- логическое ИЛИ
-
** <math>\leftrightarrow</math> (<->) логическая эквивалентность
+
** <math>\rightarrow</math> (->) -- логическая импликация
-
** <math>U</math> (U) — до тех пор, пока (until)
+
** <math>\leftrightarrow</math> (<->) -- логическая эквивалентность
-
====Выполнимость формул:====
+
'''Сильный Until:'''
-
* Задаётся последовательность состояний прохода <math>\sigma: s_0, s_1, s_2, \dots</math>
+
* всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
-
* <math>\forall i, i \geqslant 0, ~ \forall p </math> определена выполнимость <math> p </math> в <math> s_i </math>
+
* <math>s_i \models e U f ~~ \Leftrightarrow ~~ \begin{cases}
-
* Семантика LTL:
+
-
** <math>\sigma \models f \Leftrightarrow s_0 \models f</math>
+
-
** <math>s_i \models \Box f \Leftrightarrow \forall j, j \geqslant i: s_j \models f</math>
+
-
** <math>s_i \models \Diamond f \Leftrightarrow \exists j, j \geqslant i: s_j \models f</math>
+
-
** <math>s_i \models Xf \Leftrightarrow s_{i+1} \models f </math>
+
-
** '''Слабый Until:'''
+
-
*** всегда 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>
+
-
** '''Сильный Until:'''
+
-
*** всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
+
-
*** <math>s_i \models e U f ~~ \Leftrightarrow ~~ \begin{cases}
+
\exists j, j \geqslant i: ~ s_j \models f \\
\exists j, j \geqslant i: ~ s_j \models f \\
\forall k, i \leqslant k < j: ~ s_k \models e
\forall k, i \leqslant k < j: ~ s_k \models e
\end{cases}</math>
\end{cases}</math>
 +
 +
'''Слабый Until:'''
 +
* всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e)
 +
* <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>
 +
 +
<u>Выполнимость формул:</u>
 +
* Задаётся последовательность состояний прохода <math>\sigma</math>
 +
* <math>\forall i, i \geqslant 0, ~ \forall p ~~ : ~~ s_i \models p </math> '' Внимание!! это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!! ''
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. ===
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. ===
Строка 694: Строка 508:
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. ===
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. ===
-
При помощи конструкции never можно описать любой &omega;-регулярный автомат над словами
+
При помощи конструкции never можно описать любой w-регулярный автомат над словами
'''Выразительная мощность LTL'''
'''Выразительная мощность LTL'''
Строка 707: Строка 521:
(p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного.
(p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного.
-
<math>\exists </math> t(t && [](t -> X!t) && [](!t -> Xt) && [](!t -> !p))
+
<math>\exists </math> t.t && [](t -> X!t) && [](!t -> Xt) && [](!t -> !p)
LTL-формула описывает свойство, которое должно выполняться на '''всех''' вычислениях, начинающихся из исходного остояния системы
LTL-формула описывает свойство, которое должно выполняться на '''всех''' вычислениях, начинающихся из исходного остояния системы
Строка 713: Строка 527:
'''Логика СTL*'''
'''Логика СTL*'''
* Логика ветвящегося времени:
* Логика ветвящегося времени:
-
** использует кванторы ∀ и ∃ для обозначения трасс, на которых может выполняться свойство
+
** использует кванторы ∀ и ∃
** использует F вместо <> и G вместо []
** использует F вместо <> и G вместо []
'''Логика СTL'''
'''Логика СTL'''
-
Логика CTL – фрагмент логики CTL*, в котором кванторы могут встречаться только парами, причём в паре должны обязательно находиться один временной и один пространственный кванторы. Например: AG EF(p), A(p U q).
+
Логика CTL – фрагмент логики CTL*, в котором под управлением квантора пути (E или A) может находиться не более дного
 +
оператора X или U
'''Выразительные возможности CTL* и CTL'''
'''Выразительные возможности CTL* и CTL'''
Строка 745: Строка 560:
<u>Методы верификации:</u>
<u>Методы верификации:</u>
-
* "Полное" тестирование (''Лекция 1, слайды 14-22'')
+
* "Полное" тестирование (слайды 14-22)
-
* Имитационное моделирование ([http://ru.wikipedia.org/wiki/Имитационное_моделирование вики])
+
* Имитационное моделирование
-
* Доказательство теорем (''слайды 27-29'')
+
* Доказательство теорем (27-29)
-
* Статический анализ (''слайды 30-33'')
+
* Статический анализ (30-33)
-
* Верификация на моделях (''слайды 34-38'')
+
* Верификация на моделях (34-38)
<u>Типы программ:</u>
<u>Типы программ:</u>
Строка 766: Строка 581:
=== Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. ===
=== Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. ===
-
«Тестирование может показать присутствие ошибок, но не может показать их отсутствия» © Дейкстра.
 
- 
-
Обоснование полноты тестового покрытия:
 
-
* метод «чёрного ящика» (ЧЯ) — полное покрытие входных данных,
 
-
* метод «прозрачного ящика» (ПЯ) — полное покрытие кода программы.
 
-
Плюсы применения тестирования:
 
-
* проверяется та программа, которая будет использоваться,
 
-
* не требуется знание/использование дополнительных инструментальных средств,
 
-
* удобная локализация ошибки.
 
-
Минусы применения тестирования:
 
-
* не всегда есть условия для тестирования системы,
 
-
* проблема с воспроизводимостью тестов (частичное решение — имитационное моделирование).
 
- 
-
====Проблема полноты тестового покрытия====
 
-
* Чёрный ящик:
 
-
** для последовательных программ сложно перебрать все входные данные,
 
-
** для параллельных программ — очень сложно,
 
-
** для динамических структур данных, взаимодействия с окружением — невозможно.
 
-
* Прозрачный ящик:
 
-
** большой размер покрытия,
 
-
** часто невозможно построить 100% покрытие,
 
-
** полное покрытие не гарантирует отсутствия ошибок.
 
-
Итоги:
 
-
* Полный перебор входных данных — невозможен.
 
-
* Полнота покрытия кода не гарантирует правильности.
 
-
* Ошибка — ошибочное вычисление системы.
 
-
* Полнота в терминах возможных вычислений — хороший критерий.
 
=== Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. ===
=== Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. ===
Строка 873: Строка 661:
'' Лекция 1, Слайды 40-44 ''
'' Лекция 1, Слайды 40-44 ''
- 
-
'''История развития''' верификации программ на моделях:
 
-
* Флойд, 1967 – assertions, гипотеза о доказуемости корректности программы,
 
-
* Хоар, 1969 – пред- и пост-условия, триплеты Хоара (P | S | Q), логический вывод,
 
-
* Бойер, Мур, 1971 – первый автоматический прувер,
 
-
* Дейкстра, 1975 – Guarded Command Languages,
 
-
* Хоар, 1978 – взаимодействующие последовательные процессы (CSP).
 
-
* Пнуэли, 1977 – темпоральная логика LTL,
 
-
* Пнуэли, 1981 – логика ветвящегося времени (CTL),
 
-
* Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний),
 
-
* Варди и Вольпер, 1986 – новая техника model checking (анализ конформности),
 
-
* Хольцман, 1989 – верификатор SPIN.
 
-
* Бриан, 1989 – Двоичные решающие диаграммы (BDD),
 
-
* МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD),
 
-
* Хольцман, Пелед, 1994 – редукция частичных порядков,
 
-
* 1995 – редукция частичных порядков в SPIN.
 
-
* Кларк, 1992 – абстракция для уменьшения числа состояний модели,
 
-
* Эльсаиди, 1994 – семантическая минимизация,
 
-
* Пелед, 1996, Бир, 1998 – верификация модели «на лету»,
 
-
* Равви, 2000 – анализ достижимости с учётом спецификации,
 
-
* Эмерсон, Прасад, 1994 -- симметрия
 
-
'''Рост мощности''' model checking:
 
-
* 1992 год – 1020 состояний,
 
-
* 1994 год – 10120 состояний,
 
-
* 1998 год(?) – 10394 состояний
 
'' Лекция 2, Слайды 3-4 ''
'' Лекция 2, Слайды 3-4 ''
-
====Примеры классов свойств:====
+
<u>Примеры классов свойств:</u>
* Стандартные
* Стандартные
-
** Отсутствие ошибок времени выполнения (RTE),
 
-
** Отсутствие удушения (starvation),
 
-
** Не срабатывают ассерты(assertions).
 
** [http://en.wikipedia.org/wiki/Deadlock deadlocks] ([http://ru.wikipedia.org/wiki/%D0%92%D0%B7%D0%B0%D0%B8%D0%BC%D0%BD%D0%B0%D1%8F_%D0%B1%D0%BB%D0%BE%D0%BA%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0 взаимная блокировка])
** [http://en.wikipedia.org/wiki/Deadlock deadlocks] ([http://ru.wikipedia.org/wiki/%D0%92%D0%B7%D0%B0%D0%B8%D0%BC%D0%BD%D0%B0%D1%8F_%D0%B1%D0%BB%D0%BE%D0%BA%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0 взаимная блокировка])
** [http://en.wikipedia.org/wiki/Race_condition Race condition] ([http://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%81%D1%82%D0%BE%D1%8F%D0%BD%D0%B8%D0%B5_%D0%B3%D0%BE%D0%BD%D0%BA%D0%B8 состояние гонки])
** [http://en.wikipedia.org/wiki/Race_condition Race condition] ([http://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%81%D1%82%D0%BE%D1%8F%D0%BD%D0%B8%D0%B5_%D0%B3%D0%BE%D0%BD%D0%BA%D0%B8 состояние гонки])
Строка 912: Строка 672:
** корректная завершаемость
** корректная завершаемость
** причинно-следственный и темпоральный порядок состояний системы
** причинно-следственный и темпоральный порядок состояний системы
-
** Инварианты системы,
 
-
** Индикаторы прогресса,
 
- 
-
====Схема верификации на модели====
 
-
[[Изображение:Verif1.png|400px|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
+
''Схема верификации на модели: Лекция 2, слайд 3''
=== Верификация при помощи Spin. Задание свойств состояний. ===
=== Верификация при помощи Spin. Задание свойств состояний. ===
Строка 1115: Строка 871:
** присваивание
** присваивание
** печать
** печать
-
** проверка свойства безопасности (assert)
+
** проверка свойства безопасности
** отправка сообщения
** отправка сообщения
** прием сообщения
** прием сообщения

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

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

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