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

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

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

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

ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 55 килобайт. Страницы, размер которых приближается к 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 (g \models n) }{\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 )
+
=== Параллелизм. Чередование систем переходов. ===
=== Параллелизм. Чередование систем переходов. ===
Строка 159: Строка 150:
Пусть <math>TS_i = \langle S_i, Act_i, \rightarrow_i, AP_i, I_i, L_i \rangle ~~,~~ i \in \{1,2\}</math>
Пусть <math>TS_i = \langle S_i, Act_i, \rightarrow_i, AP_i, I_i, L_i \rangle ~~,~~ i \in \{1,2\}</math>
-
Тогда чередование этих систем <math>TS_1 ~|||~ TS_2= \langle S_1 \times S_2, Act_1 \cup Act_2, \rightarrow, AP_1 \cup AP_2, I_1 \times I_2, L \rangle</math>, где
+
Тогда чередование этих систем <math>TS_1 ~|||~ TS_2= \langle S_1 \times S_2, Act_1 \cup ACt_2, \rightarrow, AP_1 \cup AP_2, I_1 \times I_2, L \rangle</math>, где
* <math>L(s_1, s_2)= L_1(s_1) \cup L_2(s_2) </math>
* <math>L(s_1, s_2)= L_1(s_1) \cup L_2(s_2) </math>
* оператор <math>\rightarrow</math> определяется как
* оператор <math>\rightarrow</math> определяется как
Строка 166: Строка 157:
=== Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными. ===
=== Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными. ===
-
'' Лекция 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>TS(PG_1)~|||~TS(PG_2)</math> достоверно описывает параллельную композицию <math>PG_1</math> и <math>PG_2</math>
 
-
* в случае с разделяемыми переменными это не так (см. лекцию 4, слайд 26).
 
- 
-
Пусть
 
-
:<math>PG_i = \langle Loc_i, Act_i, Effect_i, \rightarrow_i, Loc_{0,i}, g_{0,i} \rangle,~i \in \{1, 2\}.</math>
 
-
Граф <math>PG_1~|||~PG_2</math> над <math>V_1 \cup V_2</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>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>Effect(\alpha,~\eta) = Effect_i(\alpha,~\eta),</math> если <math>\alpha \in Act_i.</math>
 
- 
-
''Пример: лекция 4, слайд 28.'' В указанном примере <math>TS(PG_1)~|||~TS(PG_2) \neq TS(PG_1~|||~PG_2)</math>
 
- 
=== Параллелизм. Синхронный параллелизм. Рандеву. ===
=== Параллелизм. Синхронный параллелизм. Рандеву. ===
* распределённые программы выполняются параллельно
* распределённые программы выполняются параллельно
Строка 188: Строка 163:
<u>Передача сообщений в распределённых программах:</u>
<u>Передача сообщений в распределённых программах:</u>
* cинхронная передача сообщений (рандеву)
* cинхронная передача сообщений (рандеву)
-
* асинхронная передача сообщений (каналы)
+
* асинхронная передача сообщений (кналы)
-
<u>Синхронный обмен сообщениями:</u>
+
<u>Синхронный обмен сообщенийями:</u>
* Процессы вместе выполняют синхронизированные действия
* Процессы вместе выполняют синхронизированные действия
* Взаимодействие процессов - одновременно
* Взаимодействие процессов - одновременно
Строка 196: Строка 171:
'''Рандеву'''
'''Рандеву'''
* <math>TS_i = \langle S_i, Act_i, \overset{a}{\rightarrow}_i ,I_i, AP_i, L_i \rangle ~~~ i=\{1,2\}</math>
* <math>TS_i = \langle S_i, Act_i, \overset{a}{\rightarrow}_i ,I_i, AP_i, L_i \rangle ~~~ i=\{1,2\}</math>
-
* <math>H \subseteq Act_1 \cap Act_2</math> -- набор синхронизированных действий.
+
* <math>H \subseteq Act_1 \cap Act_2</math>
-
** действия из H должны быть синхронизированны
+
-
** действия не из H независимы и могут чередоваться
+
Тогда <math>TS_1 ||_H TS_2= \langle S_1 \times S_2, Act_1 \cup Act_2, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle</math>, где
Тогда <math>TS_1 ||_H TS_2= \langle S_1 \times S_2, Act_1 \cup Act_2, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle</math>, где
Строка 216: Строка 189:
Тогда <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>
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. ===
- 
-
''Лекция 4. Слайды 36-39, 43-46 ''
 
- 
-
* <math>c \in Chan</math> -- Процессы взаимодействуют с помощью '''каналов''', представляющих собой FIFO буфера
 
