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

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

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

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

ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 42 килобайт. Страницы, размер которых приближается к 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>, если существует вычисление программы, в котором оно присутствует
 
=== Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.===
=== Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.===
-
'' Лекция 2, Слайды 39-50 ''
+
'''Размеченная система переходов (LTS)'''
-
 
+
-
====Размеченная система переходов (LTS)====
+
<math>TS = \langle S, Act, \overset{a}{\rightarrow} ,s_0, AP, L \rangle </math>
<math>TS = \langle S, Act, \overset{a}{\rightarrow} ,s_0, AP, L \rangle </math>
Строка 32: Строка 27:
* 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> - функция разметки
Строка 41: Строка 36:
<math>\langle s, a, s' \rangle \in \overset{a}{\rightarrow} \equiv s \overset{a}{\rightarrow} s' </math>
<math>\langle s, a, s' \rangle \in \overset{a}{\rightarrow} \equiv s \overset{a}{\rightarrow} s' </math>
-
''Пример LTS: Лекция 2, слайды 40-41''
+
Пример LTS: Лекция 2, слайд 40-41
'''Прямые потомки'''
'''Прямые потомки'''
Строка 47: Строка 42:
* <math>Post(s) = \bigcup_{a \in Act} Post(s, a)</math> - все возможные состояния s', которые <u>непосредственно вытекают</u> из s
* <math>Post(s) = \bigcup_{a \in Act} Post(s, a)</math> - все возможные состояния s', которые <u>непосредственно вытекают</u> из s
-
Система <math>TS = \langle S, Act, \overset{a}{\rightarrow} ,I, AP, L \rangle</math> '''детерминирована''':
+
Система <math>TS = <S, Act, \overset{a}{\rightarrow} ,s_0, AP, L></math> '''детерменирована''':
* '''по действиям''' тогда и только тогда, когда
* '''по действиям''' тогда и только тогда, когда
** <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> ( количество одинаково размеченных потомков не больше одного )
-
'''Недетерминизм''' - это фича! Полезен для:
+
'''Недетерменизм''' - это фича! Полезен для:
* моделирования параллельного выполнения в режиме чередования (интерливинга)
* моделирования параллельного выполнения в режиме чередования (интерливинга)
** позволяет не указывать скорость выполнения процессов
** позволяет не указывать скорость выполнения процессов
Строка 64: Строка 59:
** модель может быть построена по неполной информации
** модель может быть построена по неполной информации
-
====Вычисления====
+
'''Вычисления'''
-
# '''Конечный фрагмент вычисления <math>\sigma</math>''' системы переходов TS - это конечная последовательность чередующихся состояний и действий, заканчивающаяся состоянием: <math>\sigma = s_0 a_1 s_1 a_2 s_2 \dots a_n s_n, \forall i \in [0,n) \Rightarrow s_i \overset{a_{i+1}}{\rightarrow} s_{i+1}</math>
+
# '''Конечный фрагмент вычисления <math>\sigma</math>''' системы переходов TS называется конечная последовательность чередующихся состояний и действий <math>\sigma = s_0 a_1 s_1 a_2 s_2 \dots a_n s_n, \forall i \in [0,n] \Rightarrow s_i \overset{a_{i+1}}{\rightarrow} s_{i+1}</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>\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>
-
'''Reach(TS)''' - множество всех достижимых состояний в TS
+
'''Rich(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>
-
====Свойства линейного времени====
+
<u>Свойства линейного времени</u>
-
* Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \subseteq (2^{AP})^\omega</math>
+
* Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \in (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>TS(P) \models \varphi ~~ \equiv ~~ P \models \varphi </math>
=== Моделирование программ. Графы программ. Статическая и операционная семантика. ===
=== Моделирование программ. Графы программ. Статическая и операционная семантика. ===
Строка 90: Строка 86:
** <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>Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math>
* Эффект операторов: <math>Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math>
Строка 100: Строка 95:
<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 : 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: Строка 108:
** находимся в точке программы l
** находимся в точке программы l
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
-
* Состояния <math>\langle l,n \rangle</math> размечаются высказыванием о том, что мы находимся в точке программы <math>~ l</math> и всеми высказываниями, истинными в <math>~ n</math>
+
* Состояния <math><l,n></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><l,n></math> в состояние <math><l^', Effect(a,n)></math> по действию a.
'''Системы переходов графов программ'''
'''Системы переходов графов программ'''
Строка 121: Строка 116:
* <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>l \overset{g:a}{\rightarrow} l \and (g |= n) </math> <math>\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 |= 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> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
+
* Состояния вида <l,n> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
-
** <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 |= g ).</math>
-
'''Пример: Лекция 4, слайд 16'''
+
''Пример: Лекция 4, слайд 16''
-
 
+
-
 
+
-
'''Статическая и операционная семантика'''
+
-
 
+
-
'''Cтатическая семантика''' – набор ограничений, которым должна удовлетворять структура программы;
+
-
'''Операционная семантика''' – понятие состояния программы и изменение состояния в ходе работы программы; то, как по графу строится LTS.
+
-
(См. Л.5, сл. 15, 2010 )
+
-
 
+
-
=== Параллелизм. Чередование систем переходов. ===
+
-
''Лекция 4, слайды 21-24''
+
-
 
+
-
* Действия независимых процессов чередуются.
+
-
* Порядок выполнения процессов не известен.
+
-
 
+
-
'''Чередование:'''
+
-
* эффект от параллельного выполнения независимых действий a и b равен эффекту от их последовательного выполнения в произвольном порядке:
+
-
** <math>Effect(a ~|||~ b,n) = Effect((a;b)+(b;a),n)</math>
+
-
*** ||| -- оператор чередования
+
-
*** ; -- оператор последовательного выполнения
+
-
*** + -- оператор недетерминированного выбора
+
-
 
+
-
''Пример: Лекция 4, слайд 23''
+
-
 
+
-
'''Чередование систем переходов'''
+
-
 
+
-
Пусть <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>L(s_1, s_2)= L_1(s_1) \cup L_2(s_2) </math>
+
-
* оператор <math>\rightarrow</math> определяется как
+
-
** <math>\frac{s_1 \rightarrow_1 s_1^'}{(s_1, s_2) \rightarrow (s_1^', s_2)}</math>
+
-
** <math>\frac{s_2 \rightarrow_2 s_2^'}{(s_1, s_2) \rightarrow (s_1, s_2^')}</math>
+
 +
=== Параллелизм. Чередование систем переходов. ===
=== Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными. ===
=== Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными. ===
-
'' Лекция 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: Строка 136:
<u>Передача сообщений в распределённых программах:</u>
<u>Передача сообщений в распределённых программах:</u>
* cинхронная передача сообщений (рандеву)
* cинхронная передача сообщений (рандеву)
-
* асинхронная передача сообщений (каналы)
+
* асинхронная передача сообщений (кналы)
-
<u>Синхронный обмен сообщениями:</u>
+
<u>Синхронный обмен сообщенийями:</u>
* Процессы вместе выполняют синхронизированные действия
* Процессы вместе выполняют синхронизированные действия
* Взаимодействие процессов - одновременно
* Взаимодействие процессов - одновременно
Строка 196: Строка 144:
'''Рандеву'''
'''Рандеву'''
* <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 = \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>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>\rightarrow</math> определяется как:
** интерливинг для <math>\alpha \not\in H~:~~~ \frac{s_1 \overset{a}{\rightarrow}_1 s_1'}{ \langle s_1, s_2 \rangle \overset{a}{\rightarrow} \langle s_1', s_2 \rangle}</math> и <math>\frac{s_2 \overset{a}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{a}{\rightarrow} \langle s_1, s_2' \rangle}</math>
** интерливинг для <math>\alpha \not\in H~:~~~ \frac{s_1 \overset{a}{\rightarrow}_1 s_1'}{ \langle s_1, s_2 \rangle \overset{a}{\rightarrow} \langle s_1', s_2 \rangle}</math> и <math>\frac{s_2 \overset{a}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{a}{\rightarrow} \langle s_1, s_2' \rangle}</math>
-
** рандеву для <math>\alpha \in H~:~~~ \frac{s_1 \overset{a}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{a}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{a}{\rightarrow} \langle s_1', s_2' \rangle}</math>
+
** рандеву для <math>\alpha \in H~:~~~ \frac{s_1 \overset{a}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{a}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{a}{\rightarrow} \langle s_1', s_2 \rangle}</math>
Строка 216: Строка 162:
Тогда <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) = <N, \leqslant, \xi></math>
-
* <math>\mathbb{N}</math> - множество натуральных чисел
+
* <math>N</math> - множество натуральных чисел
-
* <math>\leqslant</math> - отношение порядка на <math>\mathbb{N}</math>
+
* <math>\leqslant</math> - отношение порядка на <math>N</math>
-
* <math>\xi: \mathbb{N} \times AP \rightarrow \{true, false\}, ~~ \forall n>0, p \in AP ~~ \Rightarrow ~~ \xi(n, p) = true \Leftrightarrow p \in L(s)</math> (для каждого порядкового номера говорит истенен или ложен заданный на нем предикат)
+
* <math>\xi: N \times AP \rightarrow \{true, false\}, ~~ \forall n>0, p \in AP ~~ \Rightarrow ~~ \xi(n, p) = true \Leftrightarrow p \in L(s)</math>
Рассмотрим трассы tr и tr' такие, что
Рассмотрим трассы tr и tr' такие, что
-
* <math>I(tr) = \langle\mathbb{N}, \leqslant, \xi\rangle, ~~ \xi: \mathbb{N} \times AP = \{true, false\}</math>
+
* <math>I(tr) = <N, \leqslant, \xi>, ~~ \xi: 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) = <N, \leqslant, \xi'>, ~~ \xi: N \times AP' = \{true, false\}</math>
-
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \prec tr'</math>), если
+
Будем говорить, что трасса tr' является '''абстракцией трассы''' tr, если
# <math>AP' \subseteq AP</math>
# <math>AP' \subseteq AP</math>
-
# <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что
+
# <math>\exists \alpha : N \rightarrow N</math> такое, что <math>\forall n,k \in N, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k) </math>
-
#* <math>\alpha</math> - неубывающая функция: <math>\forall n,k \in \mathbb{N}, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k) </math>
+
# <math>\forall n \in N, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(n, p)</math>
-
#* <math>\forall n \in \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 модели. ===
Строка 439: Строка 199:
Достаточное условие корректности:
Достаточное условие корректности:
-
* Алфавит предикатов модели включен в алафвит предикатов системы: <math>AP^2 \sube AP^1 </math>
+
* Алфавит предикатов модели включен в алафвит предикатов системы: <math>AP^2 \subset AP^1 </math>
* Задано отображение <math>a: S^1 \rightarrow S^2</math>. На отображение накладываются следующие условия:
* Задано отображение <math>a: S^1 \rightarrow S^2</math>. На отображение накладываются следующие условия:
** Оно преобразует начальное состояние системы в начальное состояние модели: <math>s^2_0 = a(s^1_0)</math>
** Оно преобразует начальное состояние системы в начальное состояние модели: <math>s^2_0 = a(s^1_0)</math>
** Каждому переходу из системы должен соответствовать переход в модели: <math>s^1_1 \rightarrow_1 s^1_2 ~ \Rightarrow ~ a(s^1_1) \rightarrow_2 a(s^1_2)</math>
** Каждому переходу из системы должен соответствовать переход в модели: <math>s^1_1 \rightarrow_1 s^1_2 ~ \Rightarrow ~ a(s^1_1) \rightarrow_2 a(s^1_2)</math>
-
* Метки на состояниях модели должны состоять только из предикатов модели: <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 AP^1</math>
-
Модель называется '''адекватной''', если:
+
'''Достаточное условие адекватности модели свойствам правильность ''' :
-
* Атомарные высказывания, в терминах которых задаются свойства, присутствуют в разметке модели. ''(Необходимое условие)''
+
-
* Из нарушения свойства на модели следует, что оно нарушается и на исходной системе. ''(Достаточное условие)''
+
-
'''Необходимое условие адекватности модели свойствам правильности''': алфавит предикатов свойств правильности включен в алфавит предикатов модели — <math>AP_\phi \subseteq AP_M</math>. Условие не является достаточным (см. примеры, лекция 3, слайды 4—5).
+
Алфавит предикатов свойств правильности включен в алфавит предикатов модели.
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. ===
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. ===
-
Лекция 10, слайды 8 - 11
 
-
Программа PG' ''корректно моделирует'' программу PG тогда и только тогда, когда система переходов TS(PG') корректно моделирует систему переходов TS(PG).
 
- 
-
Будем говорить, что PG' моделирует PG, если
 
-
* в PG' присутствуют переменные, соответствующие наблюдаемым переменным PG
 
-
* все действия PG, влияющие на наблюдаемые переменные, отражены в модели <i>(наблюдаемые операторы)</i>
 
-
* модель корректно воспроизводит возможные последовательности изменения значений наблюдаемых переменных, присутствующих в PG
 
- 
-
'''Отношение слабой симуляции''' не сохраняет количество шагов между состояниями. В связи с этим, не сохраняются свойства, не инвариантные к
 
-
прореживанию (LTL: оператор neXt).
 
== Логика LTL, автоматы Бюхи ==
== Логика LTL, автоматы Бюхи ==
=== Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. ===
=== Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. ===
-
''Лекция 5, слайды 2-14.''
 
-
'''Требования правильности''' — утверждения о возможных и невозможных вариантах выполнения программы.
+
'''Требования правильности''' -- утверждения о возможных и невозможных вариантах выполнения программы.
<u>Двойственность</u> :
<u>Двойственность</u> :
-
* если какое-то утверждение невозможно, то обратное — неизбежно
+
* если какое-то утверждение невозможно, то обратное -- неизбежно
-
* если какое-то утверждение неизбежно, то обратное — невозможно
+
* если какое-то утверждение неизбежно, то обратное -- невозможно
* при помощи логики от одного можно переходить к другому при помощи отрицания
* при помощи логики от одного можно переходить к другому при помощи отрицания
Строка 481: Строка 228:
* в 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: Строка 249:
** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.
** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.
-
'''ps'''. автор терминов – Лесли Лампорт; см. ''Лекция 5, слайд 4''.
 
=== Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. ===
=== Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. ===
-
''Лекция 6, слайды 8 - 15''
 
- 
-
'''Конечный автомат'''
 
-
описывается сигнатурой: <math>\langle S, s_0, L, F, T\rangle</math>, где
 
- 
-
* S -- множество сотояний
 
-
* <math>s_0 \in S </math> -- множество начальных состояний
 
-
* L -- конечное множество меток
 
-
* <math>F \subseteq S </math> -- множество терминальных состояний
 
-
* <math>T \subseteq 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>
 
- 
-
В противном случае автомат называется '''недетерминированным'''.
 
- 
-
'''Проходом 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>
 
