ВПнМ/Теормин

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

(Различия между версиями)
Перейти к: навигация, поиск
м (Логика LTL. Эквивалентные преобразования формул LTL.)
м (Моделирование программ. Графы программ. Статическая и операционная семантика.)
Строка 108: Строка 108:
** находимся в точке программы l
** находимся в точке программы l
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
** значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
-
* Состояния <math><l,n></math> размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
+
* Состояния <math>\langle l,n \rangle</math> размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
-
* Если в графе программы есть дуга из l в <math>l^'</math> со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния <math><l,n></math> в состояние <math><l^', Effect(a,n)></math> по действию a.
+
* Если в графе программы есть дуга из l в <math>l'</math> со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния <math>\langle l,n\rangle</math> в состояние <math>\langle l', Effect(a,n)\rangle</math> по действию a.
'''Системы переходов графов программ'''
'''Системы переходов графов программ'''
Строка 116: Строка 116:
* <math>S = Loc \times Eval(V_p)</math> (декартово произведение точек программы на всевозможные подстановки)
* <math>S = Loc \times Eval(V_p)</math> (декартово произведение точек программы на всевозможные подстановки)
-
* <math>\rightarrow : S \times Act \times S </math> с соответствующим правилом вывода <math>l \overset{g:a}{\rightarrow} l \and (g |= n) </math> <math>\langle l,n \rangle \overset{a}{\rightarrow} \langle l^',Effect(a,n) \rangle </math>
+
* <math>\rightarrow : S \times Act \times S </math> с соответствующим правилом вывода <math>l \overset{g:a}{\rightarrow} l \and (g |= n) </math> <math>\langle l,n \rangle \overset{a}{\rightarrow} \langle l',Effect(a,n) \rangle </math>
* Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы:
* Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы:

Версия 18:17, 20 мая 2009

Содержание

Моделирование и абстракция

Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.

Схема верификации на моделях (Лекция 2, слайд 3)

Состояние программы - совокупность значений переменных и управления, связанных с некоторой моделью программы.

Модель - упрощённое описание реальности, выполненное с определенной целью.

  • с каждым объектом может быть связано несколько моделей
  • каждая модель отражает свой аспект реальности

Аспекты модели:

  • простота - модель должна быть проще, чем реальность
  • корректность - не расходиться с реальностью
  • адекватность - соответствовать решаемой задаче

Построение модели

  1. формализация требований (постановка задачи моделирования)
  2. выбор языка моделирования
  3. абстракция системы до модели с учётом требований

Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.

Размеченная система переходов (LTS)

TS = \langle S, Act, \overset{a}{\rightarrow} ,s_0, AP, L \rangle

  • S - множество состояний
  • Act - множество действий
  • τ - невидимое действие
  • \overset{a}{\rightarrow} \subseteq S \times Act \times S - тотальное отношение переходов
  • s_0 \in S - начальное состояние
  • AP - множество атомарных высказываний
  • L:S \rightarrow 2^{AP} - функция разметки

S, Act - конечные или счётные множества

\langle s, a, s' \rangle \in \overset{a}{\rightarrow} \equiv s \overset{a}{\rightarrow} s'

Пример LTS: Лекция 2, слайд 40-41

Прямые потомки

  • Post(s, a) = \{s' \in S, s \overset{a}{\rightarrow} s'\} - такие состояния s', которые непосредственно вытекают из s через переход a
  • Post(s) = \bigcup_{a \in Act} Post(s, a) - все возможные состояния s', которые непосредственно вытекают из s

Система TS = <S, Act, \overset{a}{\rightarrow} ,s_0, AP, L> детерменирована:

  • по действиям тогда и только тогда, когда
    • |I| \leqslant 1
    • \forall s \in S, \forall a \in Act \Rightarrow |Post(s, a)| \leqslant 1
  • по атомарным высказываниям
    • |I| \leqslant 1
    • \forall s \in S, \forall A \in 2^{AP} ~ \Rightarrow ~ |Post(s) \cap \{s' \in S, L(s') = A\}| \leqslant 1 ( количество одинаково размеченных потомков не больше одного )