-
* <math>dom(c)</math> -- Каналы типизированы по передаваемым сообщениям
 
-
* <math>cap(c)</math> -- ёмкость канала. если <math>cap(c) = 0</math>, то взаимодействие сводится к рандеву
 
-
* действия по обмену сообщениями:
 
-
** <math>c!v</math> -- запись <math>v</math> в конец канала <math>c</math>. Выполняется только если буфер не полон (<math> < cap(c)</math>)
 
-
** <math>c?x</math> -- чтение в <math>x</math> из начала канала <math>c</math>. Выполняется только если буфер не пуст (<math> > cap(c)</math>)
 
-
** формально <math>Comm = \{c!v, c?x ~ | ~ c \in Chan, v \in dom(c), x \in V_p, dom(c) \subseteq dom(x)\}</math>
 
- 
-
<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>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>
 
- 
-
При асинхронной передаче сообщений (при <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: Строка 200:
Рассмотрим трассы 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> такое, что <math>\forall n,k \in \mathbb{N}, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k) </math> - некоторая неубывающая функция [?]
-
#* <math>\alpha</math> - неубывающая функция: <math>\forall n,k \in \mathbb{N}, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k) </math>
+
# <math>\forall n \in \mathbb{N}, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(\alpha(n), p)</math>
-
#* <math>\forall n \in \mathbb{N}, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(\alpha(n), p)</math>
+
Пример абстракции трассы: Лекция 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: Строка 232:
* Метки на состояниях модели должны состоять только из предикатов модели: <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: Строка 252:
=== Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. ===
=== Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. ===
-
''Лекция 5, слайды 2-14.''
 
-
'''Требования правильности''' — утверждения о возможных и невозможных вариантах выполнения программы.
+
'''Требования правильности''' -- утверждения о возможных и невозможных вариантах выполнения программы.
<u>Двойственность</u> :
<u>Двойственность</u> :
-
* если какое-то утверждение невозможно, то обратное — неизбежно
+
* если какое-то утверждение невозможно, то обратное -- неизбежно
-
* если какое-то утверждение неизбежно, то обратное — невозможно
+
* если какое-то утверждение неизбежно, то обратное -- невозможно
* при помощи логики от одного можно переходить к другому при помощи отрицания
* при помощи логики от одного можно переходить к другому при помощи отрицания
Строка 481: Строка 265:
* в 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: Строка 286:
** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.
** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.
-
'''ps'''. автор терминов – Лесли Лампорт; см. ''Лекция 5, слайд 4''.
 
=== Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. ===
=== Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. ===
-
''Лекция 6, слайды 8 - 15''
+
Лекция 6, слайды 8 - 15
'''Конечный автомат'''
'''Конечный автомат'''
Строка 513: Строка 296:
* <math>s_0 \in S </math> -- множество начальных состояний
* <math>s_0 \in S </math> -- множество начальных состояний
* L -- конечное множество меток
* L -- конечное множество меток
-
* <math>F \subseteq S </math> -- множество терминальных состояний
+
* <math>F \subset S </math> -- множество терминальных состояний
-
* <math>T \subseteq S \times L \times S</math> -- отношение перехода на состояниях
+
* <math>T \subset S \times L \times S</math> -- отношение перехода на состояниях
'''
'''
Детерминизм и недетерминизм'''
Детерминизм и недетерминизм'''
Конечный автомат называется '''детерминированным''', если по метке и исходному состоянию можно однозначно определить целевое состояние:
Конечный автомат называется '''детерминированным''', если по метке и исходному состоянию можно однозначно определить целевое состояние:
-
<math>\forall s \in S, \forall l \in L: ((s, l, s_1) \in A.T \and (s, L, s_2) \in A.T ~ \Rightarrow ~ s_1 = s_2) </math>
+
<math>\forall s \in S, \forall l \in L: ((s, l, s_1) \in A.T \and (s, L, s_2) \in A.T => s_1 = s_2) </math>
В противном случае автомат называется '''недетерминированным'''.
В противном случае автомат называется '''недетерминированным'''.
'''Проходом a конечного автомата''' <math>\langle S,s_0,L,F,T \rangle</math> называется такое ''упорядоченное'' и, возможно, бесконечное множеств переходов из T:
'''Проходом a конечного автомата''' <math>\langle S,s_0,L,F,T \rangle</math> называется такое ''упорядоченное'' и, возможно, бесконечное множеств переходов из T:
-
<math>a=\langle (s_0, l_0, s_1),(s_1, l_1, s_2), ... \rangle ~~ \forall i, i \geqslant 0;~ (s_i, l_{i}, s_{i+1}) \in T</math>
+
<math>a=\langle (s_0, l_0, s_1),(s_1, l_1, s_2), ... \rangle \forall i, i >= 0 (s_i, l_{i}, s_{i+1}) \in T</math>
Строка 533: Строка 316:
=== Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи. ===
=== Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи. ===
-
''Лекция 6, слайды 19-20''
+
''Лекция 6, слайды 16''
-
Для любого бесконечного прохода <math>\sigma</math> конечного автомата А можно выделить два последовательных отрезка проходов:
+
'''Допускающий проход по Бюхи'''(w-допускание) конечного автомата A называется такой ''бесконечный проход'' a, что <math>\exists i \geqslant 0, (s_{i-1}, l_{i-1}, s_i) \in a ~~ : ~~ (s_{i} \in A.F) \and (s_{i} \in a^w) </math>
-
* <math>\sigma^{+}</math> -- конечный отрезок прохода <math>\sigma</math>, включающий в себя множество состояний, встречающихся конечное число раз
+
-
* <math>\sigma^\omega</math> -- бесконечный хвост прохода <math>\sigma</math>, включающий в себя множество состояний, встречающихся бесконечное число раз
+
-
'''Допускающий проход по Бюхи''' (<math>\omega</math>-допускание) конечного автомата A называется такой ''бесконечный проход'', в котором по крайней мере одно терминальное состояние встречается бесконечное число раз: <math>\exists i \geqslant 0, (s_{i-1}, l_{i-1}, s_i) \in \sigma ~~ : ~~ (s_{i} \in A.F) \and (s_{i} \in \sigma^\omega) </math>
+
т.е. по крайней мере одно терминальное состояние встречается бесконечно часто.
-
<u>Расширение автоматов Бюхи.</u>
+
'''Расширение автоматов Бюхи.'''
-
* добавляем алфавит автомата меткой <math>\varepsilon</math>
+
-
* все конечные проходы расширяем до бесконечности меткой <math>\varepsilon</math>
+
-
Примечание. При помощи автоматов Бюхи удобно проверять свойства живучести.
+
Конечные проходы дополняются бесконечным переходом по пустому действию.
 +
