ВПнМ/Теормин
Материал из eSyr's wiki.
м (→Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств. - доб. ссылка на лекцию) |
м (→Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until. - ...) |
||
Строка 388: | Строка 388: | ||
<u>Формула в LTL '''f::='''</u> | <u>Формула в LTL '''f::='''</u> | ||
- | * '''p, q, ... ''' | + | * '''p, q, ... ''' — свойства состояний, включая '''true''' и '''false''' |
- | * '''(f)''' | + | * '''(f)''' — группировка при помощи скобок |
- | * '''<math>\alpha ~ f</math>''' | + | * '''<math>\alpha ~ f</math>''' — унарные операторы |
- | * '''<math>f_1 ~ \beta ~ f_2</math>''' | + | * '''<math>f_1 ~ \beta ~ f_2</math>''' — бинарные операторы |
<u>Операторы в LTL</u> | <u>Операторы в LTL</u> | ||
* унарные | * унарные | ||
- | ** <math>\Box</math> ([]) | + | ** <math>\Box</math> ([]) — всегда в будущем, т.е. <math>s_j \models \Box f ~~~ \Leftrightarrow ~~~ \forall j, j \geqslant i: ~ s_j \models f</math> |
- | ** <math>\ | + | ** <math>\Diamond</math> (<>) — в конце концов, т.е. <math>s_j \models \Diamond f ~~~ \Leftrightarrow ~~~ \exists j, j \geqslant i: ~ s_j \models f</math> |
- | ** <math>X</math> (X) | + | ** <math>X</math> (X) — в следующем состоянии, т.е. <math>s_j \models X f ~~~ \Leftrightarrow ~~~ i: ~ s_{j+1} \models f</math> |
- | ** <math>\neg</math> (!) | + | ** <math>\neg</math> (!) — логическое отрицание |
* бинарные | * бинарные | ||
- | + | ** <math>\wedge</math> (&&) — логическое И | |
- | ** <math>\wedge</math> (&&) | + | ** <math>\vee</math> (||) — логическое ИЛИ |
- | ** <math>\vee</math> (||) | + | ** <math>\rightarrow</math> (->) — логическая импликация |
- | ** <math>\rightarrow</math> (->) | + | ** <math>\leftrightarrow</math> (<->) — логическая эквивалентность |
- | ** <math>\leftrightarrow</math> (<->) | + | ** <math>U</math> (U) — до тех пор, пока (until) |
'''Сильный Until:''' | '''Сильный Until:''' | ||
Строка 419: | Строка 419: | ||
<u>Выполнимость формул:</u> | <u>Выполнимость формул:</u> | ||
* Задаётся последовательность состояний прохода <math>\sigma</math> | * Задаётся последовательность состояний прохода <math>\sigma</math> | ||
- | * <math>\forall i, i \geqslant 0, ~ \forall p ~~ : ~~ s_i \models p </math> '' Внимание!! это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!! '' | + | * <math>\forall i, i \geqslant 0, ~ \forall p ~~ : ~~ s_i \models p </math> ('''Внимание'''!! ''это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!!'' может быть, здесь имеется в виду что в каждом состоянии определена формула, или что если есть формула, то она определена в каком-то состоянии. вообщем, wierd). |
=== Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. === | === Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция. === |
Версия 11:59, 14 июня 2009
Моделирование и абстракция
Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.
Состояние программы - совокупность значений переменных и управления, связанных с некоторой моделью программы.
Модель - упрощённое описание реальности, выполненное с определенной целью.
- с каждым объектом может быть связано несколько моделей
- каждая модель отражает свой аспект реальности
Аспекты модели:
- простота - модель должна быть проще, чем реальность
- корректность - не расходиться с реальностью
- адекватность - соответствовать решаемой задаче
Построение модели
- формализация требований (постановка задачи моделирования)
- выбор языка моделирования
- абстракция системы до модели с учётом требований
Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.
Лекция 2, Слайды 39-50
Размеченная система переходов (LTS)
- S - множество состояний
- Act - множество действий
- τ - невидимое действие
- - тотальное отношение переходов. Тотальность означает, что из каждого состояния ведёт какое-то действие.
- - начальное состояние, либо I - множество начальных состояний
- AP - множество атомарных высказываний
- - функция разметки
S, Act - конечные или счётные множества
Пример LTS: Лекция 2, слайды 40-41
Прямые потомки
- - такие состояния s', которые непосредственно вытекают из s через переход a
- - все возможные состояния s', которые непосредственно вытекают из s
Система детерминирована:
- по действиям тогда и только тогда, когда
- (количество потомков не больше одного)
- по атомарным высказываниям
- (количество одинаково размеченных потомков не больше одного)
Недетерминизм - это фича! Полезен для:
- моделирования параллельного выполнения в режиме чередования (интерливинга)
- позволяет не указывать скорость выполнения процессов
- моделирования прототипа системы
- не ограничивает реализацию заданным порядком выполнения операторов
- построения абстракции реальной системы
- модель может быть построена по неполной информации
Вычисления
- Конечный фрагмент вычисления σ системы переходов TS - это конечная последовательность чередующихся состояний и действий, заканчивающаяся состоянием:
- Бесконечный (максимальный) фрагмент вычисления ρ -
- Начальный фрагмент вычисления - фрагмент вычисления, для которого
- Вычисление - начальный максимальный фрагмент вычисления (описывает последовательность состояний и действий)
Достижимое состояние (из начального) в системе переходов TS - такое состояние , для которого существует конечный фрагмент вычисления
Reach(TS) - множество всех достижимых состояний в TS
Трасса
Свойства линейного времени
- Свойство определяет набор допустимых трасс:
- Система переходов TS удовлетворяет свойству линейного времени , если:
- по определению программа удовлетворяет свойству φ, если её система переходов удовлетворяет этому свойству: -
Моделирование программ. Графы программ. Статическая и операционная семантика.
Граф программы – формальное описание текста программы.
- Dp -- единый абстрактный домен данных.
- P -- программа.
- Vp -- множество переменных программы(Var).
-
- -- каждая переменная принадлежит какому-либо домену
- n -- подстановка.
- Cond(Vp) -- Набор булевых условий над Vp
- формулы пропозициональной логики
- условия на переменные
- Eval(Var) -- множество значений переменных. Собственно, это и есть подстановка.
- Эффект операторов:
Граф программы:
- Loc -- множество точек
- -- множество начальных точек
- Act -- множество действий
- -- отношение перехода (Cond(Vp) -- это фактически страж оператора )
- Effect -- функция эффекта
- -- начальное условие
Получение TS из PG: раскрутка графа
- Состояние в TS -- это точка программы и текущая подстановка
- Начальное состояние -- исходная точка, удовлетворяющая начальному условию
- Атомарные высказывания в TS:
- находимся в точке программы l
- значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
- Состояния размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
- Если в графе программы есть дуга из l в l' со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния в состояние по действию a.
Системы переходов графов программ Операционная семантика -- строгое описание того как из графа программы получить ее систему переходов. Описывается это все при помощи правил вывода. TS(PG) -- система переходов графа программы задается сигнатурой
- (декартово произведение точек программы на всевозможные подстановки)
- с соответствующим правилом вывода
- Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы:
- Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы:
- Состояния вида размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
Пример: Лекция 4, слайд 16
Параллелизм. Чередование систем переходов.
Лекция 4, слайды 21-24
- Действия независимых процессов чередуются.
- Порядок выполнения процессов не известен.
Чередование:
- эффект от параллельного выполнения независимых действий a и b равен эффекту от их последовательного выполнения в произвольном порядке:
-
- ||| -- оператор чередования
- ; -- оператор последовательного выполнения
- + -- оператор недетерминированного выбора
-
Пример: Лекция 4, слайд 23
Чередование систем переходов
Пусть
Тогда чередование этих систем , где
- оператор определяется как
Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.
Лекция 4, слайды 25—28
Для графов программ PG1 (над V1) и PG2 (над V2) без разделяемых переменных (т. е. ):
- формула достоверно описывает параллельную композицию PG1 и PG2
- в случае с разделяемыми переменными это не так (см. лекцию 4, слайд 26).
Пусть
Граф над определяется так:
где отношение перехода определяется следующими правилами вывода:
- и
а если
Пример: лекция 4, слайд 28. В указанном примере
Параллелизм. Синхронный параллелизм. Рандеву.
- распределённые программы выполняются параллельно
- в распределённой программе нет разделяемых переменных
Передача сообщений в распределённых программах:
- cинхронная передача сообщений (рандеву)
- асинхронная передача сообщений (каналы)
Синхронный обмен сообщениями:
- Процессы вместе выполняют синхронизированные действия
- Взаимодействие процессов - одновременно
Рандеву
- -- набор синхронизированных действий.
- действия из H должны быть синхронизированны
- действия не из H независимы и могут чередоваться
Тогда , где
- определяется как:
- интерливинг для и
- рандеву для
Пример рандеву: Лекция 4, слайд 32
Синхронный параллелизм
Тогда , где
- определяется как:
Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.
Лекция 4. Слайды 36-39, 43-46
- -- Процессы взаимодействуют с помощью каналов, представляющих собой FIFO буфера
- dom(c) -- Каналы типизированы по передаваемым сообщениям
- cap(c) -- ёмкость канала. если cap(c) = 0, то взаимодействие сводится к рандеву
- действия по обмену сообщениями:
- c!v -- запись v в конец канала c. Выполняется только если буфер не полон ( < cap(c))
- c?x -- чтение в x из начала канала c. Выполняется только если буфер не пуст ( > cap(c))
- формально
Системы с каналами.
- Граф программы PG над (Var,Chan) задаётся , где
- Система с каналами CS над задаётся как , где PGi — граф программы над (Vari,Chan)
При асинхронной передаче сообщений (при cap(c) > 0):
- процесс Pi может выполнить , только если в c хранится меньше cap(c) сообщений;
- процесс Pj может выполнить , только если c не пуст, после чего первый элемент v извлекается из c и присваивается x (атомарно).
Оценка ξ значения канала c — это отображение канала на последовательность значений , такое что длина последовательности не превосходит ёмкости канала , и при этом означает, что v1 — верхнее сообщение в буфере.
- Кто понимает смысл этой хренотени, опишите, плз. Overrider 18:28, 22 мая 2009 (UTC)
Исходная оценка
Операционная семантика: лекция 4, слайды 44—46
Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.
Представим трассу в форме интерпретации I:
- - множество натуральных чисел
- - отношение порядка на
- (для каждого порядкового номера говорит истенен или ложен заданный на нем предикат)
Рассмотрим трассы tr и tr' такие, что
Будем говорить, что трасса tr' является абстракцией трассы tr (), если
- такое, что
- α - неубывающая функция:
Пример абстракции трассы: Лекция 2, слайд 53
Необходимое условие корректности модели - , где
- P - система
- M - модель этой системы
При этом, если - некоторое свойство системы, то выполняется тогда и только тогда, когда верно условие корректности модели.
Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.
Абстракция системы переходов -- картинка на 4 слайде 3-й лекции.
Достаточное условие корректности LTS модели.
Пусть у нас имеются две системы переходов, TS1 и TS2 -- для системы и модели соответственно:
Достаточное условие корректности:
- Алфавит предикатов модели включен в алафвит предикатов системы:
- Задано отображение . На отображение накладываются следующие условия:
- Оно преобразует начальное состояние системы в начальное состояние модели:
- Каждому переходу из системы должен соответствовать переход в модели:
- Метки на состояниях модели должны состоять только из предикатов модели:
Необходимое условие адекватности модели свойствам правильности: алфавит предикатов свойств правильности включен в алфавит предикатов модели — . Условие не является достаточным (см. примеры, лекция 3, слайды 4—5).
Абстракция. Абстракция графов программ. Отношение слабой симуляции.
Лекция 10, слайды 8 - 11
Программа PG' корректно моделирует программу PG тогда и только тогда, когда система переходов TS(PG') корректно моделирует систему переходов TS(PG).
Будем говорить, что PG' моделирует PG, если
- в PG' присутствуют переменные, соответствующие наблюдаемым переменным PG
- все действия PG, влияющие на наблюдаемые переменные, отражены в модели (наблюдаемые операторы)
- модель корректно воспроизводит возможные последовательности изменения значений наблюдаемых переменных, присутствующих в PG
Отношение слабой симуляции не сохраняет количество шагов между состояниями. В связи с этим, не сохраняются свойства, не инвариантные к прореживанию (LTL: оператор neXt).
Логика LTL, автоматы Бюхи
Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств.
Лекция 5, слайды 2-14.
Требования правильности — утверждения о возможных и невозможных вариантах выполнения программы.
Двойственность :
- если какое-то утверждение невозможно, то обратное — неизбежно
- если какое-то утверждение неизбежно, то обратное — невозможно
- при помощи логики от одного можно переходить к другому при помощи отрицания
Способы описания свойств правильности:
- свойства достижимых состояний (свойства безопасности)
- свойства последовательности состояний (свойства живучести)
- в Promela:
- свойства состояний
- asserts:
- локальные ассерты процессов
- инварианты системы процессов
- метки терминальных состояний
- задаём допустимые точки останова прочесса
- asserts:
- свойства последовательностей состояний
- метки прогресса — чтобы найти циклы бездействия
- утверждения о невозможности (never claims) — например, LTL формулы
- трассовые ассерты — используются для описания правильных последовательностей выполнения операторов отправки и приема сообщения
- свойства состояний
Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств.
Типы свойств:
- свойства безопасности
- ничего плохого никогда не произойдет
- пример: инвариант системы (например, x всегда меньше y);
- задача верификатора -- найти те вычисления, которые ведут к нарушению безопасности.
- свойства живучести
- рано или поздно произойдет что-то хорошее
- пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
- задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.
ps. автор терминов – Лесли Лампорт; см. Лекция 5, слайд 4.
Автоматы Бюхи. Конечные автоматы. Проход автомата. Язык автомата.
Лекция 6, слайды 8 - 15
Конечный автомат описывается сигнатурой: , где
- S -- множество сотояний
- -- множество начальных состояний
- L -- конечное множество меток
- -- множество терминальных состояний
- -- отношение перехода на состояниях
Детерминизм и недетерминизм
Конечный автомат называется детерминированным, если по метке и исходному состоянию можно однозначно определить целевое состояние:
В противном случае автомат называется недетерминированным.
Проходом a конечного автомата называется такое упорядоченное и, возможно, бесконечное множеств переходов из T:
Допускающим проходом конечного автомата A называется конечный проход a, финальный переход которого
(sn − 1,ln − 1,sn) ведёт в терминальное состояние.
Языком автомата A называется множество слов в алфавите A.L, соответствующих допускающим проходам автомата А
Автоматы Бюхи. Омега-допускание. Расширение автоматов Бюхи.
Лекция 6, слайды 19-20
Для любого бесконечного прохода σ конечного автомата А можно выделить два последовательных отрезка проходов:
- σ + -- конечный отрезок прохода σ, включающий в себя множество состояний, встречающихся конечное число раз
- σω -- бесконечный хвост прохода σ, включающий в себя множество состояний, встречающихся бесконечное число раз
Допускающий проход по Бюхи (ω-допускание) конечного автомата A называется такой бесконечный проход, в котором по крайней мере одно терминальное состояние встречается бесконечное число раз:
Расширение автоматов Бюхи.
- добавляем алфавит автомата меткой
- все конечные проходы расширяем до бесконечности меткой
Примечание. При помощи автоматов Бюхи удобно проверять свойства живучести.
Логика LTL. Синтаксис LTL. Семантика выполнимости формул. Сильный и слабый until.
Лекция 6, слайды 30 - 35
Особенности LTL:
- может использоваться для описания свойств как живучести, так и безопасности
- описывает свойства, которым должны удовлетворять линейные последовательности наблюдаемых состояний - трассы
- семантика LTL определена на бесконечных автоматах Бюхи. Для конечных проходов необходимо использовать расширение автомата.
Формула в LTL f::=
- p, q, ... — свойства состояний, включая true и false
- (f) — группировка при помощи скобок
- — унарные операторы
- — бинарные операторы
Операторы в LTL
- унарные
- ([]) — всегда в будущем, т.е.
- (<>) — в конце концов, т.е.
- X (X) — в следующем состоянии, т.е.
- (!) — логическое отрицание
- бинарные
- (&&) — логическое И
- (||) — логическое ИЛИ
- (->) — логическая импликация
- (<->) — логическая эквивалентность
- U (U) — до тех пор, пока (until)
Сильный Until:
- всегда e, до тех пор, пока не f, при этом f обязательно должно наступить
Слабый Until:
- всегда e, до тех пор, пока не f, при этом не факт, что f наступает (тогда всегда e)
Выполнимость формул:
- Задаётся последовательность состояний прохода σ
- (Внимание!! это слишком смахивает на бред, который должен быть интуитивно понятен. Если кто может - распишите подробнее выполнимость!! может быть, здесь имеется в виду что в каждом состоянии определена формула, или что если есть формула, то она определена в каком-то состоянии. вообщем, wierd).
Логика LTL. Основные типы свойств LTL. Цикличность, стабильность, инвариант, гарантия, отклик, приоритет, корреляция.
Лекция 6, Слайды 38-39
Формула | Описание | Тип | |
---|---|---|---|
всегда p | инвариант | ||
рано или поздно p | гарантия | ||
если p, то рано или поздно q | отклик | ||
если p то затем постоянно q до тех пор,
пока рано или поздно не наступит r | приоритет | ||
всегда рано или позндно будет p | цикличность (прогресс) | ||
рано или позндно всегда будет p | стабильность (бездействие) | ||
если рано или поздно p, то рано или поздно q | корреляция |
Логика LTL. Эквивалентные преобразования формул LTL.
Лекция 6, Слайды 40
|
|
Логика LTL. Оператор neXt. Свойства, инвариантные к прореживанию.
Лекция 7, слайды 22-25
Оператор X нужно использовать аккуратно:
- с его помощью делается утверждение о выполнимости формулы на непосредственных потомках текущего состояния,
- в распределённых системах значение оператора X неочевидно,
- поскольку алгоритм планирования процессов неизвестен, не стоит формулировать спецификацию в предположении о том,
какое состояние будет следующим,
- стоит ограничиться предположением о справедливости планирования.
Свойства, инвариантные к прореживанию
- Пусть f – трасса некоторого вычисления над пропозициональными формулами P,
- по трассе можно определить, выполняется ли на ней темпоральная формула,
- трассу можно записать в форме:
- -- где значения пропозициональных формул на каждом интервале совпадают.
- Обозначим E(f) набор всех трасс, отличающихся лишь значениями n1,n2,n3 (т.е. длиной интервалов).
- E(f) называется расширением прореживания f.
- Свойство f, инвариантное к прореживанию, либо истинно для всех трасс из E(ψ), либо ни для одной из них:
- истинность такого свойства не зависит от длины трассы, а только от порядка, в котором пропозициональные формулы меняют свои значения;
- Теорема: все формулы LTL без оператора X инвариантны к прореживанию.
- в рамках LTL без X можно описать все свойства, инвариантные к прореживанию
Логика LTL. Проверка выполнимости формул LTL при помощи автоматов Бюхи. Проверка LTL-формул в Spin.
Лекция 7, слайды 26-40
Связь LTL с автоматами Бюхи
- Удобно проверять допустимость трасс для некоторого автомата Бюхи;
- Удобно описывать свойства правильности при помощи темпоральных формул;
- Для всякой LTL-формулы f существует автомат Бюхи, который допускает те и только те прогоны, которым соответствуют трассы, на которых выполнима f;
Переход от LTL к автоматам
- Привести свойство правильности LTL к форме never языка Promela достаточно просто: нужно построить отрицание LTL формулы и поместить его в тело never:
- f выполняется на всех вычислениях <=>
- !f не выполняется ни на одном вычислении <=>
- автомат never {!f} не допускает ни одного прогона, полученного в результате синхронного выполнения с системой
Логика LTL. Выразительная мощность LTL. Логики LTL + существование, CTL* и CTL. Сравнение выразительной мощности.
При помощи конструкции never можно описать любой ω-регулярный автомат над словами
Выразительная мощность LTL
по сравнению с конструкциями never
- LTL описывает подмножество этого языка:
- всё, выразимое на LTL, может быть описано при помощи never,
- при помощи never можно описать свойства, не выразимые на LTL
- Добавление одного квантора существования над одним пропозициональным символом расширяет выразительные способности LTL до всех омега-регулярных автоматов над словами.
(p) может быть истинным после выполнения системой чётного количества шагов, но никогда не истинно после нечётного.
t(t && [](t -> X!t) && [](!t -> Xt) && [](!t -> !p))
LTL-формула описывает свойство, которое должно выполняться на всех вычислениях, начинающихся из исходного остояния системы
Логика СTL*
- Логика ветвящегося времени:
- использует кванторы ∀ и ∃ для обозначения трасс, на которых может выполняться свойство
- использует F вместо <> и G вместо []
Логика СTL
Логика CTL – фрагмент логики CTL*, в котором кванторы могут встречаться только парами, причём в паре должны обязательно находиться один временной и один пространственный кванторы. Например: AG EF(p), A(p U q).
Выразительные возможности 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: из любого состояния
система может перейти в нормальное
Верификация программ на моделях
Задача проверки правильности программ. Валидация. Верификация. Системы с повышенными требованиями к надёжности. Реактивные программы. Параллельные программы. Особенности верификации таких программ.
Валидация - исследование и обоснование того, что спецификация ПО и само ПО через реализованную в нём функциональность удовлетворяет ребованиям пользователей.
Верификация - исследование и обоснование того, что программа соответствует своей спецификации.
Верификация в общем случае алгоритмически неразрешима.
Методы верификации:
- "Полное" тестирование (Лекция 1, слайды 14-22)
- Имитационное моделирование (вики)
- Доказательство теорем (слайды 27-29)
- Статический анализ (слайды 30-33)
- Верификация на моделях (слайды 34-38)
Типы программ:
- Традиционные программы
- завершимость
- спецификация включает в себя описание входа/выхода программы
- число состояний зависит от входных данных и переменных
- Реактивные программы
- работают в бесконечном цикле
- взаимодействуют с окружением
- спецификация представляет собой пары стимул/реакция
- Параллельные программы
- совместная работа нескольких компонент
- невоспроизводимость тестов
- ограниченные возможности по наблюдению
Подходы к верификации программ. Тестирование и имитационное моделирование. Область применения, плюсы и минусы. Проблема полноты тестового покрытия.
«Тестирование может показать присутствие ошибок, но не может показать их отсутствия» © Дейкстра.
Обоснование полноты тестового покрытия:
- метод «чёрного ящика» (ЧЯ) — полное покрытие входных данных,
- метод «прозрачного ящика» (ПЯ) — полное покрытие кода программы.
Плюсы применения тестирования:
- проверяется та программа, которая будет использоваться,
- не требуется знание/использование дополнительных инструментальных средств,
- удобная локализация ошибки.
Минусы применения тестирования:
- не всегда есть условия для тестирования системы,
- проблема с воспроизводимостью тестов (частичное решение — имитационное моделирование).
Проблема полноты тестового покрытия
- Чёрный ящик:
- для последовательных программ сложно перебрать все входные данные,
- для параллельных программ — очень сложно,
- для динамических структур данных, взаимодействия с окружением — невозможно.
- Прозрачный ящик:
- большой размер покрытия,
- часто невозможно построить 100% покрытие,
- полное покрытие не гарантирует отсутствия ошибок.
Итоги:
- Полный перебор входных данных — невозможен.
- Полнота покрытия кода не гарантирует правильности.
- Ошибка — ошибочное вычисление системы.
- Полнота в терминах возможных вычислений — хороший критерий.
Подходы к верификации программ. Доказательство теорем. Область применения, плюсы и минусы.
Основные пункты:
- система и её свойста - формулы
- задан набор аксиом и правил вывода
- строится доказательство свойства-теоремы
- таким образом, производится качественный анализ системы
Пример: Лекция 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. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости.
Свойства последовательностей состояний
- метки прогресса (чтобы найти циклы бездействия)
- утверждения о невозможности (never claims)
- например, определяются LTL-формулами
- трассовые ассерты
Циклы бездействия. Мы хотим найти потенциально бесконечные циклы, не выполняющие никакой полезной работы. Помечаем меткой progress полезные операторы. Если найдется цикл, работающий потенциально бесконечно и не проходящий по метке progress, верификатор выдаст ошибку.
Ограничения справедливости. Существует два основных варианта справедливости:
- слабая справедливость:
- если оператор выполним бесконечно долго, то он в конце концов будет выполнен
- сильная справедливость:
- если оператор выполним бесконечно часто, то он в конце концов будет выполнен.
Справедливость применима как к внутреннему, так и к внешнему недетерминизму. Использование сильной справедливости – существенно дороже слабой
Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты.
never claims (утверждения о невозможности):
- выполняются синхронно с моделью
- если достигнут конец, то – ошибка
- состоят из выражений и конструкция задания потока управления
- фактически, описывают распознающий автомат.
Конструкция never
- может быть как детерминированной, так и нет;
- содержит только выражения без побочных эффектов (соотв. булевым высказываниям на состояниях);
- используются для описания неправильного поведения системы;
- прерывается при блокировании:
- блокируется => наблюдаемое поведение не соответствует описанному,
- паузы в выполнении тела never должны быть явно заданы как бесконечные циклы;
- never нарушается, если:
- достигнута закрывающая скобка,
- завершена конструкция accept (допускающий цикл);
- бездействие может быть описано как конструкция never или её часть (для цикла бездействия есть тело never по умолчанию).
Видимость
- все конструкции never – глобальны;
- тем самым, в них можно ссылаться на
- глобальные переменные,
- каналы сообщений,
- точки описания процессов (метки),
- предопределённые глобальные переменные,
- но не локальные переменные процессов;
Ассерты на трассы Используются для описания выполнения правильных и неправильных последовательностей операторов send и recieve. Ассерт notrace - утверждает, что описанный шаблон поведения невозможен.
Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin.
- Свойство выполняется на модели, если оно выполняется на всех трассах.
- Свойство нарушается на модели, если нарушается хотя бы на одной из трасс.
- Принцип верификации нарушения свойств - проще проверять нарушение свойства, чем выполнение свойства.
- Достаточно найти один контрпример
- Нарушение свойства описывается при помощи конструкции never – автомата, распознающего неправильное поведение
- Автоматы Бюхи
- Свойства на последовательностях состояний удобно описывать при помощи темпоральной логики
- Логика LTL
- Связь LTL с автоматами Бюхи
- При помощи автомата Бюхи удобно проверять допустимость трасс.
- При помощи темпоральных формул удобно описывать свойства правильности.
- Для всякой LTL-формулы f существует автомат Бюхи, который допускает те и только те прогоны, которым соответствуют трассы, на которых выполнима f
- Переход от LTL к автоматам
- 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 - описание свойств
- SPIN – Simple Promela Interpreter
Конечность моделей на 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
- задают элементарные преобразования состояний,
- размечают дуги в системе переходов соответствующего процесса,
- их немного – всего 6 типов:
- выражение
- присваивание
- печать
- проверка свойства безопасности (assert)
- отправка сообщения
- прием сообщения
- оператор может быть:
- выполнимым: может быть выполнен,
- заблокированным: (пока что) не может быть выполнен,
- выполнимость может зависеть от глобального состояния.
Оператор-выражение
- выполним только если выражение не равно 0 (истинно):
- 2 < 3 – выполним всегда,
- x < 27 – выполним только если значение x < 27,
- 3 + х – выполним только если x != -3.
Оператор-присваивание
- всегда безусловно выполним, меняет значение только одной переменной, расположенной слева от “=”.
Язык Promela. Основные операторы языка Promela. Отладочная печать, операторы skip, true, run, assert.
Основные операторы языка Promela
- присваивание: x++, x--, x = x + 1, x = run P();
- выражение: (x), (1), run P(), skip, true, else, timeout;
- печать: printf(“x = %d\n”, x);
- ассерт: assert(1+1 == 2), assert(false);
- отправка сообщения: q!m;
- приём сообщения: q?m;
Отладочная печать
- оператор печати printf, всегда безусловно выполним, на состояние не влияет
Псевдо-операторы
- skip: всегда выполним, без эффекта, эквивалент выражения (1),
- true: всегда выполним, без эффекта, эквивалент выражения (1),
- run: 0 если при создании процесса превышен лимит, pid в противном случае.
Оператор assert
- всегда выполнимо, не влияет на состояние системы,
- Spin сообщает об ошибке, если значение выражения равно 0 (false),
- используется для проверки свойств безопасности.
Язык Promela. Чередование (интерливинг) операторов. Внешний и внутренний недетерминизм. Управление выполнимостью операторов.
Чередование (интерливинг) операторов
- процессы выполняются параллельно и асинхронно, между двумя последовательными операторами одного процесса может быть сколь угодно длинная пауза,
- произвольная диспетчеризация процессов,
- выполнение операторов разных процессов происходит в произвольном порядке, основные операторы выполняются атомарно,
- в теле одного процесса также допускается недетерминированное ветвление
Внешний и внутренний недетерминизм
- два уровня недетерминизма:
- внешний (выбор процесса),
- внутренний (выбор действия в процессе).
Управление выполнимостью операторов Основной инструмент управления выполнимостью операторов в Promela – выражения (expressions). (a + b) -> c++; Так же существуют управляющие конструкции if..fi и do..od
Язык Promela. Задание потока управления последовательного процесса. Управляющие конструкции if, do. Организация внутреннего недетерминизма.
Задание потока управления последовательного процесса 5 способов задать поток управления:
- последовательная композиция(“;”), метки, goto,
- структуризация (макросы и inline),
- атомарные последовательности (atomic, d_step),
- недетерминированный выбор и итерации (if..fi, do..od),
- escape-последовательности ({...}unless{...}).
Специальные выражения и переменные
- else – true, если ни один оператор процесса не выполним,
- timeout – true, если ни один оператор модели не выполним,
- _ – переменная, доступная только по записи, значение не сохраняет,
- _pid – минимальный доступный pid,
- _nr_pr – число активных процессов.
Язык Promela. Каналы сообщений. Операторы отправки и приёма сообщений. Тип mtype. синхронная и асинхронная передача сообщений.
Каналы сообщений
- сообщения передаются через каналы (очереди/буфера ограниченного объёма)
- каналы бывают двух типов:
- буферизованные (асинхронные),
- небуферизованные (синхронные, рандеву);
chan x = [10] of {int, short, bit};
Операторы отправки и приема сообщений Отправка: ch!expr1,...exprn
- значения expri соответствуют типам в объявлении канала;
- выполнимо, если заданный канал не полон;
Приём: ch?const1 или var1,...constn или varn
- значения vari становятся равны соотв. значениям полей сообщения;
- значения consti ограничивают допустимые значения полей;
- выполнимо, если заданный канал не пуст и первое сообщение в канале соответствует всем константным значениям в операторе приёма сообщения;
Объявление mtype
- способ определить символьные константы (до 255)
Объявление mtype: mtype = {foo, bar}; mtype = {ack, msg, err, interrupt};
Объявление переменных типа mtype: mtype a; mtype b = foo;
Cинхронная и асинхронная передача сообщений
- Асинхронная передача
- асинхронные сообщения буферизуются для последующего приёма, пока канал не полон,
- отправитель блокируется, когда канал полон,
- получатель блокируется, когда канал пуст.
- Синхронная передача
- ёмкость канала равна 0 - chan ch = [0] of {mtype};
- передача сообщений методом “рандеву”,
- не хранит сообщения,
- отправитель блокируется в ожидании получателя, и наоборот,
- отправка и приём выполняются атомарно.
Язык Promela. Каналы сообщений. Вспомогательные операции с каналами сообщений.
Другие операции с каналами
- len(q) – возвращает число сообщений в канале,
- empty(q) – возвращает true, если q пуст,
- full(q) – возвращает true, если q полон,
- nempty(q) – вместо !empty(q) (в целях оптимизации),
- nfull(q) – вместо !full(q) (в целях оптимизации).
- q?[n,m,p]
- булевое выражение без побочных эффектов,
- равно true только когда q?n,m,p выполнимо, однако не влияет на значения n,m,p и не меняет собержимое канала q;
- q?<n,m,p>
- выполнимо тогда же, когда и q?n,m,p; влияет на значения n,m,p так же, как q?n,m,p, однако не меняет содержимое q;
- q?n(m,p)
- вариант записи оператора приёма сообщения (т.е. q?n,m,p),
- может использоваться для отделения переменной от констант
- q!!n,m,p – аналогично q!n,m,p, но сообщение n,m,p помещается в канал q сразу за первым сообщением, меньшим n,m,p;
- q??n,m,p – аналогично q?n,m,p, но из канала может быть выбрано любое сообщение (не обязательно первое).
Имя канала может быть локальным или глобальным, но канал сам по себе – всегда глобальный объект
Язык Promela. Основные типы данных. Область видимости данных.
Тип | Диапазон | Пример объявления | |
---|---|---|---|
bit | 0..1 | bit turn = 1; | |
bool | false..true | bool flag = true; | |
byte | 0..255 | byte cnt; | |
chan | 1..255 | chan q; | |
mtype | 1..255 | mtype msg; | |
pid | 1..255 | pid p; | |
short | -215..215-1 | short s = 100; | |
int | -231..231-1 | int x = 1; | |
unsigned | 0..2n-1 | unsigned u : 3; // 3 бита [?] |
- по умолчанию все объекты (и локальные и глобальные) инициализируются нулём;
- все переменные должны быть объявлены до первого использования;
- переменная может быть объявлена где угодно.
'Одномерные массивы'
byte a[27]; bit flags[4] = 1;
- все элементы массива инициализируются одним значением,
- индексы нумеруются с 0;
'Пользовательские типы данных'
typedef record { short f1; byte f2 = 4; } record rr; rr.f1 = 5;
Только два уровня видимости
- глобальный (данные видны всем активным процессам),
- локальный (данные видны только одному процессу)
- подобластей (напр. для блоков) нет,
- локальная переменная видна везде в теле процесса;