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