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

Лекции

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 год)

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

• Gerard J. Holzmann, Logical Model Checking, Caltech 2008, CS118
• Joost-Pieter Katoen, Introduction to Model Checking