ВПнМ/Теормин
Материал из eSyr's wiki.
Лекция 1
Валидация - исследование и обоснование того, что спецификация ПО и само ПО через реализованную в нём функциональность удовлетворяет ребованиям пользователей.
Верификация - исследование и обоснование того, что программа соответствует своей спецификации.
Верификация в общем случае алгоритмически неразрешима.
Методы верификации:
- "Полное" тестирование (слайды 14-22)
- Имитационное моделирование
- Доказательство теорем (27-29)
- Статический анализ (30-33)
- Верификация на моделях (34-38)
Моделирование и абстракция
Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.
Схема верификации на моделях (Лекция 2, слайд 3)
Состояние программы - совокупность значений переменных и управления, связанных с некоторой моделью программы.
Модель - упрощённое описание реальности, выполненное с определенной целью.
- с каждым объектом может быть связано несколько моделей
- каждая модель отражает свой аспект реальности
Аспекты модели:
- простота - модель должна быть проще, чем реальность
- корректность - не расходиться с реальностью
- адекватность - соответствовать решаемой задаче
Построение модели
- формализация требований (постановка задачи моделирования)
- выбор языка моделирования
- абстракция системы до модели с учётом требований
Моделирование программ. Размеченные системы переходов. Детерминизм и недетерминизм. Вычисления и трассы. Свойства линейного времени. Выполнимость свойства на трассе.
Размеченная система переходов (LTS)
- S - множество состояний
- Act - множество действий
- τ - невидимое действие
- - тотальное отношение переходов
- - начальное состояние
- AP - множество атомарных высказываний
- - функция разметки
S, Act - конечные или счётные множества
Пример LTS: Лекция 2, слайд 40-41
Прямые потомки
- - такие состояния s', которые непосредственно вытекают из s через переход a
- - все возможные состояния s', которые непосредственно вытекают из s
Система детерменирована:
- по действиям тогда и только тогда, когда
- по атомарным высказываниям
- ( количество одинаково размеченных потомков не больше одного )
Недетерменизм - это фича! Полезен для:
- моделирования параллельного выполнения в режиме чередования (интерливинга)
- позволяет не указывать скорость выполнения процессов
- моделирования прототипа системы
- не ограничивает реализацию заданным порядком выполнения операторов
- построения абстракции реальной системы
- модель может быть построена по неполной информации
Вычисления
- Конечный фрагмент вычисления σ системы переходов TS называется конечная последовательность чередующихся состояний и действий
- Бесконечный (максимальный) фрагмент вычисления ρ -
- Начальный фрагмент вычисления - фрагмент вычисления, для которого
- Вычисление - начальный максимальный фрагмент вычисления
Достижимое состояние (из начального) в системе переходов TS - такое состояние , для которого существует конечный фрагмент вычисления
Rich(TS) - множество всех достижимых состояний в TS
Трасса
Свойства линейного времени
- Свойство определяет набор допустимых трасс:
- Система переходов TS удовлетворяет свойству линейного времени
Моделирование программ. Графы программ. Статическая и операционная семантика.
Граф программы – формальное описание текста программы.
- Dp -- единый абстрактный домен данных.
- P -- программа.
- Vp -- множество переменных программы(Var).
-
- -- каждая переменная принадлежит какому-либо домену
- n -- подстановка.
- Cond(Vp) -- Набор булевых условий над Vp
- формулы пропозициональной логики
- условия на переменные
- Эффект операторов:
Граф программы:
- Loc -- множество точек
- -- множество начальных точек
- Act -- множество действий
- -- отношение перехода (Cond(Vp) -- это фактически страж оператора )
- Effect -- функция эффекта
- -- начальное условие
- Множество начальных состояний системы переходов описывается как множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы:
Невозможно разобрать выражение (неизвестная ошибка): I={\langle l , n \rangle ∣ l \in Loc_0 , n |= g_0 }
- Множество атомарных высказываний -- это объединение множества точек программы и всевозможных булевых высказываний над переменными программы:
- Состояния вида <l,n> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
L(\langle l , n \rangle)= {l }\cap{g \in Cond(V_P)| n |= g }.
Получение TS из PG: раскрутка графа
- Состояние в TS -- это точка программы и текущая подстановка
- Начальное состояние -- исходная точка, удовлетворяющая начальному условию
- Атомарные высказывания в TS:
- находимся в точке программы l
- значение переменной x принадлежит некоторому множеству и это множество является подмножеством множеств значений этой переменной.
- Состояния < l,n > размечаются высказыванием о том, что мы находимся в точке программы l и всеми высказываниями, истинными в n
- Если в графе программы есть дуга из l в l' со стражем g и действием a и в некоторой подстановке n выполняется страж g, то в системе переходов, которая соответствует этой программе будет присутствовать дуга из состояния < l,n > в состояние < l',Effect(a,n) > по действию a.
Системы переходов графов программ Операционная семантика -- строгое описание того как из графа программы получить ее систему переходов. Описывается это все при помощи правил вывода. TS(PG) -- система переходов графа программы задается сигнатурой
- (декартово произведение точек программы на всевозможные подстановки)
- с соответствующим правилом вывода
- Множество начальных состояний системы переходов -- множество состояний, в которых точка программы принадлежит начальным точкам, а на подстановках выполняется начальное условие графа программы
- Множество атомарных высказываний -- объединение множества точек программы и всевозможных булевых высказываний над переменными.
- Состояние <l,n> размечается точкой l, в которой находится программа и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке.
Пример: Лекция 4, слайд 16
Параллелизм. Чередование систем переходов.
Параллелизм. Чередование графов программ. Случаи без разделяемых переменных и с разделяемыми переменными.
Параллелизм. Синхронный параллелизм. Рандеву.
- распределённые программы выполняются параллельно
- в распределённой программе нет разделяемых переменных
Передача сообщений в распределённых программах:
- cинхронная передача сообщений (рандеву)
- асинхронная передача сообщений (кналы)
Синхронный обмен сообщенийями:
- Процессы вместе выполняют синхронизированные действия
- Взаимодействие процессов - одновременно
Рандеву
Тогда , где
- определяется как:
- интерливинг для и
- рандеву для
Пример рандеву: Лекция 4, слайд 32
Синхронный параллелизм
Тогда , где
- определяется как:
Параллелизм. Асинхронный параллелизм. Системы с каналами. Операционная семантика.
Абстракция. Абстракция трасс. Абстракция системы переходов. Необходимое и достаточное условие корректности LTS модели.
Представим трассу в форме интерпретации I:
- N - множество натуральных чисел
- - отношение порядка на N
Рассмотрим трассы tr и tr' такие, что
Будем говорить, что трасса tr' является абстракцией трассы tr, если
- такое, что
Пример абстракции трассы: Лекция 2, слайд 53
Необходимое условие корректности модели - , где
- P - система
- M - модель этой системы
При этом, если - некоторое свойство системы, то выполняется тогда и только тогда, когда верно условие корректности модели.
Абстракция. Абстракция системы переходов. Достаточное условие корректности LTS модели. Адекватность LTS модели.
Абстракция системы переходов -- картинка на 4 слайде 3-й лекции.
Достаточное условие корректности LTS модели.
Пусть у нас имеются две системы переходов, TS1 и TS2 -- для системы и модели соответственно:
Достаточное условие корректности:
- Алфавит предикатов модели включен в алафвит предикатов системы:
- Задано отображение . На отображение накладываются следующие условия:
- Оно преобразует начальное состояние системы в начальное состояние модели:
- Каждому переходу из системы должен соответствовать переход в модели:
- Метки на состояниях модели должны состоять только из предикатов модели:
Достаточное условие адекватности модели свойствам правильность :
Алфавит предикатов свойств правильности включен в алфавит предикатов модели.
Абстракция. Абстракция графов программ. Отношение слабой симуляции.
Логика LTL, автоматы Бюхи
Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств.
Требования правильности -- утверждения о возможных и невозможных вариантах выполнения программы.
Двойственность :
- если какое-то утверждение невозможно, то обратное -- неизбежно
- если какое-то утверждение неизбежно, то обратное -- невозможно
- при помощи логики от одного можно переходить к другому при помощи отрицания
Схема верификации на модели: Лекция 2, слайд 3
Примеры классов свойств:
- Стандартные
- Специфичные для конкретного приложения
- требования справедливости
- корректная завершаемость
- причинно-следственный и темпоральный порядок состояний системы
Способы описания свойств правильности:
- свойства достижимых состояний (свойства безопасности)
- свойства последовательности состояний (свойства живучести)
- в Promela:
- свойства состояний
- asserts
- локальные ассерты процессов
- инварианты системы процессов
- метки терминальных состояний
- задаём допустимые точки останова прочесса
- asserts
- свойства последовательностей состояний
- метки прогресса - чтобы найти циклы бездействия
- утверждения о невозможности (never claims) - например, LTL формулы
- трассовые ассерты
- свойства состояний
Свойства правильности. Свойства безопасности и живучести. Проверка таких свойств. Примеры свойств.
Типы свойств:
- свойства безопасности
- ничего плохого никогда не произойдет
- пример: инвариант системы (например, x всегда меньше y);
- задача верификатора -- найти те вычисления, которые ведут к нарушению безопасности.
- свойства живучести
- рано или поздно произойдет что-то хорошее
- пример: “отзывчивость” (например, если отправлен запрос, то рано или поздно будет сгенерирован ответ)
- задача верификатора – найти вычисления, в которых это “хорошее” может откладываться до бесконечности.