Недетерменизм - это фича! Полезен для:

  • моделирования параллельного выполнения в режиме чередования (интерливинга)
    • позволяет не указывать скорость выполнения процессов
  • моделирования прототипа системы
    • не ограничивает реализацию заданным порядком выполнения операторов
  • построения абстракции реальной системы
    • модель может быть построена по неполной информации

Вычисления

  1. Конечный фрагмент вычисления σ системы переходов TS называется конечная последовательность чередующихся состояний и действий \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}
  2. Бесконечный (максимальный) фрагмент вычисления ρ - \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}
  3. Начальный фрагмент вычисления - фрагмент вычисления, для которого s_0 \in I
  4. Вычисление - начальный максимальный фрагмент вычисления

Достижимое состояние (из начального) в системе переходов TS - такое состояние s \in S, для которого существует конечный фрагмент вычисления s_0 a_1 s_1 a_2 s_2 \dots a_n s_n = s

Rich(TS) - множество всех достижимых состояний в TS

Трасса tr = L(s_0) L(s_1) \dots \in (2^{AP})^\omega

Свойства линейного времени

  • Свойство \varphi определяет набор допустимых трасс: \varphi \in (2^{AP})^\omega
  • Система переходов TS удовлетворяет свойству линейного времени \varphi
    • TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi
    • TS(P) \models \varphi ~~ \equiv ~~ P \models \varphi

Моделирование программ. Графы программ. Статическая и операционная семантика.

Граф программы – формальное описание текста программы.

  • Dp -- единый абстрактный домен данных.
  • P -- программа.
    • Vp -- множество переменных программы(Var).
  • v \in Var
    •  dom(v) = D_p^v \subseteq D_p -- каждая переменная принадлежит какому-либо домену
  • n -- подстановка. n: V_p \rightarrow D_p, \forall v  \in Var n(v) \in D_p^v
  • Cond(Vp) -- Набор булевых условий над Vp
    • формулы пропозициональной логики
    • условия на переменные
  • Эффект операторов: Effect: Act \times Eval(Var) \rightarrow Eval(Var)

Граф программы:

  PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle

  • Loc -- множество точек
    • Loc_0 \in Loc -- множество начальных точек
  • Act -- множество действий
  • \rightarrow : Loc \times (Cond(V_p) \times Act) \times Loc -- отношение перехода (Cond(Vp) -- это фактически страж оператора )
  • Effect -- функция эффекта
  • g_0 \in Cond(V_p) -- начальное условие

Получение TS из PG: раскрутка графа

  • Состояние в TS -- это точка программы и текущая подстановка
  • Начальное состояние -- исходная точка, удовлетворяющая начальному условию
  • Атомарные высказывания в TS:
    • находимся в точке программы l
    • значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
  • Состояния \langle l,n \rangle размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
  • Если в графе программы есть дуга из l в l' со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния \langle l,n\rangle в состояние \langle l', Effect(a,n)\rangle по действию a.

Системы переходов графов программ Операционная семантика -- строгое описание того как из графа программы получить ее систему переходов. Описывается это все при помощи правил вывода. TS(PG) -- система переходов графа программы   PG= \langle Loc , Act , Effect ,\rightarrow, Loc_0, g_0 \rangle задается сигнатурой  \langle S, Act, \rightarrow, I, AP, L \rangle

  • S = Loc \times Eval(V_p) (декартово произведение точек программы на всевозможные подстановки)
  • \rightarrow : S \times Act \times S с соответствующим правилом вывода l \overset{g:a}{\rightarrow} l \and (g |= n) \langle l,n \rangle \overset{a}{\rightarrow} \langle l',Effect(a,n) \rangle
  • Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы:
    • I={\langle l , n \rangle : l \in Loc_0 , n |=  g_0 }
  • Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы:
    • AP=Loc \cup Cond(V_P)
  • Состояния вида <l,n> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
    • L(\langle l , n \rangle)= (l) \cup (g \in Cond(V_P): n |=  g ).


