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

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

Перейти к: навигация, поиск

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

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

Текущая версия Ваш текст
Строка 5: Строка 5:
* Подписка на рассылку: mailto:model-checking-subscribe@lvk.cs.msu.su
* Подписка на рассылку: mailto:model-checking-subscribe@lvk.cs.msu.su
* Сайт курса: http://savenkov.lvk.cs.msu.su/mc.html
* Сайт курса: 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://spreadsheets.google.com/pub?key=pEmg4-Q1vyjLMi3BPfZ_feQ
-
* Список вопросов к экзамену: http://docs.google.com/Doc?id=dhf679dj_10dhnfpv28
+
-
* [[ВПнМ/Теормин | Теормин]]
+
== Структура курса ==
== Структура курса ==
Строка 21: Строка 19:
* Задачи на моделирование программ: построить модель и прогнать на имит. движке: Minix или Plan9
* Задачи на моделирование программ: построить модель и прогнать на имит. движке: Minix или Plan9
* Планируется дать более сложную задачу, задача чуть побольше -->
* Планируется дать более сложную задачу, задача чуть побольше -->
-
Работа в семестре – [[ВПнМ, примеры задач|список задач]]:
+
Список задач ([[ВПнМ, примеры задач|примеры задач]]):
-
* Дана программа, необходимо посчитать количество потенциальных и достижимых состояния, а также построить LTS-диаграмму ([[ВПнМ, примеры задач/Задача 1|пример]]).
+
* Дана программа, необходимо посчитать количество потенциальных и достижимых состояния, а так же построить LTS-диаграмму ([[ВПнМ, примеры задач/Задача 1|пример задачи]]). Срок сдачи — до 7 марта.
-
* Для программы из первого задания построить её модель с использованием системы SPIN, а также вычислить с её использованием количество состояний модели. В качестве решения прислать модель и output верификатора ([[ВПнМ, примеры задач/Задача 2|пример]]).
+
* Для программы из первого задания построить её модель с использованием системы SPIN, а также вычислить с её использованием количество состояний модели. В качестве решения прислать модель и output верификатора ([[ВПнМ, примеры задач/Задача 2|пример задачи]]). Срок сдачи — до 14 марта.
-
* Дана одна из функций ОС Minix, необходимо построить её модель ([[ВПнМ, примеры задач/Задача 3|пример]]).
+
* Дана одна из функций ОС Minix, необходимо построить её модель ([[ВПнМ, примеры задач/Задача 3|пример задачи]]). Срок сдачи — до 4 апреля.
-
* Для модели, построенной в предыдущей задаче, проверить ряд свойств ([[ВПнМ, примеры задач/Задача 4|пример]]).
+
* Для модели, построенной в предыдущей задаче, проверить ряд свойств ([[ВПнМ, примеры задач/Задача 4|пример задачи]]). Срок сдачи — до 25 апреля.
-
* Задачи на '''LTL''' ([[ВПнМ, примеры задач/Задача 5|примеры]]).
+
Экзамен:
Экзамен:
-
* Экзамен устный, принимает ~3 экзаменатора.
+
* Экзамен устный
-
* '''Те, кто на протяжении семестра работал и за все сданные задачи получен полный балл, может получить "3" автоматом'''.
+
* Кто пришлёт в течении одной-двух недель письмо, получит задачу, а также, если решит её в течении одной-двух недель, не получит задачу на экзамене
-
* '''Те, кто на протяжении семестра не работал и не сдавал задачи, идут на пересдачу автоматом'''. На пересдаче даётся контрольная по тематике задач.
+
* Для тех, кто решит все задачи будет проведён предварительный экзамен на гуманных условиях
-
* (тем, кто сдает Савенкову): '''без решённой LTL оценка за экзамен поставлена не будет'''.
+
-
* будет 2 вопроса и задача (за каждый можно получить от 0 до 1 балла).
+
-
* ещё будут дополнительные вопросы (не более 3 штук), за каждый можно повысить или понизить оценку на 0,5 балла. На пересдаче дают (возможно) больше дополнительных вопросов.
+
== Литература ==
== Литература ==
-
* Кларк, Грамберг, Пелед. Верификация моделей программ: Model checking, МЦНМО, 2002
+
* Кларк, Грумберг, Пелед. Верификация моделей программ: Model checking, МЦНМО, 2002
* Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison Wesley, 2003
* Holzmann. The Spin Model Checker: Primer and Reference Manual, Addison Wesley, 2003
== Ссылки ==
== Ссылки ==
* http://www.spinroot.com/
* 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
Личные инструменты
Разделы