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

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

14 декабря, 8:45 - 10:15, предварительный зачет, аудитория П-12

21 декабря, 14:00, показ работ предварительного зачета с разбором ошибок, аудитория П-8а

22 декабря, 10:00-11:30, зачет, аудитория П-5

26 декабря, 9:30-10:30, показ работ и проставление зачетов, аудитория 726

28 декабря, 9:00-11:30, комиссия, аудитория П-8

29 декабря, 10:00, показ работ комиссии, аудитория 726, проставление зачетов

11 января, 9:00, вторая комиссия, аудитория 505

13 января, 9:00, показ работ второй комиссии, аудитория 726

18 января, 9:30, третья комиссия, ИСП РАН

19 января, 9:00, показ работ третьей комиссии, аудитория 726

19 января, 10:00, консультация к экзамену, аудиторя П-14

21 января, 9:00, экзамен, аудитории П-5 (группы 520-524) и П-6 (группы 525-528)

21 января состоялся экзамен по нашему курсу. Начало в 9:00. Экзамен письменный. Длительность 120 минут. Каждому студенту был предложен билет, состоящий из 10 заданий. Задания покрывали весь курс лекций и семинаров. Каждое задание оценивалось от 0 до 5 баллов. Список возможных типов заданий на экзамене можно скачать прямо тут. Ответы следовало писать прямо на билете. На экзамене можно было пользоваться любой печатной продукцией и рукописными текстами (крайне рекомендовалось взять конспекты лекций и пособия по нашему курсу). Пользоваться электронными средствами связи и всем прочим барахлом было запрещено.

19 января в П-14 в 10:00 состоялась консультация к экзамену. Все желающие смогли задать интересующие вас вопросы непосредственно лекторам курса.

Программа экзаменационного дня следующая:
9:00 - 11:00 - Вы пишете экзамен.
11:00 - 13:00 - мы проверяем Ваши работы.
13:00 - 14:30 - показ работ и выставление оценок в зачетки.

У всех, кто изъявил бы желание писать экзамен во второй раз, набранные за семестр баллы делятся пополам. В остальном пересдача не отличается от экзамена.

1. Что такое формальные спецификации. Абстракция, строгость (rigour), систематичность. Верификация и валидация программ и требований.

2. Формальные методы разработки программ. Уточнение программ. Принцип подстановки Лисков. Функция абстракции. Диаграмма коммутативности. Design by Contract.

3. Полнота спецификаций. Непротиворечивость спецификаций.

4. Методы VDM и RAISE.

5. Алгебраические спецификации.

6. Моделеориентированные спецификации: явные и неявные.

7. Исполнимые формальные спецификации: конечные автоматы, системы переходов.

8. Языки спецификации, спецификационные расширения языков программирования (в том числе аннотации), библиотеки функций для описания свойств данных и операций в программе без расширения языка программирования. Примеры. Сравнение.

9. Язык RSL.

10. Использование формальных спецификаций в строгих (rigour) подходах к поиску ошибок в программах.

11. Инструменты Spec# и Dafny. Проблема верификации программ, оперирующих с динамической памятью.

12. Formal testing. Model-based testing.

13. Аналитическая верификация. Понятия частичной и полной корректности.

14. Основные понятия методов Флойда. Точки сечения, индуктивные утверждения, оценочные функции, фундированные множества.

15. Метод индуктивных утверждений Флойда. Условия верификации и условия корректности.

16. Метод оценочных функций Флойда. Условия корректности и завершимости.

17. Методы Флойда для рекурсивных программ.

18. Методы Флойда для программ с частичными функциями (в частности, с операциями обращения к элементам массива).

19. Инструмент PVS: общая характеристика. Теоремы, вид представления доказательств, интерактивность.

20. Язык спецификации инструмента PVS.

21. Основные команды инструмента PVS : skolem!, flatten, split, case, induct, inst, expand, replace, lemma, assert, grind.

22. ACSL – язык аннотаций для программ на языке Си. Инструмент Frama-C.

• Блог курса, где размещаются объявления.

• Типы заданий на экзамене.

• Информация об экзамене, зачете и практических заданиях.

• Текущие баллы

• [pdf] Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL – М.: Издательский отдел факультета ВМК МГУ, 2008.

• Лекции по аналитической верификации.

• Задачи по методам Флойда для подготовки к зачету (OpenOffice).

• Инструмент Dafny: Dafny в браузере, описание языка Dafny.

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

• Инструмент PVS, памятка по работе с PVS.

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

"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."

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

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

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

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

• Пискунов А.Г. 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 )

• Anne Haxthausen: Lecture Notes on the RAISE Development Method ( pdf )

•Barnett M., Fahndrich M., Leino R., Mueller P., Schulte W., and Venter H. Specification and Verification: The Spec# Experience // Communications of the ACM, June 2011 (pdf)

•Жуков Д. Конспекты по методам Флойда ( pdf )

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