Пример: Лекция 4, слайд 16

Параллелизм. Чередование систем переходов.

Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.

Параллелизм. Синхронный параллелизм. Рандеву.

  • распределённые программы выполняются параллельно
  • в распределённой программе нет разделяемых переменных

Передача сообщений в распределённых программах:

  • cинхронная передача сообщений (рандеву)
  • асинхронная передача сообщений (кналы)

Синхронный обмен сообщенийями:

  • Процессы вместе выполняют синхронизированные действия
  • Взаимодействие процессов - одновременно

Рандеву

  • TS_i = \langle S_i, Act_i, \overset{a}{\rightarrow}_i ,I_i, AP_i, L_i \rangle ~~~ i=\{1,2\}
  • H \subseteq Act_1 \cap Act_2

Тогда TS_1 ||_H = \langle S_1 \times S_2, Act_1 \cup Act_2, \rightarrow, I_1 \times I_2, AP_1 \cup AP_2, L \rangle, где

  • L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)
  • \rightarrow определяется как:
    • интерливинг для \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} и \frac{s_2 \overset{a}{\rightarrow}_2 s_2'}{ \langle s_1, s_2 \rangle \overset{a}{\rightarrow} \langle s_1, s_2' \rangle}
    • рандеву для \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}


Пример рандеву: Лекция 4, слайд 32


Синхронный параллелизм

  • TS_i = \langle S_i, Act_i, \overset{a}{\rightarrow}_i ,I_i, AP_i, L_i \rangle ~~~ i=\{1,2\}
  • Act_1 \times Act_2 \rightarrow Act ~~ : ~~ (\alpha, \beta) \rightarrow \alpha * \beta

Тогда 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 , где

  • L(\langle s_1, s_2 \rangle) = L_1(s_1) \cup L_2(s_2)
  • \rightarrow определяется как: \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}

Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.

Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.

Представим трассу в форме интерпретации I: I(tr) = <N, \leqslant, \xi>

  • N - множество натуральных чисел
  • \leqslant - отношение порядка на N
  • \xi: N \times AP \rightarrow \{true, false\}, ~~ \forall n>0, p \in AP ~~ \Rightarrow ~~ \xi(n, p) = true \Leftrightarrow p \in L(s)

Рассмотрим трассы tr и tr' такие, что

  • I(tr) = <N, \leqslant, \xi>, ~~ \xi: N \times AP = \{true, false\}
  • I(tr) = <N, \leqslant, \xi'>, ~~ \xi: N \times AP' = \{true, false\}

Будем говорить, что трасса tr' является абстракцией трассы tr, если

  1. AP' \subseteq AP
  2. \exists \alpha : N \rightarrow N такое, что \forall n,k \in N, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k)
  3. \forall n \in N, p \in AP' ~~ \Rightarrow ~~ \xi(n, p) = \xi'(n, p)

Пример абстракции трассы: Лекция 2, слайд 53

Необходимое условие корректности модели - \forall tr \in Traces(TS(P)) ~ \exists tr' \in Traces(TS(M)) ~ : ~ tr \leqslant tr', где

  • P - система
  • M - модель этой системы

При этом, если \varphi - некоторое свойство системы, то M \models \varphi ~ \Rightarrow ~ P \models \varphi выполняется тогда и только тогда, когда верно условие корректности модели.

Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.

Абстракция системы переходов -- картинка на 4 слайде 3-й лекции.

Достаточное условие корректности LTS модели.

Пусть у нас имеются две системы переходов, TS1 и TS2 -- для системы и модели соответственно:

 TS^i = \langle S^i, Act^i, \rightarrow_i, I^i, AP^i, L^i \rangle