- 
- 
-
'''Допускающим проходом''' конечного автомата A называется конечный проход a, финальный переход которого
 
-
(<math>s_{n-1},l_{n-1},s_n)</math> ведёт в терминальное состояние.
 
- 
-
'''Языком автомата A''' называется множество слов в алфавите A.L, соответствующих допускающим проходам автомата А
 
- 
=== Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи. ===
=== Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи. ===
-
''Лекция 6, слайды 19-20''
 
- 
-
Для любого бесконечного прохода <math>\sigma</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. ===
'' Лекция 6, слайды 30 - 35''
'' Лекция 6, слайды 30 - 35''
Строка 554: Строка 259:
* может использоваться для описания свойств как живучести, так и безопасности
* может использоваться для описания свойств как живучести, так и безопасности
* описывает свойства, которым должны удовлетворять линейные последовательности наблюдаемых состояний - трассы
* описывает свойства, которым должны удовлетворять линейные последовательности наблюдаемых состояний - трассы
-
* семантика 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>
-
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. ===
+
'''Слабый Until:'''
-
'' Лекция 6, Слайды 38-39 ''
+
* всегда 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: Строка 307:
| <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 || ''цикличность (прогресс)'' ||
Строка 620: Строка 317:
=== Логика LTL. Эквивалентные преобразования формул LTL. ===
=== Логика LTL. Эквивалентные преобразования формул LTL. ===
-
'' Лекция 6, Слайды 40 ''
 
