ВПнМ

Материал из eSyr's wiki.

Содержание 1 Информация о курсе 2 Структура курса 3 Практикум и зачёт курса 4 Литература 5 Ссылки 6 Курс

Информация о курсе

• Лектор — Савенков Константин Олегович
• E-mail: mailto:model-checking@lvk.cs.msu.su
• Подписка на рассылку: mailto:model-checking-subscribe@lvk.cs.msu.su
• Сайт курса: http://savenkov.lvk.cs.msu.su/mc.html
• Результаты проверки заданий: http://spreadsheets.google.com/pub?key=pEmg4-Q1vyjLMi3BPfZ_feQ

Структура курса

• Моделирование последовательных программ и параллельно взаимодействующих систем
• Спецификация проверяемых свойств
• Верификация при помощи Spin
• Алгоритмы верификации
• Теоретические и практические трудности верификации

Практикум и зачёт курса

Список задач (примеры задач):

• Дана программа, необходимо посчитать количество потенциальных и достижимых состояния, а так же построить LTS-диаграмму (пример задачи). Срок сдачи — до 7 марта.
• Для программы из первого задания построить её модель с использованием системы SPIN, а также вычислить с её использованием количество состояний модели. В качестве решения прислать модель и output верификатора (пример задачи). Срок сдачи — до 14 марта.
• Дана одна из функций ОС Minix, необходимо построить её модель (пример задачи). Срок сдачи — до 4 апреля.
• Для модели, построенной в предыдущей задаче, проверить ряд свойств (пример задачи). Срок сдачи — до 25 апреля.

Экзамен:

• Экзамен устный
• Кто пришлёт в течении одной-двух недель письмо, получит задачу, а также, если решит её в течении одной-двух недель, не получит задачу на экзамене
• Для тех, кто решит все задачи будет проведён предварительный экзамен на гуманных условиях

Литература

• Кларк, Грумберг, Пелед. Верификация моделей программ: Model checking, МЦНМО, 2002
• Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison Wesley, 2003

Ссылки

• http://www.spinroot.com/

Курс