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

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

ПРЕДУПРЕЖДЕНИЕ: Вы редактируете устаревшую версию данной страницы. После сохранения страницы будут потеряны изменения, сделанные в последующих версиях.

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

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

== Моделирование и абстракция == === Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели. === Схема верификации на моделях (Лекция 2, слайд 3) '''Состояние программы''' - совокупность значений переменных и управления, связанных с некоторой моделью программы. '''Модель''' - упрощённое описание реальности, выполненное с определенной целью. * с каждым объектом может быть связано несколько моделей * каждая модель отражает свой аспект реальности <u>Аспекты модели:</u> * ''простота'' - модель должна быть проще, чем реальность * ''корректность'' - не расходиться с реальностью * ''адекватность'' - соответствовать решаемой задаче <u>Построение модели</u> # формализация требований (постановка задачи моделирования) # выбор языка моделирования # абстракция системы до модели с учётом требований === Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.=== '' Лекция 2, Слайды 39-50 '' ====Размеченная система переходов (LTS)==== <math>TS = \langle S, Act, \overset{a}{\rightarrow} ,s_0, AP, L \rangle </math> * S - множество состояний * Act - множество действий * '' <math>\tau</math> - невидимое действие '' * <math>\overset{a}{\rightarrow} \subseteq S \times Act \times S </math> - тотальное отношение переходов * <math>s_0 \in S</math> - начальное состояние * AP - множество атомарных высказываний * <math>L:S \rightarrow 2^{AP}</math> - функция разметки S, Act - конечные или счётные множества <math>\langle s, a, s' \rangle \in \overset{a}{\rightarrow} \equiv s \overset{a}{\rightarrow} s' </math> ''Пример LTS: Лекция 2, слайды 40-41'' '''Прямые потомки''' * <math>Post(s, a) = \{s' \in S, s \overset{a}{\rightarrow} s'\}</math> - такие состояния s', которые <u>непосредственно вытекают</u> из s через переход a * <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>|I| \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>\forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 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>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> '''Reach(TS)''' - множество всех достижимых состояний в TS '''Трасса''' <math>tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega</math> ====Свойства линейного времени==== * Свойство <math>\varphi</math> определяет набор допустимых трасс: <math>\varphi \subseteq (2^{AP})^\omega</math> * Система переходов TS удовлетворяет свойству линейного времени <math>\varphi</math> ** <math>TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi</math> ** <math>P \models \varphi ~~ \equiv ~~ TS(P) \models \varphi </math> - по определению программа удовлетворяет свойству &phi;, если её система переходов удовлетворяет этому свойству === Моделирование программ. Графы программ. Статическая и операционная семантика. === '''Граф программы''' – формальное описание текста программы. * <math>D_p</math> -- единый абстрактный домен данных. * <math>P</math> -- программа. ** <math>V_p</math> -- множество переменных программы(Var). * <math>v \in Var</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>Cond(V_p)</math> -- Набор булевых условий над <math>V_p</math> ** формулы пропозициональной логики ** условия на переменные * <math>Eval(Var)</math> -- множество значений переменных. * Эффект операторов: <math>Effect: Act \times Eval(Var) \rightarrow Eval(Var)</math> '''Граф программы:''' <math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math> * <math>Loc</math> -- множество точек ** <math>Loc_0 \in Loc</math> -- множество начальных точек * <math>Act</math> -- множество действий * <math>\rightarrow \subseteq Loc \times (Cond(V_p) \times Act) \times Loc </math> -- отношение перехода (<math>Cond(V_p) </math> -- это фактически страж оператора ) * <math>Effect</math> -- функция эффекта * <math>g_0 \in Cond(V_p)</math> -- начальное условие '''Получение TS из PG: раскрутка графа''' * Состояние в TS -- это точка программы и текущая подстановка * Начальное состояние -- исходная точка, удовлетворяющая начальному условию * Атомарные высказывания в TS: ** находимся в точке программы l ** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной. * Состояния <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. '''Системы переходов графов программ''' Операционная семантика -- строгое описание того как из графа программы получить ее систему переходов. Описывается это все при помощи правил вывода. TS(PG) -- система переходов графа программы <math> PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle </math> задается сигнатурой <math> \langle S, Act, \rightarrow, I, AP, L \rangle </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>I={\langle l , n \rangle : l \in Loc_0 , n \models g_0 }</math> * Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы: ** <math>AP=Loc \cup Cond(V_P) </math> * Состояния вида <math>\langle l,n \rangle</math> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке: ** <math>L(\langle l , n \rangle)= (l) \cup (g \in Cond(V_P): n \models g ).</math> ''Пример: Лекция 4, слайд 16'' === Параллелизм. Чередование систем переходов. === ''Лекция 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> === Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными. === === Параллелизм. Синхронный параллелизм. Рандеву. === * распределённые программы выполняются параллельно * в распределённой программе нет разделяемых переменных <u>Передача сообщений в распределённых программах:</u> * cинхронная передача сообщений (рандеву) * асинхронная передача сообщений (каналы) <u>Синхронный обмен сообщениями:</u> * Процессы вместе выполняют синхронизированные действия * Взаимодействие процессов - одновременно '''Рандеву''' * <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> -- набор синхронизированных действий. ** действия из 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>L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)</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 \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> '' Пример рандеву: Лекция 4, слайд 32 '' '''Синхронный параллелизм''' * <math>TS_i = \langle S_i, Act_i, \overset{a}{\rightarrow}_i ,I_i, AP_i, L_i \rangle ~~~ i=\{1,2\}</math> * <math>Act_1 \times Act_2 \rightarrow Act ~~ : ~~ (\alpha, \beta) \rightarrow \alpha * \beta</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>\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 = \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 модели. === Представим трассу в форме интерпретации I: <math>I(tr) = <\mathbb{N}, \leqslant, \xi></math> * <math>\mathbb{N}</math> - множество натуральных чисел * <math>\leqslant</math> - отношение порядка на <math>\mathbb{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> (для каждого порядкового номера говорит истенен или ложен заданный на нем предикат) Рассмотрим трассы tr и tr' такие, что * <math>I(tr) = <\mathbb{N}, \leqslant, \xi>, ~~ \xi: \mathbb{N} \times AP = \{true, false\}</math> * <math>I(tr) = <\mathbb{N}, \leqslant, \xi'>, ~~ \xi: \mathbb{N} \times AP' = \{true, false\}</math> Будем говорить, что трасса tr' является '''абстракцией трассы''' tr (<math>tr \leqslant tr'</math>), если # <math>AP' \subseteq AP</math> # <math>\exists \alpha : \mathbb{N} \rightarrow \mathbb{N}</math> такое, что <math>\forall n,k \in \mathbb{N}, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k) </math> - некоторая неубывающая функция [?] # <math>\forall n \in \mathbb{N}, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(\alpha(n), p)</math> Пример абстракции трассы: Лекция 2, слайд 53 ''' Необходимое условие корректности модели ''' - <math>\forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr'</math>, где * <math>P</math> - система * <math>M</math> - модель этой системы При этом, если <math>\varphi</math> - некоторое свойство системы, то <math>M \models \varphi ~ \Rightarrow ~ P \models \varphi</math> выполняется тогда и только тогда, когда верно условие корректности модели. === Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели. === Абстракция системы переходов -- картинка на 4 слайде 3-й лекции. '''Достаточное условие корректности LTS модели.''' Пусть у нас имеются две системы переходов, <math>TS^1</math> и <math>TS^2</math> -- для системы и модели соответственно: <math> TS^i = \langle S^i, Act^i, \rightarrow_i, I^i, AP^i, L^i \rangle </math> Достаточное условие корректности: * Алфавит предикатов модели включен в алафвит предикатов системы: <math>AP^2 \sube AP^1 </math> * Задано отображение <math>a: S^1 \rightarrow S^2</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>\forall s \in S^1: L^2(a(s)) = L^1(s) \cap 2^{AP^2}</math> '''Необходимое (но не достаточное) [?] условие адекватности модели свойствам правильности''' : Алфавит предикатов свойств правильности включен в алфавит предикатов модели. === Абстракция. Абстракция графов программ. Отношение слабой симуляции. === Лекция 10, слайды 8 - 11 Программа PG' ''корректно моделирует'' программу PG тогда и только тогда, когда система переходов TS(PG') корректно моделирует систему переходов TS(PG). Будем говорить, что PG' моделирует PG, если * в PG' присутствуют переменные, соответствующие наблюдаемым переменным PG * все действия PG, влияющие на наблюдаемые переменные, отражены в модели <i>(наблюдаемые операторы)</i> * модель корректно воспроизводит возможные последовательности изменения значений наблюдаемых переменных, присутствующих в PG '''Отношение слабой симуляции''' не сохраняет количество шагов между состояниями. В связи с этим, не сохраняются свойства, не инвариантные к прореживанию (LTL: оператор neXt). == Логика LTL, автоматы Бюхи == === Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств. === '''Требования правильности''' -- утверждения о возможных и невозможных вариантах выполнения программы. <u>Двойственность</u> : * если какое-то утверждение невозможно, то обратное -- неизбежно * если какое-то утверждение неизбежно, то обратное -- невозможно * при помощи логики от одного можно переходить к другому при помощи отрицания <u>Способы описания свойств правильности:</u> * свойства достижимых состояний (свойства безопасности) * свойства последовательности состояний (свойства живучести) * в Promela: ** свойства состояний *** asserts **** локальные ассерты процессов **** инварианты системы процессов *** метки терминальных состояний **** задаём допустимые точки останова прочесса ** свойства последовательностей состояний *** метки прогресса - чтобы найти циклы бездействия *** утверждения о невозможности (never claims) - например, LTL формулы *** трассовые ассерты - используются для описания правильных последовательностей выполнения операторов отправки и приема сообщения === Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств. === <u>Типы свойств:</u> * свойства безопасности ** ничего плохого никогда не произойдет ** пример: инвариант системы (например, x всегда меньше y); ** задача верификатора -- найти те вычисления, которые ведут к нарушению безопасности. * свойства живучести ** рано или поздно произойдет что-то хорошее ** пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ) ** задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности. === Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата. === Лекция 6, слайды 8 - 15 '''Конечный автомат''' описывается сигнатурой: <math>\langle S, s_0, L, F, T\rangle</math>, где * S -- множество сотояний * <math>s_0 \in S </math> -- множество начальных состояний * L -- конечное множество меток * <math>F \subset S </math> -- множество терминальных состояний * <math>T \subset S \times L \times S</math> -- отношение перехода на состояниях ''' Детерминизм и недетерминизм''' Конечный автомат называется '''детерминированным''', если по метке и исходному состоянию можно однозначно определить целевое состояние: <math>\forall s \in S, \forall l \in L: ((s, l, s_1) \in A.T \and (s, L, s_2) \in A.T => 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 >= 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, слайды 16'' '''Допускающий проход по Бюхи'''(w-допускание) конечного автомата A называется такой ''бесконечный проход'' a, что <math>\exists i \geqslant 0, (s_{i-1}, l_{i-1}, s_i) \in a ~~ : ~~ (s_{i} \in A.F) \and (s_{i} \in a^w) </math> т.е. по крайней мере одно терминальное состояние встречается бесконечно часто. '''Расширение автоматов Бюхи.''' Конечные проходы дополняются бесконечным переходом по пустому действию. При помощи автоматов Бюхи удобно проверять свойства живучести. === Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until. === '' Лекция 6, слайды 30 - 35'' <u>Особенности LTL:</u> * может использоваться для описания свойств как живучести, так и безопасности * описывает свойства, которым должны удовлетворять линейные последовательности наблюдаемых состояний - трассы * семантика LTL определена на бесконечных автоматах Бюхи. Для конечных проходов необходимо использовать расширение автоматаю <u>Формула в LTL '''f::='''</u> * '''p, q, ... ''' -- свойства состояний, включая '''true''' и '''false''' * '''(f)''' -- группировка при помощи скобок * '''<math>\alpha ~ f</math>''' -- унарные операторы * '''<math>f_1 ~ \beta ~ f_2</math>''' -- бинарные операторы <u>Операторы в LTL</u> * унарные ** <math>\Box</math> ([]) -- всегда в будущем ** <math>\diamond</math> (<>) -- в конце концов ** <math>X</math> (X) -- в следующем состоянии ** <math>\neg</math> (!) -- логическое отрицание * бинарные ** <math>U</math> (U) -- до тех пор, пока ** <math>\wedge</math> (&&) -- логическое И ** <math>\vee</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 \\ \forall k, i \leqslant k < j: ~ s_k \models e \end{cases}</math> '''Слабый Until:''' * всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e) * <math>s_i \models e \cup f ~~ \Leftrightarrow ~~ s_i \models f \vee (s_i \models e \wedge s_{i+1} \models s_i \cup f)</math> <u>Выполнимость формул:</u> * Задаётся последовательность состояний прохода <math>\sigma</math> * <math>\forall i, i \geqslant 0, ~ \forall p ~~ : ~~ s_i \models p </math> '' Внимание!! это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!! '' === Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. === '' Лекция 6, Слайды 38-39 '' {| |+ Распространенные LTL-формулы |- ! Формула !! Описание !! Тип || |- | <math>\Box p</math> || всегда p || ''инвариант'' || |- | <math>\diamond p</math> || рано или поздно p || ''гарантия'' || |- | <math>p \rightarrow \diamond q</math> || если p, то рано или поздно q || ''отклик'' || |- | <math>p \rightarrow q U r</math> || если p то затем q и рано или поздно r || ''приоритет'' || |- | <math>\Box\diamond p</math> || всегда рано или позндно будет p || ''цикличность (прогресс)'' || |- | <math>\diamond\Box p</math> || рано или позндно всегда будет p || ''стабильность (бездействие)'' || |- | <math>\diamond p \rightarrow \diamond q</math> || если рано или поздно p, то рано или поздно q || ''корреляция'' || |} === Логика LTL. Эквивалентные преобразования формул LTL. === '' Лекция 6, Слайды 40 '' {| width="100%" | <math> \begin{align} \neg\Box p & \Leftrightarrow & \diamond \neg p \\ \neg\diamond p & \Leftrightarrow & \Box \neg p \\ & & \\ \neg(p U q) & \Leftrightarrow & \neg q \cup (\neg p \wedge \neg q) \\ \neg(p \cup q) & \Leftrightarrow & \neg q U (\neg p \wedge \neg q) \\ & & \\ \Box (p \wedge q) & \Leftrightarrow & \Box p \wedge \Box q \\ \diamond (p \vee q) & \Leftrightarrow & \diamond p \vee \diamond q \\ \end{align} </math> | <math> \begin{align} p \cup (q \vee r) & \Leftrightarrow & (p \cup q) \vee (p \cup r) \\ (p \wedge q) \cup r & \Leftrightarrow & (p \cup r) \wedge (q \cup r) \\ & & \\ p U (q \vee r) & \Leftrightarrow & (p U q) \vee (p U r) \\ (p U q) \cup r & \Leftrightarrow & (p U r) \wedge (q U r) \\ & & \\ \Box\diamond (p \wedge q) & \Leftrightarrow & \Box\diamond p \wedge \Box\diamond q \\ \diamond\Box (p \vee q) & \Leftrightarrow & \diamond\Box p \vee \diamond\Box q \\ \end{align} </math> |} === Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию. === '''Оператор X нужно использовать аккуратно:''' * с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния, * в распределённых системах значение оператора X неочевидно, * поскольку алгоритм планирования процессов неизвестен, не стоит формулировать спецификацию в предположении о том, какое состояние будет следующим, * стоит ограничиться предположением о справедливости планирования. '''Свойства, инвариантные к прореживанию''' * Пусть f – трасса некоторого вычисления над пропозициональными формулами P, ** по трассе можно определить, выполняется ли на ней темпоральная формула, ** трассу можно записать в форме: ***<math>f^{n_1}, f^{n_2},f^{n_3}, ... </math> -- где значения пропозициональных формул на каждом интервале совпадают. * Обозначим E(f) набор всех трасс, отличающихся лишь значениями <math>n_1, n_2, n_3</math> (т.е. длиной интервалов). ** E(f) называется расширением прореживания f. * Свойство f, инвариантное к прореживанию, либо истинно для всех трасс из <math>E(\psi)</math>, либо ни для одной из них: ** <math>\psi \models f => \forall v \in E(\psi), v \models f </math> * истинность такого свойства не зависит от длины трассы, а только от порядка, в котором пропозициональные формулы меняют свои значения; * Теорема: все формулы LTL без оператора X инвариантны к прореживанию. === Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin. === '''Связь LTL с автоматами Бюхи''' * Удобно проверять допустимость трасс для некоторого автомата Бюхи; * Удобно описывать свойства правильности при помощи темпоральных формул; * Для всякой LTL-формулы f существует автомат Бюхи, который допускает те и только те прогоны, которым соответствуют трассы, на которых выполнима f; '''Переход от LTL к автоматам''' * Привести свойство правильности LTL к форме never языка Promela достаточно просто: нужно построить отрицание LTL формулы и поместить его в тело never: ** f выполняется на всех вычислениях <=> ** !f не выполняется ни на одном вычислении <=> ** автомат never {!f} не допускает ни одного прогона, полученного в результате синхронного выполнения с системой === Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности. === При помощи конструкции never можно описать любой w-регулярный автомат над словами '''Выразительная мощность 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*, в котором под управлением квантора пути (E или A) может находиться не более дного оператора X или U '''Выразительные возможности 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: из любого состояния система может перейти в нормальное == Верификация программ на моделях == === Задача проверки правильности программ. Валидация. Верификация. Системы с повышенными требованиями к надёжности. Реактивные программы. Параллельные программы. Особенности верификации таких программ. === '''Валидация''' - исследование и обоснование того, что спецификация ПО и само ПО через реализованную в нём функциональность удовлетворяет ребованиям пользователей. '''Верификация''' - исследование и обоснование того, что программа соответствует своей спецификации. Верификация в общем случае алгоритмически неразрешима. <u>Методы верификации:</u> * "Полное" тестирование (слайды 14-22) * Имитационное моделирование * Доказательство теорем (27-29) * Статический анализ (30-33) * Верификация на моделях (34-38) <u>Типы программ:</u> * Традиционные программы ** завершимость ** спецификация включает в себя описание входа/выхода программы ** число состояний зависит от входных данных и переменных * Реактивные программы ** работают в бесконечном цикле ** взаимодействуют с окружением ** спецификация представляет собой пары стимул/реакция * Параллельные программы ** совместная работа нескольких компонент ** невоспроизводимость тестов ** ограниченные возможности по наблюдению === Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия. === === Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы. === Основные пункты: * система и её свойста - формулы * задан набор аксиом и правил вывода * строится доказательство свойства-теоремы * таким образом, производится '' качественный '' анализ системы ''Пример: Лекция 1, слайд 28 '' <u>Достоинства:</u> * работа с бесконечными пространствами состояний * даёт более глубокое понимание системы <u>Недостатки</u> * медленная скорость работы * может потребоваться помощь человека (построение инвариантов циклов) * в общем случае нельзя построить полную систему аксиом и правил вывода === Подходы к верификации программ. Статический анализ исходного кода программ. Область применения, плюсы и минусы. === Статистический анализ -- оцениваем для каждого состояния программы потенциально возможные значения переменных. ''Пример: Лекция 1, Слайды 31-32 '' <u>Особенности:</u> * анализ исходного текста без запуска программы * в общем случае задача неразрешима <u>Достоинства:</u> * высокая скорость работы * если ответ дан - ему можно верить <u>Недостатки:</u> * узкая область применения: компиляторы, анализ похожести кода, анализ безопасности * ручная настройка при изменении применяемых свойств === Подходы к верификации программ. Верификация программ на моделях. Процесс верификации программы при помощи её модели. Область применения, плюсы и минусы. === ''Лекция 1, Слайды 34-38 , 45'' <u>Особенности:</u> * проверка свойств на конечной модели * исчерпывающий поиск по пространству состояний * свойства задаются в терминах значений предикатов состояний программы или последовательности этих значений '' Пример: Лекция 1, слайды 35-36 '' <u>Процесс верификации программ на моделях:</u> * моделирование ** построение адекватной, корректной модели ** фильтрация "лишних" состояний * спецификация свойств ** темпоральная логика ** полнота свойств * верификация ** построение контр-примера ** анализ контр-примера <u>Достоинтсва:</u> * хорошая автоматизация * если модель конечна, корректна и адекватна данному свойству, то будет получен точный ответ * выявление редких ошибок <u>Недостатки:</u> * работает только для конечных моделей <u>Области применения</u> * сетевые и криптографические протоколы * протоколы работы кэш-памяти * интегральные схемы * стандарты * встроенные системы * драйвера * и прочие программы на C === Верификация на моделях. История развития верификации программ на моделях. Схема верификации программ на моделях. Классы проверяемых свойств правильности программы. === '' Лекция 1, Слайды 40-44 '' '' Лекция 2, Слайды 3-4 '' <u>Примеры классов свойств:</u> * Стандартные ** [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 состояние гонки]) * Специфичные для конкретного приложения ** требования справедливости ** корректная завершаемость ** причинно-следственный и темпоральный порядок состояний системы ''Схема верификации на модели: Лекция 2, слайд 3'' === Верификация при помощи Spin. Задание свойств состояний. === '''Cвойства состояний''' * asserts ** локальные ассерты процессов ** инварианты системы процессов *** active proctype invariant() { assert(something)} * метки терминальных состояний ** задаём допустимые точки останова процесса *** метка end -- система не может завершить работу без того, чтобы все активные процессы либо завершились, либо остановились в точках, помеченных метками end; === Верификация при помощи Spin. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости. === '''Свойства последовательностей состояний''' * метки прогресса (чтобы найти циклы бездействия) * утверждения о невозможности (never claims) ** например, определяются LTL-формулами * трассовые ассерты '''Циклы бездействия'''. Мы хотим найти потенциально бесконечные циклы, не выполняющие никакой полезной работы. Помечаем меткой ''progress'' полезные операторы. Если найдется цикл, работающий потенциально бесконечно и не проходящий по метке progress, верификатор выдаст ошибку. '''Ограничения справедливости'''. Существует два основных варианта справедливости: * слабая справедливость: ** если оператор выполним бесконечно долго, то он в конце концов будет выполнен * сильная справедливость: ** если оператор выполним бесконечно часто,то он в конце концов будет выполнен. Справедливость применима как к внутреннему, так и к внешнему недетерминизму. Использование сильной справедливости – существенно дороже слабой === Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты. === '''never claims (утверждения о невозможности):''' * выполняются синхронно с моделью, * если достигнут конец, то – ошибка, * состоят из выражений и конструкция задания потока управления * фактически, описывают распознающий автомат. '''Конструкция never''' * может быть как детерминированной, так и нет; * содержит только выражения без побочных эффектов (соотв. булевым высказываниям на состояниях); * используются для описания неправильного поведения системы; * прерывается при блокировании: ** блокируется => наблюдаемое поведение не соответствует описанному, ** паузы в выполнении тела never должны быть явно заданы как бесконечные циклы; * never нарушается, если: ** достигнута закрывающая скобка, ** завершена конструкция accept (допускающий цикл); * бездействие может быть описано как конструкция never или её часть (для цикла бездействия есть тело never по умолчанию). '''Видимость''' * все конструкции never – глобальны; * тем самым, в них можно ссылаться на ** глобальные переменные, ** каналы сообщений, ** точки описания процессов (метки), ** предопределённые глобальные переменные, ** но не локальные переменные процессов; '''Ассерты на трассы''' Используются для описания выполнения правильных и неправильных последовательностей операторов send и recieve. ''Ассерт notrace'' - утверждает, что описанный шаблон поведения невозможен. === Верификация при помощи 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. Процесс моделирования и верификации при помощи системы 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. Процессы, локальные и глобальные объекты данных, каналы сообщений. === '''Устройство модели'''. Существует три типа объектов: * процессы * глобальные и локальные объекты данных * каналы сообщений '''Процессы''' * Поведение процесса задаётся в объявлении типа процесса (proctype) * Экземпляр процесса – инстанциация proctype * Два вида инстанцирования процессов: ** В начальном состоянии системы - ''префикс active'' ** В произвольном достижимом состоянии системы - ''оператор run'' '''Локальные и глобальные объекты данных'''. Два уровня видимости: * глобальный (данные видны всем активным процессам) * локальный (данные видны только одному процессу) ** есть особенность: локальная переменная, объявленная в теле процесса, видна во всем процессе (нет понятия ''область видимости переменной'' внутри процесса) '''Каналы сообщений''' * каналы бывают двух типов: ** буферизованные (асинхронные) ** небуферизованные (синхронные, рандеву) * пример объявления канала: chan x = [10] of {int, short, bit}; ** ''10'' - максимальное число сообщений в канале. 0 определяет канал рандеву. ** ''{int, short, bit}'' - структура пересылаемых сообщений === Язык 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. Отладочная печать, операторы skip, true, run, assert. === === Язык Promela. Чередование (интерливинг) операторов. Внешний и внутренний недетерминизм. Управление выполнимостью операторов. === === Язык Promela. Задание потока управления последовательного процесса. Управляющие конструкции if, do. Организация внутреннего недетерминизма. === === Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений. === === Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений. === === Язык Promela. Основные типы данных. Область видимости данных. ===

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

Описание изменений:

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

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

• Шаблон:Курс ВПнМ