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

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

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

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

= Формальная спецификация и верификация программ =

* Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя.
* Для оценки нужно иметь зачёт по практикуму, суммарная оценка на экзамене складывается из оценки на коллоквиуме, на экзамене и, возможно, оценки за практикум

== Структура курса ==
# (5—6 лекций) RAISE/RSL
#* (~3 семинара) Параллельно с этим нач. практические занятия. Порядка трёх занятий на практикуме будет посвящено выполнению и сдаче контрольных заданий на практикуме
# (3 лекции) Методы аналитической верификации. В частности, метод Флойда
# (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS
# Коллоквиум
# Экзамен (результаты: [http://spreadsheets.google.com/pub?key=tACFiixUTF7fD4j7Sj3oUnQ&gid=2 2009] [https://spreadsheets.google.com/pub?key=0AoN5iJE0CvIadGV1NjdOQjV0eXdsSEpoRVZ5TFBoNHc&hl=ru&output=html 2010])

== Материалы ==
* [http://sp.cs.msu.su/courses/fmsp/meth2008.zip [Кузьменкова, Петренко-2008&#93; Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL]
* [http://sp.cs.msu.su/courses/fmsp/rsl2001.zip [Кузьменкова, Петренко-2001&#93; Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL: Конспект лекций.]
* [http://sp.cs.msu.su/courses/fmsp/total13.zip [Кузьменкова, Петренко-1999&#93; Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму]
* [http://sp.cs.msu.su/courses/fmsp/msc&sdl.pdf [Мансуров, Майлингова&#93; Мансуров Н. Н., Майлингова О. Л. "Методы формальной спецификации программ: языки MSC и SDL" Методическое пособие по практикуму]

=== Ссылки ===
* [http://sp.cs.msu.su/courses/fmsp/ Страница курса на сайте кафедры СП]
* [http://www.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/RMain.html Страница курса на сайте ИСП РАН]

«Что гуглить»:
* [http://www.google.com/search?q=Vienna+Development+Method VDM], [http://www.google.com/search?q=Abstract+State+Machine+Language ASML], [http://www.google.com/search?q=Z+notation Z], [http://www.google.com/search?q=B-toolkit B-toolkit]
* [http://www.google.com/search?q=Java+Modelling+Language JML], [http://www.google.com/search?q=Eiffel+language Eiffel]
* [http://www.google.com/search?q=Spec# Spec#]
* [http://www.google.com/search?q=Linux+Standard+Base LSB]
* [http://www.google.com/search?q=Microsoft+Interoperability+Project Microsoft Interoperability Project]
* [http://www.google.com/search?q=PVS+Specification+and+Verification+System PVS], [http://www.google.com/search?q=Isabelle+theorem+prover Isabella], [http://www.google.com/search?q=HOL+theorem+prover HOL]

== Курс ==
{{Курс МФСП}}
{{Лекции}}

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

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

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

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

Получено с http://esyr.org/wiki/%D0%9C%D0%A4%D0%A1%D0%9F