Редактирование: ВПнМ/Теормин
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
ПРЕДУПРЕЖДЕНИЕ: Длина этой страницы составляет 87 килобайт. Страницы, размер которых приближается к 32 КБ или превышает это значение, могут неверно отображаться в некоторых браузерах. Пожалуйста, рассмотрите вариант разбиения страницы на меньшие части.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 3: | Строка 3: | ||
[[Изображение:Verif1.png|400px|thumb|right|Схема верификации на моделях (''Лекция 2, слайд 3'')]] | [[Изображение:Verif1.png|400px|thumb|right|Схема верификации на моделях (''Лекция 2, слайд 3'')]] | ||
- | '''Состояние программы''' - совокупность значений | + | '''Состояние программы''' - совокупность значений переменных и управления, связанных с некоторой моделью программы. |
'''Модель''' - упрощённое описание реальности, выполненное с определенной целью. | '''Модель''' - упрощённое описание реальности, выполненное с определенной целью. | ||
Строка 74: | Строка 74: | ||
'''Reach(TS)''' - множество всех достижимых состояний в TS | '''Reach(TS)''' - множество всех достижимых состояний в TS | ||
- | '''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math> | + | '''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math> |
====Свойства линейного времени==== | ====Свойства линейного времени==== | ||
Строка 90: | Строка 90: | ||
** <math> dom(v) = D_p^v \subseteq D_p</math> -- каждая переменная принадлежит какому-либо домену | ** <math> dom(v) = D_p^v \subseteq D_p</math> -- каждая переменная принадлежит какому-либо домену | ||
* <math>n</math> -- подстановка. <math>n: V_p \rightarrow D_p, \forall v \in Var</math> <math>n(v) \in D_p^v</math> | * <math>n</math> -- подстановка. <math>n: V_p \rightarrow D_p, \forall v \in Var</math> <math>n(v) \in D_p^v</math> | ||
- | * <math> | + | * <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: | Строка 100: | ||
<math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math> | <math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math> | ||
- | * <math> | + | * <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: | Строка 113: | ||
** находимся в точке программы 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. |
'''Системы переходов графов программ''' | '''Системы переходов графов программ''' | ||
Строка 131: | Строка 131: | ||
- | + | ''Пример: Лекция 4, слайд 16'' | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
=== Параллелизм. Чередование систем переходов. === | === Параллелизм. Чередование систем переходов. === | ||
Строка 216: | Строка 209: | ||
Тогда <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> |
=== Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. === | === Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика. === | ||
Строка 247: | Строка 240: | ||
''Операционная семантика: лекция 4, слайды 44—46'' | ''Операционная семантика: лекция 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 модели. === | ||
Строка 412: | Строка 252: | ||
* <math>I(tr') = \langle\mathbb{N}, \leqslant, \xi'\rangle, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math> | * <math>I(tr') = \langle\mathbb{N}, \leqslant, \xi'\rangle, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math> | ||
- | Будем говорить, что трасса 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: | Строка 260: | ||
Пример абстракции трассы: Лекция 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 модели. === | ||
Строка 444: | Строка 281: | ||
** Каждому переходу из системы должен соответствовать переход в модели: <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 2^{AP^2}</math> | ||
- | |||
- | Модель называется '''адекватной''', если: | ||
- | * Атомарные высказывания, в терминах которых задаются свойства, присутствуют в разметке модели. ''(Необходимое условие)'' | ||
- | * Из нарушения свойства на модели следует, что оно нарушается и на исходной системе. ''(Достаточное условие)'' | ||
'''Необходимое условие адекватности модели свойствам правильности''': алфавит предикатов свойств правильности включен в алфавит предикатов модели — <math>AP_\phi \subseteq AP_M</math>. Условие не является достаточным (см. примеры, лекция 3, слайды 4—5). | '''Необходимое условие адекватности модели свойствам правильности''': алфавит предикатов свойств правильности включен в алфавит предикатов модели — <math>AP_\phi \subseteq AP_M</math>. Условие не является достаточным (см. примеры, лекция 3, слайды 4—5). | ||
Строка 575: | Строка 408: | ||
** <math>U</math> (U) — до тех пор, пока (until) | ** <math>U</math> (U) — до тех пор, пока (until) | ||
- | + | '''Сильный 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> ('''Внимание'''!! ''это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!!'' может быть, здесь имеется в виду что в каждом состоянии определена формула, или что если есть формула, то она определена в каком-то состоянии. вообщем, wierd). | ||
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. === | === Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. === | ||
Строка 884: | Строка 714: | ||
* Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний), | * Кларк, Эмерсон, 1981 и Квили, Сифакис, 1982 – model checking (обход достижимых состояний), | ||
* Варди и Вольпер, 1986 – новая техника model checking (анализ конформности), | * Варди и Вольпер, 1986 – новая техника model checking (анализ конформности), | ||
- | * Хольцман, | + | * Хольцман, 1981 – верификатор SPIN. |
* Бриан, 1989 – Двоичные решающие диаграммы (BDD), | * Бриан, 1989 – Двоичные решающие диаграммы (BDD), | ||
* МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD), | * МакМиллан, 1993 – верификатор SMV (символьная верификация, BDD), | ||
Строка 901: | Строка 731: | ||
'' Лекция 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: | Строка 739: | ||
** корректная завершаемость | ** корректная завершаемость | ||
** причинно-следственный и темпоральный порядок состояний системы | ** причинно-следственный и темпоральный порядок состояний системы | ||
- | ** Инварианты системы, | ||
- | ** Индикаторы прогресса, | ||
- | |||
- | ====Схема верификации на модели==== | ||
- | + | ''Схема верификации на модели: Лекция 2, слайд 3'' | |
=== Верификация при помощи Spin. Задание свойств состояний. === | === Верификация при помощи Spin. Задание свойств состояний. === |