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

Общая информация
ЛекторЮ. Г. Карпов
Семестрвесна 2012
Дата начала18.03.2012
Количество пар3
Язык курсарусский
Видеоhttp://www.lektorium.tv/course/?id=22862
Анонсы
Встреча на сайте T&Phttp://theoryandpractice.ru/seminars/24730-verifikatsiya-parallelnykh-i-rasprede...
Анонс habrahabr.ruhttp://habrahabr.ru/events/418/
Аннотация Мини-курс посвящён изложению интересных новых результатов теоретической информатики, имеющих важное применение в верификации дискретных систем. Изложение материала доступно студентам младших курсов. Участникам семинара будут розданы (в ограниченном количестве) пособия, в которых излагается как теоретический материал семинара, так и практические рекомендации по использованию системы верификации SPIN. Для участия в практической работе необходимо принести с собой ноутбук с установленной системой SPIN: http://dcn.ftk.spbstu.ru/~belyaev/materials.rar
Лекции Подсказка: слайды, видеозапись и другие материалы лекции доступны со страницы лекции, попасть на которую можно, нажав на её название.

1. Model checking: новый метод верификации параллельных и распределенных программных систем
(18.03.2012 - 11:15 - 12:50)

Доклад представляет новые результаты теоретической информатики в области верификации параллельных и распределенных программ. Верификация — это процесс проверки выполнения требований к поведению программной системы на всех возможных траекториях ее вычислений. Недавний революционный прорыв в области верификации связан с методом Model checking (проверка модели), который состоит в том, что истинность формулы темпоральной логики, описывающей требование к поведению программы, проверяется на модели программы.

Темпоральная логика — это модальная логика, позволяющая формализовать утверждения о поведении дискретных систем, истинность которых зависит от времени. В докладе рассматривается логика ветвящегося времени CTL* и ее подклассы — логики CTL и LTL. Темпоральные логики оказались удобным формализмом для задания свойств корректного поведения дискретных систем, взаимодействующих друг с другом и окружением. Истинность либо ложность формул этих логик определяется на структуре Крипке — одном из формализмов, описывающих реактивные (реагирующие) систем с конечным числом состояний. Структура Крипке К называется “моделью” темпоральной формулы Ф, если Ф истинна на К. В докладе рассматриваются алгоритмы Model checking, т.е. алгоритмы проверки выполнимости темпоральных формул на структурах Крипке.

http://www.lektorium.tv/lecture/?id=13649
2. Введение в практическую верификацию. Система верификации SPIN (И.В.Шошмина, А.Б.Беляев)
(18.03.2012 - 13:00 - 14:35)

Доклад посвящен изложению методики использования программного средства Spin с входным языком Promela, которое широко применяется для верификации протоколов, параллельных программ и широкого класса дискретных систем. Пакет Spin – свободно распространяемое программное средство для формальной верификации систем. Spin разработан в Исследовательском Центре Bell Labs Джерардом Холзманном (Jerard Holzmann) для проверки компьютерных протоколов. Ежегодно проводятся конференции пользователей этого пакета, в литературе широко обсуждаются многочисленные примеры применения Spin для верификации сложных систем, в том числе бортовых программ, разрабатываемых NASA.

Spin осуществляет проверку не программ, а моделей программ, построенных на С-подобном входном языке пакета Spin, названном автором Promela – Protocol Meta Language. В свою очередь, аббревиатура Spin расшифровывается как Simple Promela Interpreter — простой интерпретатор программ на языке Promela. Конструкции языка Promela просты, они имеют ясную и четкую семантику, позволяющую перевести (оттранслировать) любую программу на этом языке в систему переходов, которая далее анализируется. Программы на языке Promela переводятся в Spin’е в структуру Крипке, и затем на ней проверяется выполнение заданных формул темпоральной логики линейного времени LTL, описывающих требования к программной системе.

http://www.lektorium.tv/lecture/?id=13650
3. Практическая работа по верификации параллельных программ и протоколов (И.В.Шошмина, А.Б.Беляев)
(18.03.2012 - 15:35 - 17:10)

В рамках семинара слушатели получат первоначальный практический опыт непосредственной работы с системой верификации SPIN, возможности и средства проверки корректности программ с помощью SPIN. Будет рассказано об особенностях установки и запуска системы SPIN на компьютерах слушателей, будут рассмотрены режимы работы системы, решены задачи с обнаружением тонких ошибок в параллельных программах и протоколах. Будут рассмотрены примеры использования системы SPIN и метода верификации Model checking не только для верификации параллельных программ, но и для решения логических задач, выявления атаки в криптографическом протоколе аутентификации Нидхема-Шредера и т.п.
Ваша оценка: Пусто Средняя: 4.5 (8 votes)
Share |
Юрий Глебович Карпов
И.В.Шошмина
А.Б.Беляев
Слушатели курса "Верификация параллельных и распределенных программных систем"
Юрий Глебович Карпов
А.Б.Беляев
Студенты курса "Верификация параллельных и распределенных программных систем"