Достаточное условие корректности:

  • Алфавит предикатов модели включен в алафвит предикатов системы: AP^2 \subset AP^1
  • Задано отображение a: S^1 \rightarrow S^2. На отображение накладываются следующие условия:
    • Оно преобразует начальное состояние системы в начальное состояние модели: s^2_0 = a(s^1_0)
    • Каждому переходу из системы должен соответствовать переход в модели: s^1_1 \rightarrow_1 s^1_2 ~ \Rightarrow ~ a(s^1_1) \rightarrow_2 a(s^1_2)
  • Метки на состояниях модели должны состоять только из предикатов модели: \forall s \in S^1: L^2(a(s)) = L^1(s) \cap  AP^1

Достаточное условие адекватности модели свойствам правильность  :

Алфавит предикатов свойств правильности включен в алфавит предикатов модели.

Абстракция. Абстракция графов программ. Отношение слабой симуляции.

Логика LTL, автоматы Бюхи

Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств.

Требования правильности -- утверждения о возможных и невозможных вариантах выполнения программы.

Двойственность :

  • если какое-то утверждение невозможно, то обратное -- неизбежно
  • если какое-то утверждение неизбежно, то обратное -- невозможно
  • при помощи логики от одного можно переходить к другому при помощи отрицания

Способы описания свойств правильности:

  • свойства достижимых состояний (свойства безопасности)
  • свойства последовательности состояний (свойства живучести)
  • в Promela:
    • свойства состояний
      • asserts
        • локальные ассерты процессов
        • инварианты системы процессов
      • метки терминальных состояний
        • задаём допустимые точки останова прочесса
    • свойства последовательностей состояний
      • метки прогресса - чтобы найти циклы бездействия
      • утверждения о невозможности (never claims) - например, LTL формулы
      • трассовые ассерты

Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств.

Типы свойств:

  • свойства безопасности
    • ничего плохого никогда не произойдет
    • пример: инвариант системы (например, x всегда меньше y);
    • задача верификатора -- найти те вычисления, которые ведут к нарушению безопасности.
  • свойства живучести
    • рано или поздно произойдет что-то хорошее
    • пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
    • задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.

Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата.

Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи.

Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until.

Лекция 6, слайды 30 - 35


Особенности LTL:

  • может использоваться для описания свойств как живучести, так и безопасности
  • описывает свойства, которым должны удовлетворять линейные последовательности наблюдаемых состояний - трассы
  • семантика LTL определена на бесконечных автоматах Бюхи. Для конечных проходов необходимо использовать расширение автоматаю

Формула в LTL f::=

  • p, q, ... -- свойства состояний, включая true и false
  • (f) -- группировка при помощи скобок
  • \alpha ~ f -- унарные операторы
  • f_1 ~ \beta ~ f_2 -- бинарные операторы

Операторы в LTL

  • унарные
    • \Box ([]) -- всегда в будущем
    • \diamond (<>) -- в конце концов
    • X (X) -- в следующем состоянии
    • \neg (!) -- логическое отрицание
  • бинарные
    • U (U) -- до тех пор, пока
    • \wedge (&&) -- логическое И
    • \vee (||) -- логическое ИЛИ
    • \rightarrow (->) -- логическая импликация
    • \leftrightarrow (<->) -- логическая эквивалентность

Сильный Until:

  • всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
  • 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}

Слабый Until:

  • всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e)
  • 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)

Выполнимость формул:

  • Задаётся последовательность состояний прохода σ
  • \forall i, i \geqslant 0, ~ \forall p ~~ : ~~ s_i \models p Внимание!! это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!!

Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция.

Лекция 6, Слайды 38-39

Распространенные LTL-формулы
Формула Описание Тип
\Box p всегда p инвариант
\diamond p рано или поздно p гарантия
p \rightarrow \diamond q если p, то рано или поздно q отклик
p \rightarrow q U r если p то затем q и рано или поздно r приоритет
\Box\diamond p всегда рано или позндно будет p цикличность (прогресс)
\diamond\Box p рано или позндно всегда будет p стабильность (бездействие)
\diamond p \rightarrow \diamond q если рано или поздно p, то рано или поздно q корреляция

