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

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

(Различия между версиями)

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

Версия 16:27, 20 мая 2009

Содержание

1 Моделирование и абстракция
2 Логика LTL, автоматы Бюхи
3 Верификация программ на моделях
4 Система Spin и язык Promela

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

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

Схема верификации на моделях (Лекция 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$ ( количество одинаково размеченных потомков не больше одного )

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

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

Вычисления

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

Достижимое состояние (из начального) в системе переходов 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 удовлетворяет свойству линейного времени
- $TS \models \varphi ~~ \Leftrightarrow ~~ Traces(TS) \subseteq \varphi$
- $TS(P) \models \varphi ~~ \equiv ~~ P \models \varphi$

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

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

$D p$ -- единый абстрактный домен данных.
P -- программа.
- $V p$ -- множество переменных программы(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(V_p) -- Набор булевых условий над V_p
- формулы пропозициональной логики
- условия на переменные
Эффект операторов: $Effect: Act \times Eval(Var) \rightarrow Eval(Var)$

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

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

Loc -- множество точек
- $Loc_0 \in Loc$ -- множество начальных точек
$A c t$ -- множество действий
$\rightarrow : Loc \times (Cond(V_p) \times Act) \times Loc$ -- отношение перехода ( $C o n d (V p)$ -- это фактически страж оператора )
$E f f e c t$ -- функция эффекта
$g_0 \in Cond(V_p)$ -- начальное условие

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

Состояние в TS -- это точка программы и текущая подстановка
Начальное состояние -- исходная точка, удовлетворяющая начальному условию
Атомарные высказывания в TS:
- находимся в точке программы l
- значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
Состояния $< l, n >$ размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
Если в графе программы есть дуга из l в $l'$ со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния $< l, n >$ в состояние $< l', E f f e c t (a, n) >$ по действию 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)$
определяется как:
- интерливинг для $\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, если

$AP' \subseteq AP$
$\exists \alpha : N \rightarrow N$ такое, что $\forall n,k \in N, n \leqslant k ~~ \Rightarrow ~~ \alpha(n) \leqslant \alpha(k)$
$\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 модели.

Пусть у нас имеются две системы переходов, $T S 1$ и $T S 2$ -- для системы и модели соответственно:

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

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

Алфавит предикатов модели включен в алафвит предикатов системы: $AP^2 \subset AP^1$
Задано отображение . На отображение накладываются следующие условия:
- Оно преобразует начальное состояние системы в начальное состояние модели: $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, автоматы Бюхи

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

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

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

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

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

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

Стандартные
- deadlocks (взаимная блокировка)
- Race condition (состояние гонки)
Специфичные для конкретного приложения
- требования справедливости
- корректная завершаемость
- причинно-следственный и темпоральный порядок состояний системы

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Недостатки

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

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

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

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

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

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

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

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

Недостатки:

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

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

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

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

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

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

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

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

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

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

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

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

автомат.

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

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

Верификация при помощи 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. Основные типы данных. Область видимости данных.

Получено с http://esyr.us/wiki/%D0%92%D0%9F%D0%BD%D0%9C/%D0%A2%D0%B5%D0%BE%D1%80%D0%BC%D0%B8%D0%BD

@@ Строка 365: / Строка 365: @@
 '''Конструкция never'''
 * может быть как детерминированной, так и нет;
-* содержит только выражения без побочных эффектов (соотв. булевым
+* содержит только выражения без побочных эффектов (соотв. булевым высказываниям на состояниях);
-высказываниям на состояниях);
 * используются для описания неправильного поведения системы;
 * прерывается при блокировании:
 ** блокируется => наблюдаемое поведение не соответствует описанному,
-** паузы в выполнении тела never должны быть явно заданы как бесконечные
+** паузы в выполнении тела never должны быть явно заданы как бесконечные циклы;
-циклы;
 * never нарушается, если:
 ** достигнута закрывающая скобка,
 ** завершена конструкция accept (допускающий цикл);
-* бездействие может быть описано как конструкция never или её часть
+* бездействие может быть описано как конструкция never или её часть (для цикла бездействия есть тело never по умолчанию).
-(для цикла бездействия есть тело never по умолчанию).
 === Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin. ===