ВПнМ/Теормин
Материал из eSyr's wiki.
(→Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты.) |
(→Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты.) |
||
Строка 427: | Строка 427: | ||
** предопределённые глобальные переменные, | ** предопределённые глобальные переменные, | ||
** но не локальные переменные процессов; | ** но не локальные переменные процессов; | ||
+ | |||
+ | '''Ассерты на трассы''' | ||
+ | Используются для описания выполнения прывильных и неправильных последовательностей операторов send и recieve | ||
=== Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin. === | === Верификация при помощи Spin. Принцип верификации нарушения свойств. Контрпримеры. Процесс верификации при помощи Spin. Использование LTL в Spin. === |
Версия 16:46, 20 мая 2009
Моделирование и абстракция
Моделирование программ. Понятие состояния. Потенциальные и достижимые состояния. Требования к модели. Процесс построения модели.
Схема верификации на моделях (Лекция 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 -- функция эффекта
- -- начальное условие
Получение 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> размечаются высказываниям о точке программы, в которой мы находимся и всеми высказываниями из множества всевозможных высказываний, которые верны в этой подстановке:
Пример: Лекция 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, автоматы Бюхи
Свойства правильности. Формулирование требований правильности программы. Двойственность. Типы свойств.
Требования правильности -- утверждения о возможных и невозможных вариантах выполнения программы.
Двойственность :
- если какое-то утверждение невозможно, то обратное -- неизбежно
- если какое-то утверждение неизбежно, то обратное -- невозможно
- при помощи логики от одного можно переходить к другому при помощи отрицания
Способы описания свойств правильности:
- свойства достижимых состояний (свойства безопасности)
- свойства последовательности состояний (свойства живучести)
- в Promela:
- свойства состояний
- asserts
- локальные ассерты процессов
- инварианты системы процессов
- метки терминальных состояний
- задаём допустимые точки останова прочесса
- 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
Особенности:
- анализ исходного текста без запуска программы
- в общем случае задача неразрешима
Достоинства:
- высокая скорость работы
- если ответ дан - ему можно верить
Недостатки:
- узкая область применения: компиляторы, анализ похожести кода, анализ безопасности
- ручная настройка при изменении применяемых свойств
Подходы к верификации программ. Верификация программ на моделях. Процесс верификации программы при помощи её модели. Область применения, плюсы и минусы.
Лекция 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
- задаём допустимые точки останова процесса
Верификация при помощи Spin. Задание свойств последовательностей состояний. Циклы бездействия. Ограничения справедливости.
Верификация при помощи Spin. Задание свойств последовательностей состояний. Утверждения о невозможности. Трассовые ассерты.
never claims (утверждения о невозможности):
- выполняются синхронно с моделью,
- если достигнут конец, то – ошибка,
- состоят из выражений и конструкция задания
потока управления
- фактически, описывают распознающий
автомат.
Конструкция never
- может быть как детерминированной, так и нет;
- содержит только выражения без побочных эффектов (соотв. булевым высказываниям на состояниях);
- используются для описания неправильного поведения системы;
- прерывается при блокировании:
- блокируется => наблюдаемое поведение не соответствует описанному,
- паузы в выполнении тела never должны быть явно заданы как бесконечные циклы;
- never нарушается, если:
- достигнута закрывающая скобка,
- завершена конструкция accept (допускающий цикл);
- бездействие может быть описано как конструкция never или её часть (для цикла бездействия есть тело never по умолчанию).
Видимость
- все конструкции never – глобальны;
- тем самым, в них можно ссылаться на
- глобальные переменные,
- каналы сообщений,
- точки описания процессов (метки),
- предопределённые глобальные переменные,
- но не локальные переменные процессов;
Ассерты на трассы Используются для описания выполнения прывильных и неправильных последовательностей операторов send и recieve