{| width="100%"
{| width="100%"
|
|
Строка 655: Строка 351:
=== Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию. ===
=== Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию. ===
-
''Лекция 7, слайды 22-25 ''
+
'''Оператор X нужно использовать аккуратно:'''
-
 
+
-
'''Оператор <math>X</math> нужно использовать аккуратно:'''
+
* с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния,
* с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния,
-
* в распределённых системах значение оператора <math>X</math> неочевидно,
+
* в распределённых системах значение оператора X неочевидно,
* поскольку алгоритм планирования процессов неизвестен, не стоит формулировать спецификацию в предположении о том,
* поскольку алгоритм планирования процессов неизвестен, не стоит формулировать спецификацию в предположении о том,
какое состояние будет следующим,
какое состояние будет следующим,
Строка 673: Строка 367:
** 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-формулы f существует автомат Бюхи, который допускает те и только те прогоны, которым соответствуют трассы, на которых выполнима f;
 
- 
-
'''Переход от LTL к автоматам'''
 
-
* Привести свойство правильности LTL к форме never языка Promela достаточно просто: нужно построить отрицание LTL формулы и поместить его в тело never:
 
-
** f выполняется на всех вычислениях <=>
 
-
** !f не выполняется ни на одном вычислении <=>
 
-
** автомат never {!f} не допускает ни одного прогона, полученного в результате синхронного выполнения с системой
 
- 
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. ===
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. ===
-
При помощи конструкции never можно описать любой &omega;-регулярный автомат над словами
 
- 
-
'''Выразительная мощность LTL'''
 
- 
-
по сравнению с конструкциями never
 
- 
-
* LTL описывает подмножество этого языка:
 
-
** всё, выразимое на LTL, может быть описано при помощи never,
 
-
** при помощи never можно описать свойства, не выразимые на LTL
 
-
* Добавление одного квантора существования над одним пропозициональным символом расширяет выразительные способности LTL до всех омега-регулярных автоматов над словами.
 
- 
-
(p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного.
 
- 
-
<math>\exists </math> t(t && [](t -> X!t) && [](!t -> Xt) && [](!t -> !p))
 
- 
-
LTL-формула описывает свойство, которое должно выполняться на '''всех''' вычислениях, начинающихся из исходного остояния системы
 
- 
-
'''Логика СTL*'''
 
-
* Логика ветвящегося времени:
 
-
** использует кванторы ∀ и ∃ для обозначения трасс, на которых может выполняться свойство
 
-
** использует F вместо <> и G вместо []
 
- 
-
'''Логика СTL'''
 
- 
-
Логика CTL – фрагмент логики CTL*, в котором кванторы могут встречаться только парами, причём в паре должны обязательно находиться один временной и один пространственный кванторы. Например: AG EF(p), A(p U q).
 
-
'''Выразительные возможности CTL* и CTL'''
 
-
* CTL* и CTL описывают подмножества w-регулярных автоматов над деревьями
 
-
** автоматы над деревьями более выразительны, чем автоматы над словами (CTL-формула выполнима на дереве трасс, а не на одной трассе);
 
-
* CTL и LTL являются подмножествами CTL*;
 
-
* CTL и LTL не сравнимы по выразительной мощности (пересекаются, но не включают);
 
-
* на LTL можно описать свойства, не выразимые на CTL:
 
-
** CTL не позволяет описать свойства вида []<>(p),
 
-
** при помощи []<>(p) в LTL задаются ограничения справедливости;
 
-
* на CTL можно описать свойства, не выразимые на LTL:
 
-
** на LTL нельзя описать свойства вида AGEF(p),
 
-
** AGEF(p) используется для описания свойства reset: из любого состояния
 
-
система может перейти в нормальное
 
== Верификация программ на моделях ==
== Верификация программ на моделях ==
Строка 745: Строка 390:
<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: Строка 411:
=== Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. ===
=== Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. ===
-
«Тестирование может показать присутствие ошибок, но не может показать их отсутствия» © Дейкстра.
 
- 
-
Обоснование полноты тестового покрытия:
 
-
* метод «чёрного ящика» (ЧЯ) — полное покрытие входных данных,
 
-
* метод «прозрачного ящика» (ПЯ) — полное покрытие кода программы.
 
-
Плюсы применения тестирования:
 
-
* проверяется та программа, которая будет использоваться,
 
-
* не требуется знание/использование дополнительных инструментальных средств,
 
-
* удобная локализация ошибки.
 
-
Минусы применения тестирования:
 
-
* не всегда есть условия для тестирования системы,
 
-
* проблема с воспроизводимостью тестов (частичное решение — имитационное моделирование).
 
- 
-
====Проблема полноты тестового покрытия====
 
-
* Чёрный ящик:
 
-
** для последовательных программ сложно перебрать все входные данные,
 
-
** для параллельных программ — очень сложно,
 
-
** для динамических структур данных, взаимодействия с окружением — невозможно.
 
-
* Прозрачный ящик:
 
-
** большой размер покрытия,
 
-
** часто невозможно построить 100% покрытие,
 
-
** полное покрытие не гарантирует отсутствия ошибок.
 
-
Итоги:
 
-
* Полный перебор входных данных — невозможен.
 
-
* Полнота покрытия кода не гарантирует правильности.
 
-
* Ошибка — ошибочное вычисление системы.
 
-
* Полнота в терминах возможных вычислений — хороший критерий.
 
=== Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. ===
=== Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. ===
Строка 873: Строка 491:
'' Лекция 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: Строка 502:
** корректная завершаемость
** корректная завершаемость
** причинно-следственный и темпоральный порядок состояний системы
** причинно-следственный и темпоральный порядок состояний системы
-
** Инварианты системы,
 
-
** Индикаторы прогресса,
 
-
====Схема верификации на модели====
+
''Схема верификации на модели: Лекция 2, слайд 3''
-
 
+
-
[[Изображение:Verif1.png|400px|Схема верификации на моделях (''Лекция 2, слайд 3'')]]
+
=== Верификация при помощи Spin. Задание свойств состояний. ===
=== Верификация при помощи Spin. Задание свойств состояний. ===
Строка 930: Строка 516:
=== Верификация при помощи Spin. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости. ===
=== Верификация при помощи Spin. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости. ===
- 
-
'''Свойства последовательностей состояний'''
 
-
* метки прогресса (чтобы найти циклы бездействия)
 
-
* утверждения о невозможности (never claims)
 
-
** например, определяются LTL-формулами
 
-
* трассовые ассерты
 
- 
-
'''Циклы бездействия'''. Мы хотим найти потенциально бесконечные циклы, не выполняющие никакой полезной работы. Помечаем меткой ''progress'' полезные операторы. Если найдется цикл, работающий потенциально бесконечно и не проходящий по метке progress, верификатор выдаст ошибку.
 
- 
-
'''Ограничения справедливости'''.
 
-
Существует два основных варианта справедливости:
 
-
* слабая справедливость:
 
-
** если оператор выполним бесконечно '''долго''', то он в конце концов будет выполнен
 
-
* сильная справедливость:
 
-
** если оператор выполним бесконечно '''часто''', то он в конце концов будет выполнен.
 
-
Справедливость применима как к внутреннему, так и к
 
-
внешнему недетерминизму.
 
-
Использование сильной справедливости – существенно дороже слабой
 
- 
=== Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты. ===
=== Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты. ===
'''never claims (утверждения о невозможности):'''
'''never claims (утверждения о невозможности):'''
-
* выполняются синхронно с моделью
+
* выполняются синхронно с моделью,
-
* если достигнут конец, то – ошибка
+
* если достигнут конец, то – ошибка,
-
* состоят из выражений и конструкция задания потока управления
+
* состоят из выражений и конструкция задания
-
* фактически, описывают распознающий автомат.
+
потока управления
 +
* фактически, описывают распознающий
 +
автомат.
'''Конструкция never'''
'''Конструкция never'''
Строка 978: Строка 547:
'''Ассерты на трассы'''
'''Ассерты на трассы'''
-
Используются для описания выполнения правильных и неправильных последовательностей операторов send и recieve. ''Ассерт notrace'' - утверждает, что описанный шаблон поведения
+
Используются для описания выполнения прывильных и неправильных последовательностей операторов send и recieve
-
невозможен.
+
=== Верификация при помощи 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
Личные инструменты
Разделы