Главная страница « Информация « 5 курс «

Лекторы: проф., доктор физ.-мат. наук Петренко А. К., канд. физ.-мат. наук Хорошилов А. В.
Продолжительность: 36 часов лекции, 36 часов семинары, 72 часа самостоятельная работа.
Аудитория: студенты 5 курса кафедр СП, АСВК и АЯ.
Лекции по средам на первой паре (8:45 - 10:30) в аудитории П-8.

• Гугл-группа: новости + rss, онлайн-общение с преподавателями; участие свободное неанонимное.

• Гугл-сайт: "задачник-2010", задачи экзамена с примерами.

• Страница курса на сервере ИСП РАН.

• Результаты экзамена (XLS, 72кБ)

Расписание мероприятий

"The idea of specification is, ideally, to write as little as possible, to model the data structures in a minimal way, trying to avoid making premature design decisions about data structures and algorithms. Above all, the aim is to meet the requirements, and the less you write the less there is to validate against the requirements."

Разрабатываемые системы представляются в виде набора компонент, каждый компонент обладает своим программным интерфейсом. Методы строгого описания семантики таких интерфейсов составляют первую часть курса. Аналитические методы проверки корректности реализации интерфейсов данному строгому их описанию составляют вторую часть курса.

Информация об экзамене по курсу

• Экзамен поточный письменный с оценкой.

• На экзамене будет предложено 5 задач. Первые 3 задачи относятся к первой части курса (формальная спецификация программ), вторые 2 задачи относятся ко второй части курса (верификация программ). Оценка выставляется на основе успешности решения предложенных 5 задач и оценки за семинары (6-я "псевдозадача").

• На пересдаче зачтенные в течение семестра и экзамена задачи не учитываются, оценка за семинары учитывается.

• Каждая задача может быть решена на полный, половинный или нулевой балл. Оценка за курс выставляется на основе количества полностью решенных задач и количества задач, решенных наполовину. Способ определения балла за каждое конкретное решение определяется только экзаменаторами. Половинные баллы не суммируются. Перевод оценки за семинары в полный/половинный/нулевой балл определяется семинаристом.

• Алгоритм перевода баллов в оценку: (e - количество половинных баллов, f - количество полных баллов, e + f < 7)

• "отлично": f isin {5, 6}
• "хорошо": f = 4 /\ e isin {1,2}
• "удовлетворительно": f isin {3,4} /\ e <= f \ 4

• Кроме экзамена проводятся два коллоквиума в течение семестра (коллоквиум по первой части курса и коллоквиум по второй части курса) и письменная работа на задачах обоих коллоквиумов в конце 2010 года. Коллоквиумы дают возможность зачесть часть задач раньше экзамена, тем самым упростить сдачу курса в сессию.

• RSL Type Checker: для Windows (889 Кб) и для некоторых дистрибутивов Linux. Неподдерживаемые и дополнительные особенности языка RSL для rsltc.

• Памятка по работе с pvs и лекции по аналитической верификации

• Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL – М.: Издательский отдел факультета ВМК МГУ, 2008. (WinWord (114 Кб): http, ftp).

• Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL: Конспект лекций. – М.: Издательский отдел факультета ВМК МГУ, 2001. - 107 с. (Zip-архив файла WinWord97, 137Kb: http, ftp).

• Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму – М.: Издательский отдел факультета ВМК МГУ, 1999. (Zip-архив файла WinWord97, 260Kb: http, ftp).

• Пискунов А.Г. The RAISE Method Group: алгебраическое проектирование класса – 2007. (PDF, 341Kb: http).

• George C. Introduction to RAISE. UNU/IIST – 2002. (PDF, 272Kb: http).

• Джим Вудкок. Первые шаги к решению проблемы верификации программ // Открытые системы, 2006, ?8. читать онлайн

• Джонатан П. Боуэн, Майкл Дж. Хинчи. Десять заповедей формальных методов // Мир ПК, 1997, ??9-10. читать онлайн: часть 1, часть 2.

• Кулямин В.В. Методы верификации программного обеспечения ( pdf )

• Кулямин В.В. Перспективы интеграции методов верификации программного обеспечения ( читать онлайн )

• Парнас Д.Л. Реальное переосмысление "формальных методов" ( читать онлайн )

• Van H.D., George C., Janowski T. Specification Case Studies in RAISE // UNU-IIST, Springer, 2002 ( pdf )

• Ковалев С.П. Применение формальных методов для обеспечения качества вычислительных систем // Вестник НГУ, серия "Математика, механика, информатика", Том IV, 2004, вып.2, с.49--74 ( pdf )

Семинары проходят по средам в ауд.526-б или 248 (комп.класс) на 2/3 парах. О начале занятий в компьютерном классе будет сообщено позднее.

• Страница преддипломной практики на сервере ИСП РАН.

• реферат --- информация готовится...

Размещение на других ресурсах, а также коммерческое использование материалов, опубликованных в данном разделе, возможно только с разрешения авторов.