ВПнМ

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

Версия 23:00, 2 июня 2010 (править) 212.192.251.39 (Обсуждение) (→Ссылки) ← К предыдущему изменению		Версия 16:01, 3 июня 2010 (править) (отменить) ESyr01 (Обсуждение | вклад) (Отмена правки № 7839 участника 212.192.251.39 (обсуждение) толсто же, ну.) К следующему изменению →
Строка 40:		Строка 40:
	== Ссылки ==		== Ссылки ==
	* http://www.spinroot.com/		* http://www.spinroot.com/
-	* http://www.meatspin.com/
	== Курс ==		== Курс ==

---

Версия 16:01, 3 июня 2010

Содержание 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
• Результаты проверки заданий: 2008 2009 2010
• Список вопросов к экзамену: http://docs.google.com/Doc?id=dhf679dj_10dhnfpv28
• Теормин

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

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

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

Работа в семестре – список задач:

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

Экзамен:

• Экзамен устный, принимает ~3 экзаменатора.
• Те, кто на протяжении семестра работал и за все сданные задачи получен полный балл, может получить "3" автоматом.
• (тем, кто сдает Савенкову): без решённой LTL оценка за экзамен поставлена не будет.
• будет 2 вопроса и задача (за каждый можно получить от 0 до 1 балла).
• ещё будут дополнительные вопросы (не более 3 штук), за каждый можно повысить или понизить оценку на 0,5 балла.

Литература

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

Ссылки

• http://www.spinroot.com/

Курс