Редактирование: ВПнМ

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

Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.

Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.

[[Изображение:Savenkov.jpg|320px|thumb|Савенков Константин Олегович]]
== Информация о курсе ==
* Лектор — Савенков Константин Олегович
* 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 2008] [http://spreadsheets.google.com/pub?key=pEmg4-Q1vyjIKG8JMLlDuPw 2009] [http://spreadsheets.google.com/pub?key=tW03VzK1KKvy0R_M2qe8FFg&output=html 2010]
* Список вопросов к экзамену: http://docs.google.com/Doc?id=dhf679dj_10dhnfpv28
* [[ВПнМ/Теормин | Теормин]]

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

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

Работа в семестре – [[ВПнМ, примеры задач|список задач]]:
* Дана программа, необходимо посчитать количество потенциальных и достижимых состояния, а также построить LTS-диаграмму ([[ВПнМ, примеры задач/Задача 1|пример]]).
* Для программы из первого задания построить её модель с использованием системы SPIN, а также вычислить с её использованием количество состояний модели. В качестве решения прислать модель и output верификатора ([[ВПнМ, примеры задач/Задача 2|пример]]).
* Дана одна из функций ОС Minix, необходимо построить её модель ([[ВПнМ, примеры задач/Задача 3|пример]]).
* Для модели, построенной в предыдущей задаче, проверить ряд свойств ([[ВПнМ, примеры задач/Задача 4|пример]]).
* Задачи на '''LTL''' ([[ВПнМ, примеры задач/Задача 5|примеры]]).
Экзамен:
* Экзамен устный, принимает ~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/
* http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml

== Курс ==
{{Курс ВПнМ}}

Пожалуйста, обратите внимание, что все ваши добавления могут быть отредактированы или удалены другими участниками. Если вы не хотите, чтобы кто-либо изменял ваши тексты, не помещайте их сюда.
Вы также подтверждаете, что являетесь автором вносимых дополнений, или скопировали их из источника, допускающего свободное распространение и изменение своего содержимого (см. eSyr's_wiki:Авторское право).
НЕ РАЗМЕЩАЙТЕ БЕЗ РАЗРЕШЕНИЯ ОХРАНЯЕМЫЕ АВТОРСКИМ ПРАВОМ МАТЕРИАЛЫ!

Описание изменений:

Отменить | Справка по редактированию (в новом окне)

Шаблоны, использованные на этой странице:

Получено с http://esyr.me/wiki/%D0%92%D0%9F%D0%BD%D0%9C

Редактирование: ВПнМ

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

Просмотры

Личные инструменты

Навигация

инструменты

Разделы

Спецкурсы

9 семестр

7 семестр

5 семестр

3 семестр

Поиск

Инструменты

@@ Строка 30: / Строка 30: @@
 * Экзамен устный, принимает ~3 экзаменатора.
 * '''Те, кто на протяжении семестра работал и за все сданные задачи получен полный балл, может получить "3" автоматом'''.
-* '''Те, кто на протяжении семестра не работал и не сдавал задачи, идут на пересдачу автоматом'''. На пересдаче даётся контрольная по тематике задач.
+* '''Те, кто на протяжении семестра не работал и не сдавал задачи, идут на пересдачу автоматом'''.
 * (тем, кто сдает Савенкову): '''без решённой LTL оценка за экзамен поставлена не будет'''.
 * будет 2 вопроса и задача (за каждый можно получить от 0 до 1 балла).