Логика LTL. Эквивалентные преобразования формул LTL.

Лекция 6, Слайды 40


\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}


\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}

Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию.

Оператор X нужно использовать аккуратно:

  • с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния,
  • в распределённых системах значение оператора X неочевидно,
  • поскольку алгоритм планирования процессов неизвестен, не стоит формулировать спецификацию в предположении о том,

какое состояние будет следующим,

  • стоит ограничиться предположением о справедливости планирования.


Свойства, инвариантные к прореживанию

  • Пусть f – трасса некоторого вычисления над пропозициональными формулами P,
    • по трассе можно определить, выполняется ли на ней темпоральная формула,
    • трассу можно записать в форме:
      • f^{n_1}, f^{n_2},f^{n_3}, ... -- где значения пропозициональных формул на каждом интервале совпадают.
  • Обозначим E(f) набор всех трасс, отличающихся лишь значениями n1,n2,n3 (т.е. длиной интервалов).
    • E(f) называется расширением прореживания f.
  • Свойство ψ, инвариантное к прореживанию, либо истинно для всех трасс из E(ψ), либо ни для одной из них:
    • \psi \models f => \forall v \in E(\psi), v \models f
  • истинность такого свойства не зависит от длины трассы, а только от порядка, в котором пропозициональные формулы

меняют свои значения;

  • Теорема: все формулы LTL без оператора X инвариантны к

прореживанию.

Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin.

Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности.

Верификация программ на моделях

Задача проверки правильности программ. Валидация. Верификация. Системы с повышенными требованиями к надёжности. Реактивные программы. Параллельные программы. Особенности верификации таких программ.

Валидация - исследование и обоснование того, что спецификация ПО и само ПО через реализованную в нём функциональность удовлетворяет ребованиям пользователей.

Верификация - исследование и обоснование того, что программа соответствует своей спецификации.

Верификация в общем случае алгоритмически неразрешима.

Методы верификации:

  • "Полное" тестирование (слайды 14-22)
  • Имитационное моделирование
  • Доказательство теорем (27-29)
  • Статический анализ (30-33)
  • Верификация на моделях (34-38)

Типы программ:

  • Традиционные программы
    • завершимость
    • спецификация включает в себя описание входа/выхода программы
    • число состояний зависит от входных данных и переменных
  • Реактивные программы
    • работают в бесконечном цикле
    • взаимодействуют с окружением
    • спецификация представляет собой пары стимул/реакция
  • Параллельные программы
    • совместная работа нескольких компонент
    • невоспроизводимость тестов
    • ограниченные возможности по наблюдению

Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия.

Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы.

Основные пункты:

  • система и её свойста - формулы
  • задан набор аксиом и правил вывода
  • строится доказательство свойства-теоремы
  • таким образом, производится качественный анализ системы

Пример: Лекция 1, слайд 28

Достоинства:

  • работа с бесконечными пространствами состояний
  • даёт более глубокое понимание системы

Недостатки

  • медленная скорость работы
  • может потребоваться помощь человека (построение инвариантов циклов)
  • в общем случае нельзя построить полную систему аксиом и правил вывода

Подходы к верификации программ. Статический анализ исходного кода программ. Область применения, плюсы и минусы.

Статистический анализ -- оцениваем для каждого состояния программы потенциально возможные значения переменных.

Пример: Лекция 1, Слайды 31-32

Особенности:

  • анализ исходного текста без запуска программы
  • в общем случае задача неразрешима

Достоинства:

  • высокая скорость работы
  • если ответ дан - ему можно верить

Недостатки:

  • узкая область применения: компиляторы, анализ похожести кода, анализ безопасности
  • ручная настройка при изменении применяемых свойств

Подходы к верификации программ. Верификация программ на моделях. Процесс верификации программы при помощи её модели. Область применения, плюсы и минусы.

Лекция 1, Слайды 34-38 , 45

