ВПнМ

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

(Различия между версиями)
Перейти к: навигация, поиск
(2009 update)
(Ссылки)
 
(12 промежуточных версий не показаны.)
Строка 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
+
* Результаты проверки заданий: [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
+
* Список вопросов к экзамену: http://docs.google.com/Doc?id=dhf679dj_10dhnfpv28
 +
* [[ВПнМ/Теормин | Теормин]]
== Структура курса ==
== Структура курса ==
Строка 20: Строка 21:
* Задачи на моделирование программ: построить модель и прогнать на имит. движке: Minix или Plan9
* Задачи на моделирование программ: построить модель и прогнать на имит. движке: Minix или Plan9
* Планируется дать более сложную задачу, задача чуть побольше -->
* Планируется дать более сложную задачу, задача чуть побольше -->
-
Список задач ([[ВПнМ, примеры задач|примеры задач]]):
+
Работа в семестре – [[ВПнМ, примеры задач|список задач]]:
-
* Дана программа, необходимо посчитать количество потенциальных и достижимых состояния, а так же построить LTS-диаграмму ([[ВПнМ, примеры задач/Задача 1|пример задачи]]). Срок сдачи — до 23 марта.
+
* Дана программа, необходимо посчитать количество потенциальных и достижимых состояния, а также построить LTS-диаграмму ([[ВПнМ, примеры задач/Задача 1|пример]]).
-
* Для программы из первого задания построить её модель с использованием системы SPIN, а также вычислить с её использованием количество состояний модели. В качестве решения прислать модель и output верификатора ([[ВПнМ, примеры задач/Задача 2|пример задачи]]).
+
* Для программы из первого задания построить её модель с использованием системы SPIN, а также вычислить с её использованием количество состояний модели. В качестве решения прислать модель и output верификатора ([[ВПнМ, примеры задач/Задача 2|пример]]).
-
* Дана одна из функций ОС Minix, необходимо построить её модель ([[ВПнМ, примеры задач/Задача 3|пример задачи]]).
+
* Дана одна из функций ОС Minix, необходимо построить её модель ([[ВПнМ, примеры задач/Задача 3|пример]]).
-
* Для модели, построенной в предыдущей задаче, проверить ряд свойств ([[ВПнМ, примеры задач/Задача 4|пример задачи]]).
+
* Для модели, построенной в предыдущей задаче, проверить ряд свойств ([[ВПнМ, примеры задач/Задача 4|пример]]).
 +
* Задачи на '''LTL''' ([[ВПнМ, примеры задач/Задача 5|примеры]]).
Экзамен:
Экзамен:
-
* Экзамен устный
+
* Экзамен устный, принимает ~3 экзаменатора.
-
* Кто пришлёт в течении одной-двух недель письмо, получит задачу, а также, если решит её в течении одной-двух недель, не получит задачу на экзамене
+
* '''Те, кто на протяжении семестра работал и за все сданные задачи получен полный балл, может получить "3" автоматом'''.
-
* Для тех, кто решит все задачи будет проведён предварительный экзамен на гуманных условиях
+
* '''Те, кто на протяжении семестра не работал и не сдавал задачи, идут на пересдачу автоматом'''. На пересдаче даётся контрольная по тематике задач.
 +
* (тем, кто сдает Савенкову): '''без решённой LTL оценка за экзамен поставлена не будет'''.
 +
* будет 2 вопроса и задача (за каждый можно получить от 0 до 1 балла).
 +
* ещё будут дополнительные вопросы (не более 3 штук), за каждый можно повысить или понизить оценку на 0,5 балла. На пересдаче дают (возможно) больше дополнительных вопросов.
== Литература ==
== Литература ==
Строка 36: Строка 41:
== Ссылки ==
== Ссылки ==
* http://www.spinroot.com/
* http://www.spinroot.com/
 +
* http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml
== Курс ==
== Курс ==

Текущая версия

Савенков Константин Олегович
Савенков Константин Олегович

Содержание

[править] Информация о курсе

[править] Структура курса

  • Моделирование последовательных программ и параллельно взаимодействующих систем
  • Спецификация проверяемых свойств
  • Верификация при помощи 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

[править] Ссылки

[править] Курс


Верификация программ на моделях


01 02 03 04 05 06 07 08 09 10


Календарь

пт пт пт пт пт
Февраль
  08 15 22 29
Март
  14 21 28
Апрель
04 11 18

Материалы по курсу
Список вопросов к экзамену | Примеры задач: 1 2 3 4 5 | Теормин


Лекции

10 семестр История развития вычислительных технологий в СССР, России | Современные проблемы прикладной математики
9 семестр Формальная спецификация и верификация программ | Теория игры и исследования операций | История и методология прикладной математики | Основы российского права | История религии | Параллельная обработка данных
8 семестр Верификация программ на моделях | Математические основы теории прогнозирования | Основы квантовой физики и квантовых вычислений | Методы оптимизации | Распределённые операционные системы
7 семестр Вычислительные Системы | Объектно-ориентированные Анализ и Проектирование | Искусственный Интеллект | Математическая Логика | Функциональный Анализ | Социология | Параллельная Обработка Данных
6 семестр Основы Кибернетики | Численные Методы | Конструирование Компиляторов | Компьютерные Сети
5 семестр Базы Данных | Языки Программирования | Экономические Науки
3 семестр Операционные системы

Спецкурсы
Осень 2013 Современная криптография | Дизайн и реализация ОС FreeBSD
Весна 2011 Практические аспекты сетевой безопасности | Сетевое администрирование в UNIX
Осень 2010 UNИX | Теория функционального программирования. Язык Haskell | Введение в информационную безопасность | Информационный поиск
Весна 2010 UNИX | Архитектура и программирование массивно-параллельных вычислительных систем | Язык Ада
Осень 2009 UNИX | Введение в парадигмы программирования
Весна 2009 UNИX | Архитектура и программирование массивно-параллельных вычислительных систем
Осень 2008 UNИX | Структурные методы обработки изображений и сигналов
Весна 2008 UNИX | Вопросы организации вычислительных кластеров на основе UNIX-серверов | Философия математики
Осень 2007 UNИX
Весна 2007 UNИX | Практика мультипарадигмального программирования
Осень 2006 Введение в теорию построения оптимизирующих компиляторов

Отдельные лекции Bruce Eckel, The State of The Java Union | Richard Stallman: Free software: ethics and practice, Copyright vs Community in the Age of Computer Networks | Наану Александр, Vim | Erinn Clark, The Tor Project: Anonymity Online
Личные инструменты
Разделы