МФСП
Материал из eSyr's wiki.
(Различия между версиями)
(+2010) |
|||
| (8 промежуточных версий не показаны.) | |||
| Строка 2: | Строка 2: | ||
[[Image:Petrenko.jpg|240px|thumb|Петренко Александр Константинович]] | [[Image:Petrenko.jpg|240px|thumb|Петренко Александр Константинович]] | ||
| - | [[Image:Petrenko_bot.jpg|240px|thumb|]] | + | [[Image:Petrenko_bot.jpg|240px|thumb|Алексей Хорошилов]] |
== Информация о курсе == | == Информация о курсе == | ||
* Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru) | * Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru) | ||
| Строка 8: | Строка 8: | ||
* Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя. | * Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя. | ||
| + | * Для оценки нужно иметь зачёт по практикуму, суммарная оценка на экзамене складывается из оценки на коллоквиуме, на экзамене и, возможно, оценки за практикум | ||
== Структура курса == | == Структура курса == | ||
| Строка 15: | Строка 16: | ||
# (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS | # (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&# | + | * [http://sp.cs.msu.su/courses/fmsp/meth2008.zip [Кузьменкова, Петренко-2008] Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL] |
| - | * [http://sp.cs.msu.su/courses/fmsp/rsl2001.zip [Кузьменкова, Петренко-2001&# | + | * [http://sp.cs.msu.su/courses/fmsp/rsl2001.zip [Кузьменкова, Петренко-2001] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL: Конспект лекций.] |
| - | * [http://sp.cs.msu.su/courses/fmsp/total13.zip [Кузьменкова, Петренко-1999&# | + | * [http://sp.cs.msu.su/courses/fmsp/total13.zip [Кузьменкова, Петренко-1999] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму] |
| - | * [http://sp.cs.msu.su/courses/fmsp/msc&sdl.pdf [Мансуров, Майлингова&# | + | * [http://sp.cs.msu.su/courses/fmsp/msc&sdl.pdf [Мансуров, Майлингова] Мансуров Н. Н., Майлингова О. Л. "Методы формальной спецификации программ: языки MSC и SDL" Методическое пособие по практикуму] |
| - | + | ||
| - | == Ссылки == | + | === Ссылки === |
* [http://sp.cs.msu.su/courses/fmsp/ Страница курса на сайте кафедры СП] | * [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.ispras.ru/~RedVerst/RedVerst/Lectures%20and%20training%20courses/MSU%20course%20Formal%20specification%20of%20software/RMain.html Страница курса на сайте ИСП РАН] | ||
| Строка 35: | Строка 35: | ||
* [http://www.google.com/search?q=Microsoft+Interoperability+Project Microsoft Interoperability Project] | * [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] | * [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] | ||
| + | |||
| + | == Курс == | ||
| + | * [[МФСП: Оформление задач|Оформление задач]] | ||
{{Курс МФСП}} | {{Курс МФСП}} | ||
| + | {{Лекции}} | ||
Текущая версия
Содержание |
[править] Формальная спецификация и верификация программ
[править] Информация о курсе
- Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru)
- Семинарист АСВК — Петровский Михаил Игоревич
- Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя.
- Для оценки нужно иметь зачёт по практикуму, суммарная оценка на экзамене складывается из оценки на коллоквиуме, на экзамене и, возможно, оценки за практикум
[править] Структура курса
- (5—6 лекций) RAISE/RSL
- (~3 семинара) Параллельно с этим нач. практические занятия. Порядка трёх занятий на практикуме будет посвящено выполнению и сдаче контрольных заданий на практикуме
- (3 лекции) Методы аналитической верификации. В частности, метод Флойда
- (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS
- Коллоквиум
- Экзамен (результаты: 2009 2010)
[править] Материалы
- [Кузьменкова, Петренко-2008] Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL
- [Кузьменкова, Петренко-2001] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL: Конспект лекций.
- [Кузьменкова, Петренко-1999] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму
- [Мансуров, Майлингова] Мансуров Н. Н., Майлингова О. Л. "Методы формальной спецификации программ: языки MSC и SDL" Методическое пособие по практикуму
[править] Ссылки
«Что гуглить»:
[править] Курс
Формальная спецификация и верификация программ
|
|
