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

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

В рамках семестра надо набирать баллы: работая на семинарах, на лекциях, выполняя практические задания, написав экзамен. В зависимости от суммы баллов будет поставлена оценка. На семинарах проводятся две контрольные. За каждую контрольную можно получить до 10 баллов. Контрольная – это частичная «репетиция» экзамена (задачи те же, условия те же, времени в два раза больше). Семинарист может поставить еще до 10 баллов за работу на семинарах. На лекциях даются небольшие задания, за которые тоже можно получить баллы. Для получения зачета нужно обязательно решить задачу «на Флойда», вне зависимости от того, сколько получено баллов к началу зачетной сессии. На экзамене будет много небольших задачек, их типы и примеры лекторы опубликуют перед экзаменом на странице курса. На экзамене можно пользоваться конспектами и книжками, но нельзя пользоваться компьютерами и нельзя разговаривать.

Это лишь краткое описание. Обязательно ознакомьтесь с полным описанием курса (pdf).

• Текущие баллы за курс. Следите за обновлениями на этой странице !!!

19 декабря, 08:40, П-6 -- "коллоквиум" (предварительный зачет).

25 декабря, 09:00, 726 -- показ работ "коллоквиума", проставление зачетов тем, кто успешно справился с заданием "коллоквиума".

26 декабря, 09:00, П-14 -- зачет по курсу (проводится одновременно на всём потоке). Продолжительность зачета - 90 минут.

29 декабря, 15:00, П-5 -- комиссия (показ работ и выставление оценок в тот же день).

11 января -- комиссия №2.

24 января, 09:00 -- экзамен, затем показ работ и выставление оценок. Студенты из групп 520 - 524 пишут экзамен в аудитории П-5. Студенты из групп 525 - 528 пишут экзамен в аудитории П-6.

NEW Материалы к экзамену:

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

• John Hatcliff, Gary T. Leavens, K. Rustan M. Leino, Peter Müller, Matthew J. Parkinson: Behavioral interface specification languages. ACM Comput. Surv. 44(3): 16 (2012) [pdf]

Материалы к практическому заданию по уточнению программ (RAISE):

• Формулировка задания и пример сделанного задания (предварительная версия, конструктивные комментарии приветствуются);

• Методическое пособие по RSL и RAISE-методу.

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

Материалы к контрольной работе №1:

• Упражнения для подготовки к контрольной работе №1;

• То, что надо обязательно знать по RSL;

• Методическое пособие по RSL;

• Описание языка RSL на русском языке.

Материалы к практическому заданию по Dafny:

• Формулировка задания и пример выполнения;

• проект Dafny;

• Dafny в браузере;

• Getting Started with Dafny;

• Слайды лекции №7;

• Упражнения по Dafny (Dafny trainings) для освоения языка Dafny и методов спецификации и верификации.

Материалы к практическому заданию по пруверу PVS:

• проект PVS — Prototype Verification System;

• памятка по работе с PVS.

Чтобы получить практическое задание по PVS, необходимо написать письмо на адрес khoroshilov@ispras.ru до 01 декабря 2012 года.

Материалы к практическому заданию по методам Флойда (Frama-C, ACSL, Why):

• проект Frama-C : плагин Jessie (плагин для автоматического построения условий корректности аннотированных спецификацией программ на языке Си).

Чтобы получить практическое задание по методам Флойда, необходимо написать письмо на адрес khoroshilov@ispras.ru до 01 декабря 2012 года.

Материалы к контрольной работе №2:

• Упражнения для подготовки к контрольной работе №2 (pdf).

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

Материалы к зачету:

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

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

• Лекция №1. 5 сентября 2012 года. «Место формальных методов в computer science.» [иллюстрации к лекции (pdf)]

52:15

55:46

• Лекция №2. 12 сентября 2012 года. «Виды формальных спецификаций. Примеры на RSL и Dafny.» [иллюстрации к лекции (pdf)]

44:10

47:11

• Лекция №3. 19 сентября 2012 года. «Спецификации в языках программирования. Design-by-Contract, Spec# (введение).» [иллюстрации к лекции (pdf)]

38:49

53:31

• Лекция №4. 26 сентября 2012 года. «Введение в Dafny.» [иллюстрации к лекции (pdf)]

29:46

44:45

• Лекция №5. 3 октября 2012 года. «Введение в Dafny (продолжение).» [иллюстрации к лекции (pdf)]

42:15

42:46

• Лекция №6. 10 октября 2012 года. «RAISE-метод.» [иллюстрации к лекции (pdf)]

44:04

51:01

• Лекция №7. 17 октября 2012 года. «Спецификация побочного эффекта программ.» [иллюстрации к лекции (pdf)]

32:55

42:28

• Лекция №8. 24 октября 2012 года. «Тестирование на основе моделей.» [иллюстрации к лекции (pdf)]

43:25

45:14

• Лекция №9. 31 октября 2012 года. «UniTESK.» [иллюстрации к лекции (pdf)]

46:12

37:45

• Лекция №10. 7 ноября 2012 года. «Аналитическая верификация программ: основные понятия.» [метод.пособие]

37:17

54:17

• Лекция №11. 14 ноября 2012 года. «Метод индуктивных утверждений Флойда.» [метод.пособие]

42:18

45:28

• Лекция №12. 21 ноября 2012 года. «Метод фундированных множеств Флойда.» [метод.пособие]

35:59

45:31

• Лекция №13. 28 ноября 2012 года. «Языки спецификации ACSL и PVS Language.» [PVS Language Reference]

40:13

43:17

• Лекция №14. 5 декабря 2012 года. «Инструмент PVS.» [PVS Prover Guide]

38:09

13:29

Пример, рассмотренный на лекции, можно прочитать в этом пособии (стр. 69 -- 72).

• Лекция №15. 12 декабря 2012 года. «Консультация по темам "Методы Флойда" и "PVS".» [иллюстрации к лекции]

38:44

33:33

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

•Jeannette M. Wing. A Specifier's Introduction to Formal methods ( pdf )

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