МФСП
Материал из eSyr's wiki.
(Различия между версиями)
| Строка 6: | Строка 6: | ||
* Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru) | * Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru) | ||
* Семинарист АСВК — Петровский Михаил Игоревич | * Семинарист АСВК — Петровский Михаил Игоревич | ||
| + | |||
| + | * Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя. | ||
== Структура курса == | == Структура курса == | ||
| Строка 25: | Строка 27: | ||
* [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 Страница курса на сайте ИСП РАН] | ||
| + | |||
| + | «Что гуглить»: | ||
| + | * [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] | ||
{{Курс МФСП}} | {{Курс МФСП}} | ||
Версия 14:44, 12 сентября 2008
Содержание |
Формальная спецификация и верификация программ
Информация о курсе
- Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru)
- Семинарист АСВК — Петровский Михаил Игоревич
- Экзамен письменный. Пользоваться можно чем угодно, списывать нельзя.
Структура курса
- (5—6 лекций) RAISE/RSL
- (~3 семинара) Параллельно с этим нач. практические занятия. Порядка трёх занятий на практикуме будет посвящено выполнению и сдаче контрольных заданий на практикуме
- (3 лекции) Методы аналитической верификации. В частности, метод Флойда
- (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS
- Коллоквиум
- Экзамен
Материалы
- [Кузьменкова, Петренко-2008d; Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL
- [Кузьменкова, Петренко-2001d; Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL: Конспект лекций.
- [Кузьменкова, Петренко-1999d; Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму
- [Мансуров, Майлинговаd; Мансуров Н. Н., Майлингова О. Л. "Методы формальной спецификации программ: языки MSC и SDL" Методическое пособие по практикуму
(см. также Ссылки)
Ссылки
«Что гуглить»:
