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

Версия 15:08, 12 сентября 2008

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

Петренко Александр Константинович

Информация о курсе

• Лектор — Петренко Александр Константинович (mailto:petrenko@ispras.ru)
• Семинарист АСВК — Петровский Михаил Игоревич

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

Структура курса

1. (5—6 лекций) RAISE/RSL
   • (~3 семинара) Параллельно с этим нач. практические занятия. Порядка трёх занятий на практикуме будет посвящено выполнению и сдаче контрольных заданий на практикуме
2. (3 лекции) Методы аналитической верификации. В частности, метод Флойда
3. (3—4 лекции) Инструментальная поддержка аналитической верификации. В качестве базы испльзуется PVS
4. Коллоквиум
5. Экзамен

Материалы

• [Кузьменкова, Петренко-2008] Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL
• [Кузьменкова, Петренко-2001] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL: Конспект лекций.
• [Кузьменкова, Петренко-1999] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму
• [Мансуров, Майлингова] Мансуров Н. Н., Майлингова О. Л. "Методы формальной спецификации программ: языки MSC и SDL" Методическое пособие по практикуму

(см. также Ссылки)

Ссылки

• Страница курса на сайте кафедры СП
• Страница курса на сайте ИСП РАН

«Что гуглить»:

• VDM, ASML, Z, B-toolkit
• JML, Eiffel
• Spec#
• LSB
• Microsoft Interoperability Project
• PVS, Isabella, HOL

Курс