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

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

• окончательные результаты за курс (OpenOffice, PDF);

• Работает RSS-поток новостей практикума и курса.

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

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

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

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

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

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

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

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

• Пример решения и оформления задачи на уточнение (третья задачка)

• Методические материалы по решению четвертой задачи (предложение и формальное описание инвариантов типов данных и программных контрактов функций)

• Страница курса и страница производственной практики на сайте ИСП РАН.
• RSL Type Checker: для Windows (889 Кб) и для некоторых дистрибутивов Linux. Неподдерживаемые и дополнительные особенности языка RSL для rsltc.
• Задачи для семинара по структурам данных в RSL (PDF, 90Kb: http).
• Памятка по работе с pvs и лекции по аналитической верификации
• [Кузьменкова, Петренко-2008] Кузьменкова Е. А., Петренко А. К. Практикум по формальной спецификации программ на языке RSL – М.: Издательский отдел факультета ВМК МГУ, 2008. (WinWord (114 Кб): http).
• [Кузьменкова, Петренко-2001] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL: Конспект лекций. – М.: Издательский отдел факультета ВМК МГУ, 2001. - 107 с. (Zip-архив файла WinWord97, 137Kb: http).
• [Кузьменкова, Петренко-1999] Кузьменкова Е. А., Петренко А. К. Формальная спецификация программ на языке RSL. Методическое пособие по практикуму – М.: Издательский отдел факультета ВМК МГУ, 1999. (Zip-архив файла WinWord97, 260Kb: 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 )

Вам предстоит участвовать в проекте по разработке системы, первичное описание которой вы получили. Заказчиком системы является Петр Николаевич. Вашим непосредственным начальником будет Антон Егорович, программистом - Иван Семенович.

В рамках практикума по курсу ФСиВП от вас требуется подготовить формальное и детальное описание системы, которое можно передавать программисту для реализации. Подготовка должна происходить в три этапа.

1. На первом этапе вы взаимодействуете с заказчиком системы для выяснения более детальных требований. Результатом этого этапа должен быть документ на русском языке, в котором сформулированы требования к целевой системе. В качестве приложения к документу необходимо приложить RSL схему со списком операций, которые должна выполнять система, и списком типов, с которыми ей предстоит оперировать. Для каждой операции должна быть задана её сигнатура.

Этап заканчивается, когда заказчик прочитает документ с приложением и подпишет его.

2. На втором этапе вам потребуется оформить требования не менее чем к 10 операциям в формально, в виде спецификаций на языке RSL. Список операций, для которых требования формализуются, должен быть согласован с разработчиком.

Этап заканчивается, когда у разработчика не останется вопросов по спецификации. Спецификация на RSL должна соответствовать спецификации на русском языке. Все изменения в спецификации на русском языке должны согласовываться с заказчиком.

3. На третьем этапе разработчик реализует систему в соответствии со спецификацией и передает ее заказчику. Заказчик начинает работу с ней и может выявить несоответствия своим ожиданиям. Если эти несоответствия являются следствием неполноты или некорректности вашей спецификации, то ваш начальник принимает решение, надо ли обновлять и пересогласовывать спецификации.

С вашим заказчиком можно связаться по электронному адресу rsl-customer@sed.ispras.ru. Большинство взаимодействий с заказчиком будет происходить посредством электронной почты. Если потребуется для дела, возможно, вам удастся договориться с ним о других формах взаимодействия.

С Иваном Семёновичем можно связаться по электронному адресу rsl-developer@sed.ispras.ru. Он живет в другом городе и взаимодействие с ним возможно только через Интернет.

Электронный адрес Антона Егоровича rsl-manager@sed.ispras.ru. Он контролирует проект и решает все проблемы, связанные со взаимодействием с заказчиком и разработчиком.

Сроки проекта. 1-й этап - 7 ноября, 2-й этап - 25 ноября.

Оценка за данную работу выставляется начальником по результатам обсуждениия с заказчиком и разработчиком.

Существенно негативными моментами являются
- несогласованное с начальником невыполнение работы в срок;
- несоответствия, выявленные на третьем этапе, по причине проблем в вашей спецификации.

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