Особенности:

  • проверка свойств на конечной модели
  • исчерпывающий поиск по пространству состояний
  • свойства задаются в терминах значений предикатов состояний программы или последовательности этих значений

Пример: Лекция 1, слайды 35-36

Процесс верификации программ на моделях:

  • моделирование
    • построение адекватной, корректной модели
    • фильтрация "лишних" состояний
  • спецификация свойств
    • темпоральная логика
    • полнота свойств
  • верификация
    • построение контр-примера
    • анализ контр-примера

Достоинтсва:

  • хорошая автоматизация
  • если модель конечна, корректна и адекватна данному свойству, то будет получен точный ответ
  • выявление редких ошибок

Недостатки:

  • работает только для конечных моделей


Области применения

  • сетевые и криптографические протоколы
  • протоколы работы кэш-памяти
  • интегральные схемы
  • стандарты
  • встроенные системы
  • драйвера
  • и прочие программы на C

Верификация на моделях. История развития верификации программ на моделях. Схема верификации программ на моделях. Классы проверяемых свойств правильности программы.

Лекция 1, Слайды 40-44

Лекция 2, Слайды 3-4

Примеры классов свойств:

Схема верификации на модели: Лекция 2, слайд 3

Верификация при помощи Spin. Задание свойств состояний.

Cвойства состояний

  • asserts
    • локальные ассерты процессов
    • инварианты системы процессов
      • active proctype invariant() { assert(something)}
  • метки терминальных состояний
    • задаём допустимые точки останова процесса
      • метка end -- система не может завершить работу без того, чтобы все активные процессы либо завершились, либо остановились в точках, помеченных метками end;

Верификация при помощи Spin. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости.

Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты.

never claims (утверждения о невозможности):

  • выполняются синхронно с моделью,
  • если достигнут конец, то – ошибка,
  • состоят из выражений и конструкция задания

потока управления

  • фактически, описывают распознающий

автомат.

Конструкция never

  • может быть как детерминированной, так и нет;
  • содержит только выражения без побочных эффектов (соотв. булевым высказываниям на состояниях);
  • используются для описания неправильного поведения системы;
  • прерывается при блокировании:
    • блокируется => наблюдаемое поведение не соответствует описанному,
    • паузы в выполнении тела never должны быть явно заданы как бесконечные циклы;
  • never нарушается, если:
    • достигнута закрывающая скобка,
    • завершена конструкция accept (допускающий цикл);
  • бездействие может быть описано как конструкция never или её часть (для цикла бездействия есть тело never по умолчанию).

Видимость

  • все конструкции never – глобальны;
  • тем самым, в них можно ссылаться на
    • глобальные переменные,
    • каналы сообщений,
    • точки описания процессов (метки),
    • предопределённые глобальные переменные,
    • но не локальные переменные процессов;

Ассерты на трассы Используются для описания выполнения прывильных и неправильных последовательностей операторов send и recieve

Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin.

Система Spin и язык Promela

Система Spin. Процесс моделирования и верификации при помощи системы Spin. Конечность моделей на Promela. Асинхронное выполнение моделей. Недетерминированный поток управления. Понятие выполнимости оператора.

Язык Promela. Основные компоненты модели на языке Promela. Процессы, локальные и глобальные объекты данных, каналы сообщений.

Язык Promela. Механизмы взаимодействия процессов в языке Promela. Глобальные переменные, каналы сообщений, явная синхронизация.

Язык Promela. Основные операторы языка Promela. Операторы-выражения, присваивания.

Язык Promela. Основные операторы языка Promela. Отладочная печать, операторы skip, true, run, assert.

Язык Promela. Чередование (интерливинг) операторов. Внешний и внутренний недетерминизм. Управление выполнимостью операторов.

Язык Promela. Задание потока управления последовательного процесса. Управляющие конструкции if, do. Организация внутреннего недетерминизма.

Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений.

Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений.

Язык Promela. Основные типы данных. Область видимости данных.

Личные инструменты
Разделы