При помощи автоматов Бюхи удобно проверять свойства живучести.
=== Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until. ===
=== Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until. ===
Строка 554: Строка 334:
* может использоваться для описания свойств как живучести, так и безопасности
* может использоваться для описания свойств как живучести, так и безопасности
* описывает свойства, которым должны удовлетворять линейные последовательности наблюдаемых состояний - трассы
* описывает свойства, которым должны удовлетворять линейные последовательности наблюдаемых состояний - трассы
-
* семантика LTL определена на бесконечных автоматах Бюхи. Для конечных проходов необходимо использовать расширение автомата.
+
* семантика LTL определена на бесконечных автоматах Бюхи. Для конечных проходов необходимо использовать расширение автоматаю
<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 s_i \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. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. ===
Строка 607: Строка 384:
| <math>p \rightarrow \diamond q</math> || если p, то рано или поздно q || ''отклик'' ||
| <math>p \rightarrow \diamond q</math> || если p, то рано или поздно q || ''отклик'' ||
|-
|-
-
| <math>p \rightarrow q U r</math>
+
| <math>p \rightarrow q U r</math> || если p то затем q и рано или поздно r || ''приоритет'' ||
-
| если p то затем постоянно q до тех пор,
+
-
пока рано или поздно не наступит r
+
-
| ''приоритет''
+
|-
|-
| <math>\Box\diamond p</math> || всегда рано или позндно будет p || ''цикличность (прогресс)'' ||
| <math>\Box\diamond p</math> || всегда рано или позндно будет p || ''цикличность (прогресс)'' ||
Строка 655: Строка 429:
=== Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию. ===
=== Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию. ===
-
''Лекция 7, слайды 22-25 ''
+
'''Оператор X нужно использовать аккуратно:'''
-
 
+
-
'''Оператор <math>X</math> нужно использовать аккуратно:'''
+
* с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния,
* с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния,
-
* в распределённых системах значение оператора <math>X</math> неочевидно,
+
* в распределённых системах значение оператора X неочевидно,
* поскольку алгоритм планирования процессов неизвестен, не стоит формулировать спецификацию в предположении о том,
* поскольку алгоритм планирования процессов неизвестен, не стоит формулировать спецификацию в предположении о том,
какое состояние будет следующим,
какое состояние будет следующим,
Строка 673: Строка 445:
** E(f) называется расширением прореживания f.
** E(f) называется расширением прореживания f.
-
* Свойство f, инвариантное к прореживанию, либо истинно для всех трасс из <math>E(\psi)</math>, либо ни для одной из них:
+
* Свойство <math>\psi</math>, инвариантное к прореживанию, либо истинно для всех трасс из <math>E(\psi)</math>, либо ни для одной из них:
-
** <math>\psi \models f ~ \Rightarrow ~ \forall v \in E(\psi), v \models f </math>
+
** <math>\psi \models f => \forall v \in E(\psi), v \models f </math>
-
* истинность такого свойства не зависит от длины трассы, а только от порядка, в котором пропозициональные формулы меняют свои значения;
+
* истинность такого свойства не зависит от длины трассы, а только от порядка, в котором пропозициональные формулы
-
* Теорема: все формулы LTL без оператора <math>X</math> инвариантны к прореживанию.
+
меняют свои значения;
-
* в рамках LTL без <math>X</math> можно описать все свойства, инвариантные к прореживанию
+
* Теорема: все формулы LTL без оператора X инвариантны к
 +
