Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 79 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 1: | Строка 1: | ||
== Моделирование и абстракция == | == Моделирование и абстракция == | ||
=== Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели. === | === Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели. === | ||
- | + | Схема верификации на моделях (Лекция 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>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>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> | + | * Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</math> |
- | * | + | ** <math>TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi</math> |
+ | ** <math>P \models \varphi ~~ \equiv ~~ TS(P) \models \varphi </math> - по определению программа удовлетворяет свойству φ, если её система переходов удовлетворяет этому свойству | ||
=== Моделирование программ. Графы программ. Статическая и операционная семантика. === | === Моделирование программ. Графы программ. Статическая и операционная семантика. === | ||
Строка 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> | + | * <math>Cond(V_p)</math> -- Набор булевых условий над <math>V_p</math> |
- | ** формулы пропозициональной логики | + | ** формулы пропозициональной логики |
- | ** условия на переменные | + | ** условия на переменные |
- | * <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> | + | * <math>Loc</math> -- множество точек |
** <math>Loc_0 \in Loc</math> -- множество начальных точек | ** <math>Loc_0 \in Loc</math> -- множество начальных точек | ||
- | * <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> | + | * <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>\langle l,n \rangle</math> размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n |
- | * Если в графе программы есть дуга из | + | * Если в графе программы есть дуга из 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 | + | * <math>\rightarrow : S \times Act \times S </math> с соответствующим правилом вывода <math> \frac{l \overset{g:a}{\rightarrow} l \and (n \models g) }{\langle l,n \rangle \overset{a}{\rightarrow} \langle l',Effect(a,n) \rangle }</math> |
* Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы: | * Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы: | ||
- | ** <math>I= | + | ** <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)= | + | ** <math>L(\langle l , n \rangle)= (l) \cup (g \in Cond(V_P): n \models g ).</math> |
- | + | ''Пример: Лекция 4, слайд 16'' | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
=== Параллелизм. Чередование систем переходов. === | === Параллелизм. Чередование систем переходов. === | ||
Строка 168: | Строка 159: | ||
'' Лекция 4, слайды 25—28 '' | '' Лекция 4, слайды 25—28 '' | ||
- | Для графов программ <math>PG_1</math> (над <math>V_1</math>) и <math>PG_2</math> (над <math>V_2</math>) без разделяемых переменных (т. е. <math>V_1 \cap V_2 = \ | + | Для графов программ <math>PG_1</math> (над <math>V_1</math>) и <math>PG_2</math> (над <math>V_2</math>) без разделяемых переменных (т. е. <math>V_1 \cap V_2 = \emptyset</math>), формула |
- | + | :<math>TS(PG_1)~|||~TS(PG_2)</math> | |
- | + | достоверно описывает параллельную композицию <math>PG_1</math> и <math>PG_2</math>. В случае с разделяемыми переменными это не так (см. лекцию 4, слайд 26). | |
Пусть | Пусть | ||
Строка 177: | Строка 168: | ||
:<math>PG_1~|||~PG_2 = \langle Loc_1 \times Loc_2, Act_1 \cup Act_2, Effect, \rightarrow, Loc_{0,1} \times Loc_{0,2}, g_{0,1} \land g_{0,2} \rangle,</math> | :<math>PG_1~|||~PG_2 = \langle Loc_1 \times Loc_2, Act_1 \cup Act_2, Effect, \rightarrow, Loc_{0,1} \times Loc_{0,2}, g_{0,1} \land g_{0,2} \rangle,</math> | ||
где отношение перехода <math>\rightarrow</math> определяется следующими правилами вывода: | где отношение перехода <math>\rightarrow</math> определяется следующими правилами вывода: | ||
- | :<math>l_1 \overset{g: | + | :<math>l_1 \overset{g:a}{\rightarrow}_1 l'_1 \over \langle l_1, l_2 \rangle \overset{g:a}{\rightarrow} \langle l'_1, l_2 \rangle</math> и <math>l_2 \overset{g:a}{\rightarrow}_2 l'_2 \over \langle l_1, l_2 \rangle \overset{g:a}{\rightarrow} \langle l_1, l'_2 \rangle,</math> |
а <math>Effect(\alpha,~\eta) = Effect_i(\alpha,~\eta),</math> если <math>\alpha \in Act_i.</math> | а <math>Effect(\alpha,~\eta) = Effect_i(\alpha,~\eta),</math> если <math>\alpha \in Act_i.</math> | ||
Строка 216: | Строка 207: | ||
Тогда <math>TS_1 \times TS_2 = \langle S_1 \times S_2, Act, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle </math>, где | Тогда <math>TS_1 \times TS_2 = \langle S_1 \times S_2, Act, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle </math>, где | ||
* <math>L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)</math> | * <math>L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)</math> | ||
- | * <math>\rightarrow</math> определяется как: <math>\frac{s_1 \overset{\alpha}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{\beta}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{\alpha * \beta}{\rightarrow} \langle s_1', s_2 | + | * <math>\rightarrow</math> определяется как: <math>\frac{s_1 \overset{\alpha}{\rightarrow}_1 s_1' ~ \wedge ~ s_2 \overset{\beta}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{\alpha * \beta}{\rightarrow} \langle s_1', s_2 \rangle}</math> |
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. === | === Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. === | ||
Строка 231: | Строка 222: | ||
<u>Системы с каналами.</u> | <u>Системы с каналами.</u> | ||
- | * Граф программы | + | * Граф программы задаётся <math>PG = \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> |
- | * Система с каналами | + | * Система с каналами CS над <math>\bigcup_{1 \leqslant i \leqslant n} PG_i, Chan</math> задаётся как <math>\left[PG_1, PG_2, \dots, PG_n \right]</math>, где <math>PG_i</math> -- граф программы над <math>(Var_i, Chan)</math> |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
=== Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. === | === Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели. === | ||
- | Представим трассу в форме интерпретации I: <math>I(tr) = | + | Представим трассу в форме интерпретации I: <math>I(tr) = <\mathbb{N}, \leqslant, \xi></math> |
* <math>\mathbb{N}</math> - множество натуральных чисел | * <math>\mathbb{N}</math> - множество натуральных чисел | ||
* <math>\leqslant</math> - отношение порядка на <math>\mathbb{N}</math> | * <math>\leqslant</math> - отношение порядка на <math>\mathbb{N}</math> | ||
Строка 409: | Строка 233: | ||
Рассмотрим трассы tr и tr' такие, что | Рассмотрим трассы tr и tr' такие, что | ||
- | * <math>I(tr) = | + | * <math>I(tr) = <\mathbb{N}, \leqslant, \xi>, ~~ \xi: \mathbb{N} \times AP = \{true, false\}</math> |
- | * <math>I(tr | + | * <math>I(tr) = <\mathbb{N}, \leqslant, \xi'>, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math> |
- | Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \ | + | Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \leqslant tr'</math>), если |
# <math>AP' \subseteq AP</math> | # <math>AP' \subseteq AP</math> | ||
# <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что | # <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что | ||
Строка 420: | Строка 244: | ||
Пример абстракции трассы: Лекция 2, слайд 53 | Пример абстракции трассы: Лекция 2, слайд 53 | ||
- | ''' | + | ''' Необходимое условие корректности модели ''' - <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr'</math>, где |
- | <math> | + | * <math>P</math> - система |
- | + | * <math>M</math> - модель этой системы | |
- | + | При этом, если <math>\varphi</math> - некоторое свойство системы, то <math>M \models \varphi ~ \Rightarrow ~ P \models \varphi</math> выполняется тогда и только тогда, когда верно условие корректности модели. | |
- | + | ||
- | + | ||
- | + | ||
=== Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. === | === Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. === | ||
Строка 445: | Строка 266: | ||
* Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap 2^{AP^2}</math> | * Метки на состояниях модели должны состоять только из предикатов модели: <math>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap 2^{AP^2}</math> | ||
- | + | '''Необходимое (но не достаточное) [?] условие адекватности модели свойствам правильности''' : | |
- | + | ||
- | + | ||
- | + | Алфавит предикатов свойств правильности включен в алфавит предикатов модели. | |
=== Абстракция. Абстракция графов программ. Отношение слабой симуляции. === | === Абстракция. Абстракция графов программ. Отношение слабой симуляции. === | ||
Строка 467: | Строка 286: | ||
=== Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. === | === Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. === | ||
- | ''Лекция 5, слайды 2-14.'' | ||
- | '''Требования правильности''' | + | '''Требования правильности''' -- утверждения о возможных и невозможных вариантах выполнения программы. |
<u>Двойственность</u> : | <u>Двойственность</u> : | ||
- | * если какое-то утверждение невозможно, то обратное | + | * если какое-то утверждение невозможно, то обратное -- неизбежно |
- | * если какое-то утверждение неизбежно, то обратное | + | * если какое-то утверждение неизбежно, то обратное -- невозможно |
* при помощи логики от одного можно переходить к другому при помощи отрицания | * при помощи логики от одного можно переходить к другому при помощи отрицания | ||
Строка 481: | Строка 299: | ||
* в Promela: | * в Promela: | ||
** свойства состояний | ** свойства состояний | ||
- | *** | + | *** asserts |
**** локальные ассерты процессов | **** локальные ассерты процессов | ||
- | **** | + | **** инварианты системы процессов |
*** метки терминальных состояний | *** метки терминальных состояний | ||
**** задаём допустимые точки останова прочесса | **** задаём допустимые точки останова прочесса | ||
** свойства последовательностей состояний | ** свойства последовательностей состояний | ||
- | *** метки прогресса | + | *** метки прогресса - чтобы найти циклы бездействия |
- | *** утверждения о невозможности (never claims) | + | *** утверждения о невозможности (never claims) - например, LTL формулы |
- | *** трассовые ассерты | + | *** трассовые ассерты - используются для описания правильных последовательностей выполнения операторов отправки и приема сообщения |
=== Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств. === | === Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств. === | ||
Строка 502: | Строка 320: | ||
** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ) | ** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ) | ||
** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности. | ** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности. | ||
- | '''ps'''. автор терминов – Лесли Лампорт; см. ''Лекция 5, слайд 4''. | ||
=== Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. === | === Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. === | ||
Строка 557: | Строка 374: | ||
<u>Формула в LTL '''f::='''</u> | <u>Формула в LTL '''f::='''</u> | ||
- | * '''p, q, ... ''' | + | * '''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>\Box</math> ([]) -- всегда в будущем |
- | ** <math>\ | + | ** <math>\diamond</math> (<>) -- в конце концов |
- | ** <math>X</math> (X) | + | ** <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>\leftrightarrow</math> (<->) -- логическая эквивалентность | |
- | + | '''Сильный Until:''' | |
- | + | * всегда e, до тех пор, пока не f, при этом f обязательно должно наступить | |
- | + | * <math>s_i \models e U f ~~ \Leftrightarrow ~~ \begin{cases} | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
\exists j, j \geqslant i: ~ s_j \models f \\ | \exists j, j \geqslant i: ~ s_j \models f \\ | ||
\forall k, i \leqslant k < j: ~ s_k \models e | \forall k, i \leqslant k < j: ~ s_k \models e | ||
\end{cases}</math> | \end{cases}</math> | ||
+ | |||
+ | '''Слабый Until:''' | ||
+ | * всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e) | ||
+ | * <math>s_i \models e \cup f ~~ \Leftrightarrow ~~ s_i \models f \vee (s_i \models e \wedge s_{i+1} \models e \cup f)</math> | ||
+ | |||
+ | <u>Выполнимость формул:</u> | ||
+ | * Задаётся последовательность состояний прохода <math>\sigma</math> | ||
+ | * <math>\forall i, i \geqslant 0, ~ \forall p ~~ : ~~ s_i \models p </math> '' Внимание!! это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!! '' | ||
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. === | === Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. === | ||
Строка 694: | Строка 508: | ||
=== Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. === | === Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. === | ||
- | При помощи конструкции never можно описать любой | + | При помощи конструкции never можно описать любой w-регулярный автомат над словами |
'''Выразительная мощность LTL''' | '''Выразительная мощность LTL''' | ||
Строка 707: | Строка 521: | ||
(p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного. | (p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного. | ||
- | <math>\exists </math> t | + | <math>\exists </math> t.t && [](t -> X!t) && [](!t -> Xt) && [](!t -> !p) |
LTL-формула описывает свойство, которое должно выполняться на '''всех''' вычислениях, начинающихся из исходного остояния системы | LTL-формула описывает свойство, которое должно выполняться на '''всех''' вычислениях, начинающихся из исходного остояния системы | ||
Строка 713: | Строка 527: | ||
'''Логика СTL*''' | '''Логика СTL*''' | ||
* Логика ветвящегося времени: | * Логика ветвящегося времени: | ||
- | ** использует кванторы ∀ и ∃ | + | ** использует кванторы ∀ и ∃ |
** использует F вместо <> и G вместо [] | ** использует F вместо <> и G вместо [] | ||
'''Логика СTL''' | '''Логика СTL''' | ||
- | Логика CTL – фрагмент логики CTL*, в котором | + | Логика CTL – фрагмент логики CTL*, в котором под управлением квантора пути (E или A) может находиться не более дного |
+ | оператора X или U | ||
'''Выразительные возможности CTL* и CTL''' | '''Выразительные возможности CTL* и CTL''' | ||
Строка 745: | Строка 560: | ||
<u>Методы верификации:</u> | <u>Методы верификации:</u> | ||
- | * "Полное" тестирование ( | + | * "Полное" тестирование (слайды 14-22) |
- | * Имитационное моделирование | + | * Имитационное моделирование |
- | * Доказательство теорем ( | + | * Доказательство теорем (27-29) |
- | * Статический анализ ( | + | * Статический анализ (30-33) |
- | * Верификация на моделях ( | + | * Верификация на моделях (34-38) |
<u>Типы программ:</u> | <u>Типы программ:</u> | ||
Строка 766: | Строка 581: | ||
=== Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. === | === Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. === | ||
- | «Тестирование может показать присутствие ошибок, но не может показать их отсутствия» © Дейкстра. | ||
- | |||
- | Обоснование полноты тестового покрытия: | ||
- | * метод «чёрного ящика» (ЧЯ) — полное покрытие входных данных, | ||
- | * метод «прозрачного ящика» (ПЯ) — полное покрытие кода программы. | ||
- | Плюсы применения тестирования: | ||
- | * проверяется та программа, которая будет использоваться, | ||
- | * не требуется знание/использование дополнительных инструментальных средств, | ||
- | * удобная локализация ошибки. | ||
- | Минусы применения тестирования: | ||
- | * не всегда есть условия для тестирования системы, | ||
- | * проблема с воспроизводимостью тестов (частичное решение — имитационное моделирование). | ||
- | |||
- | ====Проблема полноты тестового покрытия==== | ||
- | * Чёрный ящик: | ||
- | ** для последовательных программ сложно перебрать все входные данные, | ||
- | ** для параллельных программ — очень сложно, | ||
- | ** для динамических структур данных, взаимодействия с окружением — невозможно. | ||
- | * Прозрачный ящик: | ||
- | ** большой размер покрытия, | ||
- | ** часто невозможно построить 100% покрытие, | ||
- | ** полное покрытие не гарантирует отсутствия ошибок. | ||
- | Итоги: | ||
- | * Полный перебор входных данных — невозможен. | ||
- | * Полнота покрытия кода не гарантирует правильности. | ||
- | * Ошибка — ошибочное вычисление системы. | ||
- | * Полнота в терминах возможных вычислений — хороший критерий. | ||
=== Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. === | === Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. === | ||
Строка 873: | Строка 661: | ||
'' Лекция 1, Слайды 40-44 '' | '' Лекция 1, Слайды 40-44 '' | ||
- | |||
- | '''История развития''' верификации программ на моделях: | ||
- | * Флойд, 1967 – assertions, гипотеза о доказуемости корректности программы, | ||
- | * Хоар, 1969 – пред- и пост-условия, триплеты Хоара (P | S | Q), логический вывод, | ||
- | * Бойер, Мур, 1971 – первый автоматический прувер, | ||
- | * Дейкстра, 1975 – Guarded Command Languages, | ||
- | * Хоар, 1978 – взаимодействующие последовательные процессы (CSP). | ||
- | * Пнуэли, 1977 – темпоральная логика LTL, | ||
- | * Пнуэли, 1981 – логика ветвящегося времени (CTL), | ||
- | * Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний), | ||
- | * Варди и Вольпер, 1986 – новая техника model checking (анализ конформности), | ||
- | * Хольцман, 1989 – верификатор SPIN. | ||
- | * Бриан, 1989 – Двоичные решающие диаграммы (BDD), | ||
- | * МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD), | ||
- | * Хольцман, Пелед, 1994 – редукция частичных порядков, | ||
- | * 1995 – редукция частичных порядков в SPIN. | ||
- | * Кларк, 1992 – абстракция для уменьшения числа состояний модели, | ||
- | * Эльсаиди, 1994 – семантическая минимизация, | ||
- | * Пелед, 1996, Бир, 1998 – верификация модели «на лету», | ||
- | * Равви, 2000 – анализ достижимости с учётом спецификации, | ||
- | * Эмерсон, Прасад, 1994 -- симметрия | ||
- | '''Рост мощности''' model checking: | ||
- | * 1992 год – 1020 состояний, | ||
- | * 1994 год – 10120 состояний, | ||
- | * 1998 год(?) – 10394 состояний | ||
'' Лекция 2, Слайды 3-4 '' | '' Лекция 2, Слайды 3-4 '' | ||
- | + | <u>Примеры классов свойств:</u> | |
* Стандартные | * Стандартные | ||
- | ** Отсутствие ошибок времени выполнения (RTE), | ||
- | ** Отсутствие удушения (starvation), | ||
- | ** Не срабатывают ассерты(assertions). | ||
** [http://en.wikipedia.org/wiki/Deadlock deadlocks] ([http://ru.wikipedia.org/wiki/%D0%92%D0%B7%D0%B0%D0%B8%D0%BC%D0%BD%D0%B0%D1%8F_%D0%B1%D0%BB%D0%BE%D0%BA%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0 взаимная блокировка]) | ** [http://en.wikipedia.org/wiki/Deadlock deadlocks] ([http://ru.wikipedia.org/wiki/%D0%92%D0%B7%D0%B0%D0%B8%D0%BC%D0%BD%D0%B0%D1%8F_%D0%B1%D0%BB%D0%BE%D0%BA%D0%B8%D1%80%D0%BE%D0%B2%D0%BA%D0%B0 взаимная блокировка]) | ||
** [http://en.wikipedia.org/wiki/Race_condition Race condition] ([http://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%81%D1%82%D0%BE%D1%8F%D0%BD%D0%B8%D0%B5_%D0%B3%D0%BE%D0%BD%D0%BA%D0%B8 состояние гонки]) | ** [http://en.wikipedia.org/wiki/Race_condition Race condition] ([http://ru.wikipedia.org/wiki/%D0%A1%D0%BE%D1%81%D1%82%D0%BE%D1%8F%D0%BD%D0%B8%D0%B5_%D0%B3%D0%BE%D0%BD%D0%BA%D0%B8 состояние гонки]) | ||
Строка 912: | Строка 672: | ||
** корректная завершаемость | ** корректная завершаемость | ||
** причинно-следственный и темпоральный порядок состояний системы | ** причинно-следственный и темпоральный порядок состояний системы | ||
- | ** Инварианты системы, | ||
- | ** Индикаторы прогресса, | ||
- | |||
- | ====Схема верификации на модели==== | ||
- | + | ''Схема верификации на модели: Лекция 2, слайд 3'' | |
=== Верификация при помощи Spin. Задание свойств состояний. === | === Верификация при помощи Spin. Задание свойств состояний. === | ||
Строка 1115: | Строка 871: | ||
** присваивание | ** присваивание | ||
** печать | ** печать | ||
- | ** проверка свойства безопасности | + | ** проверка свойства безопасности |
** отправка сообщения | ** отправка сообщения | ||
** прием сообщения | ** прием сообщения |