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

Лекции

  1. 11.02.2013. Введение в формальные методы проверки правильности программ. (слайды в PDF)
    • Правильность программ. Актуальность верификации.
    • Формальные методы проверки правильности. Тестирование.
    • Доказательство теорем. Статический анализ.
    • Верификация программ на моделях. Динамическая верификация. История развития.
    • Обзор курса. Порядок выставления оценок.
  2. 25.02.2013. Моделирование программ. (слайды в PDF)
    • Контрольная работа. Итоги прошлой лекции.
    • Области применения и общая схема верификации программ на моделях.
    • Потенциальные и достижимые состояния программы.
    • Процесс построения модели программы.
  3. 04.03.2013. Системы переходов (LTS). Корректность и адекватность LTS модели. (слайды в PDF)
    • Схема формальных понятий. Различные представления программы и требований.
    • Размеченные системы переходов.
    • Понятие недетерминизма.
    • Пути. Вычисления. Трассы. Свойства линейного времени.
    • Корректность и адекватность модели (на уровне трасс и LTS).
  4. 11.03.2013. Система верификации SPIN. Описание моделей на языке Promela.(слайды в PDF)
    • Система верификации SPIN. Язык Promela.
    • Основные операторы языка Promela.
    • Взаимодействие при помощии передачи сообщений.
    • Типы данных. Задание потока управления модели.
    • Протокол чередования бита. Параметры запуска верификатора.
  5. 18.03.2013. Практические приёмы абстракции. Свойства линейного времени. Спецификация и верификация свойств при помощи Spin.(слайды в PDF)
    • Практические приёмы абстракции.
    • Ассерты. Состояния останова. Циклы бездействия. Справедливость.
    • Свойства безопасности и живучести.
    • Примеры проверки свойств протоколов.
  6. 25.03.2013. Свойства живучести в Promela. Спецификация и верификация свойств при помощи автоматов Бюхи.(слайды в PDF)
    • Свойства живучести в Spin. Конструкции never.
    • Трассовые ассерты. Верификация нарушения свойств.
    • Автоматы Бюхи.
    • Проверка свойств при помощи автоматов Бюхи.
  7. 01.04.2013. Логика линейного времени (LTL). Использование LTL в Spin.(слайды в PDF)
    • Логика LTL. Семантика выполнимости формул.
    • Логика LTL. Примеры.
    • Спецификация свойств на LTL.
    • Переход от LTL к автоматам Бюхи.
    • Практические приемы работы с LTL. Шаблоны.
  8. 08.04.2013. Графы программ. Системы с каналами взаимодействия. Синхронный и асинхронный параллелизм.(слайды в PDF)
    • Графы программ.
    • Графы программ с разделяемыми переменными.
    • Графы распределённых программ. Синхронный и асинхронный параллелизм.
  9. 15.04.2013. Выразительная мощность LTL. Корректная абстракция графов программ. Отношение моделирования (симуляции).(PDF)

Оценки по практикуму: [Google.Docs]

Слайды (2011г.)

Список вопросов к экзамену (2011 год)

Курс лекций разработан на основе следующих курсов:

©  Konstantin Savenkov, 2003-2011
savenkov@cs.msu.su

Яндекс цитирования