прореживанию.
=== Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin. ===
=== Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin. ===
-
'' Лекция 7, слайды 26-40 ''
 
- 
'''Связь LTL с автоматами Бюхи'''
'''Связь LTL с автоматами Бюхи'''
* Удобно проверять допустимость трасс для некоторого автомата Бюхи;
* Удобно проверять допустимость трасс для некоторого автомата Бюхи;
Строка 694: Строка 465:
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. ===
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. ===
-
При помощи конструкции never можно описать любой &omega;-регулярный автомат над словами
+
При помощи конструкции never можно описать любой w-регулярный автомат над словами
-
 
+
'''Выразительная мощность LTL'''
'''Выразительная мощность LTL'''
Строка 707: Строка 477:
(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: Строка 483:
'''Логика С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: Строка 516:
<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: Строка 537:
=== Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. ===
=== Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. ===
-
«Тестирование может показать присутствие ошибок, но не может показать их отсутствия» © Дейкстра.
 
- 
-
Обоснование полноты тестового покрытия:
 
-
* метод «чёрного ящика» (ЧЯ) — полное покрытие входных данных,
 
-
* метод «прозрачного ящика» (ПЯ) — полное покрытие кода программы.
 
-
Плюсы применения тестирования:
 
-
* проверяется та программа, которая будет использоваться,
 
-
* не требуется знание/использование дополнительных инструментальных средств,
 
-
* удобная локализация ошибки.
 
-
Минусы применения тестирования:
 
-
* не всегда есть условия для тестирования системы,
 
-
* проблема с воспроизводимостью тестов (частичное решение — имитационное моделирование).
 
- 
-
====Проблема полноты тестового покрытия====
 
-
* Чёрный ящик:
 
-
** для последовательных программ сложно перебрать все входные данные,
 
-
** для параллельных программ — очень сложно,
 
-
** для динамических структур данных, взаимодействия с окружением — невозможно.
 
-
* Прозрачный ящик:
 
-
** большой размер покрытия,
 
-
** часто невозможно построить 100% покрытие,
 
-
** полное покрытие не гарантирует отсутствия ошибок.
 
-
Итоги:
 
-
* Полный перебор входных данных — невозможен.
 
-
* Полнота покрытия кода не гарантирует правильности.
 
-
* Ошибка — ошибочное вычисление системы.
 
-
* Полнота в терминах возможных вычислений — хороший критерий.
 
=== Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. ===
=== Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. ===
Строка 873: Строка 617:
'' Лекция 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: Строка 628:
** корректная завершаемость
** корректная завершаемость
** причинно-следственный и темпоральный порядок состояний системы
** причинно-следственный и темпоральный порядок состояний системы
-
** Инварианты системы,
 
-
** Индикаторы прогресса,
 
-
====Схема верификации на модели====
+
''Схема верификации на модели: Лекция 2, слайд 3''
-
 
+
-
[[Изображение:Verif1.png|400px|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
+
=== Верификация при помощи Spin. Задание свойств состояний. ===
=== Верификация при помощи Spin. Задание свойств состояний. ===
Строка 942: Строка 654:
Существует два основных варианта справедливости:
Существует два основных варианта справедливости:
* слабая справедливость:
* слабая справедливость:
-
** если оператор выполним бесконечно '''долго''', то он в конце концов будет выполнен
+
** если оператор выполним бесконечно долго, то он в конце концов будет выполнен
* сильная справедливость:
* сильная справедливость:
-
** если оператор выполним бесконечно '''часто''', то он в конце концов будет выполнен.
+
** если оператор выполним бесконечно часто,то он в конце концов будет выполнен.
Справедливость применима как к внутреннему, так и к
Справедливость применима как к внутреннему, так и к
внешнему недетерминизму.
внешнему недетерминизму.
Строка 951: Строка 663:
=== Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты. ===
=== Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты. ===
'''never claims (утверждения о невозможности):'''
'''never claims (утверждения о невозможности):'''
-
* выполняются синхронно с моделью
+
* выполняются синхронно с моделью,
-
* если достигнут конец, то – ошибка
+
* если достигнут конец, то – ошибка,
-
* состоят из выражений и конструкция задания потока управления
+
* состоят из выражений и конструкция задания
-
* фактически, описывают распознающий автомат.
+
потока управления
 +
* фактически, описывают распознающий
 +
автомат.
'''Конструкция never'''
'''Конструкция never'''
Строка 983: Строка 697:
=== Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin. ===
=== Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin. ===
-
* Свойство ''выполняется'' на модели, если оно выполняется на всех трассах.
 
-
* Свойство ''нарушается'' на модели, если нарушается хотя бы на одной из трасс.
 
-
* '''Принцип верификации нарушения свойств''' - проще проверять нарушение свойства, чем выполнение свойства.
 
-
** Достаточно найти один контрпример
 
-
* Нарушение свойства описывается при помощи конструкции never – автомата, распознающего неправильное поведение
 
-
** Автоматы Бюхи
 
-
* Свойства на последовательностях состояний удобно описывать при помощи темпоральной логики
 
-
** Логика LTL
 
- 
-
* <u>Связь LTL с автоматами Бюхи</u>
 
-
** При помощи автомата Бюхи удобно проверять допустимость трасс.
 
-
** При помощи темпоральных формул удобно описывать свойства правильности.
 
-
** Для всякой LTL-формулы f существует автомат Бюхи, который допускает те и только те прогоны, которым соответствуют трассы, на которых выполнима f
 
-
* <u>Переход от LTL к автоматам</u>
 
-
** f выполняется на всех вычислениях <=>
 
-
** !f не выполняется ни на одном вычислении <=>
 
-
** автомат never {!f} не допускает ни одного прогона, полученного в результате синхронного выполнения с системой
 
- 
-
'''Использование LTL в Spin'''
 
-
* SPIN как раз и занимается тем, что преобразует LTL-формулы в автомат Бюхи, описываемый конструкцией never.
 
-
* Если во время верификации нашлась трасса, принадлежащая языку автомата Бюхи (т.е, конструкция never выполнилась, и мы дошли до её конца), SPIN выдаст '''контрпример''', содержащий эту трассу.
 
== Система Spin и язык Promela ==
== Система Spin и язык Promela ==
=== Система Spin. Процесс моделирования и верификации при помощи системы Spin. Конечность моделей на Promela. Асинхронное выполнение моделей. Недетерминированный поток управления. Понятие выполнимости оператора. ===
=== Система Spin. Процесс моделирования и верификации при помощи системы Spin. Конечность моделей на Promela. Асинхронное выполнение моделей. Недетерминированный поток управления. Понятие выполнимости оператора. ===
- 
- 
-
'''Верификация программы на модели'''
 
-
* Мы хотим задавать, как система устроена и как она должна быть устроена
 
-
* Таким образом, нужно две нотации:
 
-
** чтобы описать поведение (устройство системы)
 
-
** чтобы описать требования (свойства правильности)
 
-
* Верификатор:
 
-
** проверяет, что устройство системы удовлетворяет свойствам правильности
 
-
** выбранная нотация гарантирует разрешимость проверки правильности любого свойства любой модели
 
-
* Все держится на трех китах
 
-
** ''SPIN'' – Simple Promela Interpreter
 
-
*** верификация
 
-
*** моделирование
 
-
** ''Promela'' – Process Meta Language - описание поведения модели
 
-
*** недетерминированный язык с охраняемыми командами
 
-
*** задача языка – разрешить описывать такие модели, которые могут быть верифицированы
 
-
** ''LTL'' – Linear Temporal Logic - описание свойств
 
- 
-
'''Конечность моделей на Promela'''
 
-
* У моделей – конечное число состояний (потенциально бесконечные элементы моделей в Promela ограничены)
 
-
** гарантирует разрешимость верификации
 
-
* Почему число состояний конечно?
 
-
** Число активных процессов конечно (от 0 до 255)
 
-
** У каждого процесса – ограниченное количество операторов
 
-
** Диапазоны типов данных ограничены
 
-
** Размер всех каналов сообщений ограничен
 
- 
-
'''Асинхронное выполнение моделей'''
 
-
* нет глобальных часов
 
-
* по умолчанию синхронизация отсутствует
 
- 
-
'''Недетерминированный поток управления'''
 
-
* абстракция от деталей реализации
 
-
* Два уровня недетерминизма
 
-
** внешний (выбор процесса)
 
-
*** процессы выполняются параллельно и асинхронно (между двумя последовательными операторами одного процесса может быть сколь угодно длинная пауза)
 
-
*** произвольная диспетчеризация процессов
 
-
*** выполнение операторов разных процессов происходит в произвольном порядке (основные операторы выполняются атомарно)
 
-
* внутренний (выбор действия в процессе).
 
-
** в теле одного процесса также допускается недетерминированное ветвление
 
- 
-
'''Понятие выполнимости оператора'''
 
-
* с любым оператором связаны понятия предусловия и эффекта
 
-
* оператор выполняется (производя эффект), только если предусловие истинно, в противном случае он заблокирован
 
-
** Пример 1: ''q?m''; если канал ''q'' не пуст, читаем из него сообщение, иначе ждём
 
-
** Пример 2: (''x > y) -> y++''; процесс будет заблокирован до тех пор, пока ''x'' не станет больше ''y''. После этого ''y'' увеличится на единицу.
 
- 
=== Язык Promela. Основные компоненты модели на языке Promela. Процессы, локальные и глобальные объекты данных, каналы сообщений. ===
=== Язык Promela. Основные компоненты модели на языке Promela. Процессы, локальные и глобальные объекты данных, каналы сообщений. ===
- 
-
'''Устройство модели'''. Существует три типа объектов:
 
-
* процессы
 
-
* глобальные и локальные объекты данных
 
-
* каналы сообщений
 
- 
-
'''Процессы'''
 
-
* Поведение процесса задаётся в объявлении типа процесса (proctype)
 
-
* Экземпляр процесса – инстанциация proctype
 
-
* Два вида инстанцирования процессов:
 
-
** В начальном состоянии системы - ''префикс active''
 
-
** В произвольном достижимом состоянии системы - ''оператор run''
 
- 
-
'''Локальные и глобальные объекты данных'''. Два уровня видимости:
 
-
* глобальный (данные видны всем активным процессам)
 
-
* локальный (данные видны только одному процессу)
 
-
** есть особенность: локальная переменная, объявленная в теле процесса, видна во всем процессе (нет понятия ''область видимости переменной'' внутри процесса)
 
- 
-
'''Каналы сообщений'''
 
-
* каналы бывают двух типов:
 
-
** буферизованные (асинхронные)
 
-
** небуферизованные (синхронные, рандеву)
 
-
* пример объявления канала: chan x = [10] of {int, short, bit};
 
-
** ''10'' - максимальное число сообщений в канале. 0 определяет канал рандеву.
 
-
** ''{int, short, bit}'' - структура пересылаемых сообщений
 
- 
=== Язык Promela. Механизмы взаимодействия процессов в языке Promela. Глобальные переменные, каналы сообщений, явная синхронизация. ===
=== Язык Promela. Механизмы взаимодействия процессов в языке Promela. Глобальные переменные, каналы сообщений, явная синхронизация. ===
- 
-
''см. предыдущий вопрос''
 
- 
-
'''Явная синхронизация:'''
 
- 
-
active proctype A() provided (toggle == true){
 
-
L: cnt++;
 
-
printf("A: cnt=%d\n", cnt);
 
-
toggle = false;
 
-
goto L
 
-
}
 
- 
- 
-
active proctype B() provided (toggle == false){
 
-
L: cnt--;
 
-
printf("B: cnt=%d\n", cnt);
 
-
toggle = true;
 
-
goto L
 
-
}
 
- 
-
Процесс выполняется, только если значение provided clause равно true.
 
-
По умолчанию значение равно true
 
- 
=== Язык Promela. Основные операторы языка Promela. Операторы-выражения, присваивания. ===
=== Язык Promela. Основные операторы языка Promela. Операторы-выражения, присваивания. ===
-
'''Основные операторы языка Promela'''
 
-
* задают элементарные преобразования состояний,
 
-
* размечают дуги в системе переходов соответствующего процесса,
 
-
* их немного – всего 6 типов:
 
-
** выражение
 
-
** присваивание
 
-
** печать
 
-
** проверка свойства безопасности (assert)
 
-
** отправка сообщения
 
-
** прием сообщения
 
-
* оператор может быть:
 
-
** выполнимым: ''может'' быть выполнен,
 
-
** заблокированным: (пока что) ''не может'' быть выполнен,
 
-
** выполнимость может зависеть от глобального состояния.
 
- 
-
'''Оператор-выражение'''
 
-
* выполним только если выражение не равно 0 (истинно):
 
-
** 2 < 3 – выполним всегда,
 
-
** x < 27 – выполним только если значение x < 27,
 
-
** 3 + х – выполним только если x != -3.
 
- 
-
'''Оператор-присваивание'''
 
-
* всегда безусловно выполним, меняет значение только одной переменной, расположенной слева от “=”.
 
- 
=== Язык Promela. Основные операторы языка Promela. Отладочная печать, операторы skip, true, run, assert. ===
=== Язык Promela. Основные операторы языка Promela. Отладочная печать, операторы skip, true, run, assert. ===
- 
-
'''Основные операторы языка Promela'''
 
-
* присваивание: x++, x--, x = x + 1, x = run P();
 
-
* выражение: (x), (1), run P(), skip, true, else, timeout;
 
-
* печать: printf(“x = %d\n”, x);
 
-
* ассерт: assert(1+1 == 2), assert(false);
 
-
* отправка сообщения: q!m;
 
-
* приём сообщения: q?m;
 
- 
-
'''Отладочная печать'''
 
-
* оператор печати ''printf'', всегда безусловно выполним, на состояние не влияет
 
- 
-
'''Псевдо-операторы'''
 
-
* skip: всегда выполним, без эффекта, эквивалент выражения (1),
 
-
* true: всегда выполним, без эффекта, эквивалент выражения (1),
 
-
* run: 0 если при создании процесса превышен лимит, pid в противном случае.
 
- 
-
'''Оператор assert'''
 
-
* всегда выполнимо, не влияет на состояние системы,
 
-
* Spin сообщает об ошибке, если значение выражения равно 0 (false),
 
-
* используется для проверки свойств безопасности.
 
- 
=== Язык Promela. Чередование (интерливинг) операторов. Внешний и внутренний недетерминизм. Управление выполнимостью операторов. ===
=== Язык Promela. Чередование (интерливинг) операторов. Внешний и внутренний недетерминизм. Управление выполнимостью операторов. ===
-
'''Чередование (интерливинг) операторов'''
 
-
* процессы выполняются параллельно и асинхронно, ''между двумя последовательными операторами одного процесса может быть сколь угодно длинная пауза'',
 
-
* произвольная диспетчеризация процессов,
 
-
* выполнение операторов разных процессов происходит в произвольном порядке, ''основные операторы выполняются атомарно'',
 
-
* в теле одного процесса также допускается недетерминированное ветвление
 
- 
-
'''Внешний и внутренний недетерминизм'''
 
-
* два уровня недетерминизма:
 
-
** внешний (выбор процесса),
 
-
** внутренний (выбор действия в процессе).
 
- 
-
'''Управление выполнимостью операторов'''
 
-
Основной инструмент управления выполнимостью операторов в Promela – выражения (expressions).
 
-
(a + b) -> c++;
 
-
Так же существуют управляющие конструкции if..fi и do..od
 
- 
=== Язык Promela. Задание потока управления последовательного процесса. Управляющие конструкции if, do. Организация внутреннего недетерминизма. ===
=== Язык Promela. Задание потока управления последовательного процесса. Управляющие конструкции if, do. Организация внутреннего недетерминизма. ===
-
'''Задание потока управления последовательного процесса'''
 
-
5 способов задать поток управления:
 
-
* последовательная композиция(“;”), метки, goto,
 
-
* структуризация (макросы и inline),
 
-
* атомарные последовательности (atomic, d_step),
 
-
* недетерминированный выбор и итерации (if..fi, do..od),
 
-
* escape-последовательности ({...}unless{...}).
 
- 
-
'''Специальные выражения и переменные'''
 
-
* else – true, если ни один оператор процесса не выполним,
 
-
* timeout – true, если ни один оператор модели не выполним,
 
-
* _ – переменная, доступная только по записи, значение не сохраняет,
 
-
* _pid – минимальный доступный pid,
 
-
* _nr_pr – число активных процессов.
 
- 
=== Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений. ===
=== Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений. ===
-
'''Каналы сообщений'''
 
-
* сообщения передаются через каналы (очереди/буфера ограниченного объёма)
 
-
* каналы бывают двух типов:
 
-
** буферизованные (асинхронные),
 
-
** небуферизованные (синхронные, рандеву);
 
- 
-
chan x = [10] of {int, short, bit};
 
- 
-
'''Операторы отправки и приема сообщений'''
 
-
Отправка: ch!expr1,...exprn
 
-
* значения expri соответствуют типам в объявлении канала;
 
-
* выполнимо, если заданный канал не полон;
 
-
Приём: ch?const1 или var1,...constn или varn
 
-
* значения vari становятся равны соотв. значениям полей сообщения;
 
-
* значения consti ограничивают допустимые значения полей;
 
-
* выполнимо, если заданный канал не пуст и первое сообщение в канале соответствует всем константным значениям в операторе приёма сообщения;
 
- 
-
'''Объявление mtype'''
 
-
* способ определить символьные константы (до 255)
 
- 
-
Объявление mtype:
 
-
mtype = {foo, bar};
 
-
mtype = {ack, msg, err, interrupt};
 
- 
-
Объявление переменных типа mtype:
 
-
mtype a;
 
-
mtype b = foo;
 
- 
-
'''Cинхронная и асинхронная передача сообщений'''
 
-
* Асинхронная передача
 
-
** асинхронные сообщения буферизуются для последующего приёма, пока канал не полон,
 
-
** отправитель блокируется, когда канал полон,
 
-
** получатель блокируется, когда канал пуст.
 
-
* Синхронная передача
 
-
** ёмкость канала равна 0 - chan ch = [0] of {mtype};
 
-
** передача сообщений методом “рандеву”,
 
-
** не хранит сообщения,
 
-
** отправитель блокируется в ожидании получателя, и наоборот,
 
-
** отправка и приём выполняются атомарно.
 
- 
=== Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений. ===
=== Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений. ===
-
'''Другие операции с каналами'''
 
-
* len(q) – возвращает число сообщений в канале,
 
-
* empty(q) – возвращает true, если q пуст,
 
-
* full(q) – возвращает true, если q полон,
 
-
* nempty(q) – вместо !empty(q) (в целях оптимизации),
 
-
* nfull(q) – вместо !full(q) (в целях оптимизации).
 
-
* q?[n,m,p]
 
-
** булевое выражение без побочных эффектов,
 
-
** равно true только когда q?n,m,p выполнимо, однако не влияет на значения n,m,p и не меняет собержимое канала q;
 
-
* q?<n,m,p>
 
-
** выполнимо тогда же, когда и q?n,m,p; влияет на значения n,m,p так же, как q?n,m,p, однако не меняет содержимое q;
 
-
* q?n(m,p)
 
-
** вариант записи оператора приёма сообщения (т.е. q?n,m,p),
 
-
** может использоваться для отделения переменной от констант
 
-
* q!!n,m,p – аналогично q!n,m,p, но сообщение n,m,p помещается в канал q сразу за первым сообщением, меньшим n,m,p;
 
-
* q??n,m,p – аналогично q?n,m,p, но из канала может быть выбрано любое сообщение (не обязательно первое).
 
- 
-
''Имя канала может быть локальным или глобальным, но канал сам по себе – всегда глобальный объект''
 
- 
=== Язык Promela. Основные типы данных. Область видимости данных. ===
=== Язык Promela. Основные типы данных. Область видимости данных. ===
- 
-
{|
 
-
|+ Основные типы данных
 
-
! Тип !! Диапазон !! Пример объявления !!
 
-
|-
 
-
| bit || 0..1 || bit turn = 1; ||
 
-
|-
 
-
|bool || false..true || bool flag = true; ||
 
-
|-
 
-
|byte || 0..255 || byte cnt; ||
 
-
|-
 
-
|chan || 1..255 || chan q; ||
 
-
|-
 
-
|mtype || 1..255 || mtype msg; ||
 
-
|-
 
-
|pid || 1..255 || pid p; ||
 
-
|-
 
-
|short || -2<sup>15</sup>..2<sup>15</sup>-1 || short s = 100; ||
 
-
|-
 
-
|int || -2<sup>31</sup>..2<sup>31</sup>-1 || int x = 1; ||
 
-
|-
 
-
|unsigned || 0..2<sup>n</sup>-1 || unsigned u : 3; // 3 бита [?] ||
 
-
|}
 
- 
-
* по умолчанию все объекты (и локальные и глобальные) инициализируются нулём;
 
-
* все переменные должны быть объявлены до первого использования;
 
-
* переменная может быть объявлена где угодно.
 
- 
-
'Одномерные массивы'
 
- 
-
byte a[27];
 
-
bit flags[4] = 1;
 
- 
-
* все элементы массива инициализируются одним значением,
 
-
* индексы нумеруются с 0;
 
- 
-
'Пользовательские типы данных'
 
- 
-
typedef record {
 
-
short f1;
 
-
byte f2 = 4;
 
-
}
 
-
record rr;
 
-
rr.f1 = 5;
 
- 
-
'''Только два уровня видимости'''
 
-
* глобальный (данные видны всем активным процессам),
 
-
* локальный (данные видны только одному процессу)
 
-
** подобластей (напр. для блоков) нет,
 
-
** локальная переменная видна везде в теле процесса;
 
- 
-
{{Курс ВПнМ}}
 

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


Отменить | Справка по редактированию (в новом окне)

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

Получено с 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
Личные инструменты
Разделы