Курс, 3-й поток, 7-й и 8-й семестры лекции (64 часа), экзамен в 8-м семестре семинары (64 часа), зачет без оценки в 7-м и 8-м семестре

Скачать 45.7 Kb.

Название	Курс, 3-й поток, 7-й и 8-й семестры лекции (64 часа), экзамен в 8-м семестре семинары (64 часа), зачет без оценки в 7-м и 8-м семестре
Дата публикации	28.06.2013
Размер	45.7 Kb.
Тип	Программа курса

litcey.ru > Информатика > Программа курса

Методы формальной спецификации программ

4 курс, 3-й поток, 7-й и 8-й семестры.

лекции (64 часа), экзамен в 8-м семестре

семинары (64 часа), зачет без оценки в 7-м и 8-м семестре
Кафедра, отвечающая за курс: системного программирования

Составители программы: проф., доктор физ.-мат. наук Петренко А. К.,

канд. физ.-мат. наук Мансуров Н. Н.

Лекторы: проф., доктор физ.-мат. наук Петренко А.К.,

Фролов А. М., Караулов А. А.

Аннотация

В курсе рассматривается широкий спектр подходов к формальной спецификации программ от классических языков формальной спецификации до языков проектирования и определения архитектуры. Помимо собственно проблем специфицирования затрагиваются вопросы моделирования, пошагового проектирования, анализа программ и программной архитектуры, методы аналитической верификации и тестирования на основе формальных спецификаций. Курс базируется на следующих языках спецификации и формальных нотациях: RSL, SDL, MSC с привлечением примеров на UML и других языках спецификации и моделирования.
^

Программа курса

ПЕРВАЯ ЧАСТЬ (7-й семестр)

Понятие строгих и формальных методах разработки программ. Место строгих и формальных методов процессах разработки программ. Виды использования строгих и формальных методов: моделирование, специфицирование, верификация. Моделирование и абстракция. Виды абстрагирования. Парадигмы моделирования и спецификации.

Методология RAISE - строгий подход к индустриальной программной инженерии; язык RSL. Типы, аксиомы, значения. Алгебраические спецификации, явные и неявные формы спецификации операций. Абстракция и уточнение в RSL. Пошаговое уточнение в RAISE. Параллельность. Недетерминизм и «недоспецификация». Задача проверки реализации на соответствие требований, специфицированных для модели.

^ Верификация программ. Верификация моделей и верификация реализаций. Статическая и динамическая верификация. Подходы статической верификации. Верификация моделей программ.

^ Динамическая верификация программ. Верификация и валидация. Тестирование. Тестирование на основе моделей. Связь между тестированием на основе моделей и разработкой на основе моделей (MDA). Методы «черного ящика» и «белого ящика». Классы эквивалентности тестовых наборов. Критерии полноты тестового покрытия. Декомпозиция тестовых наборов и подзадачи тестирования, унифицированные архитектуры тестовых наборов. Конечные автоматы (КА): детерминированные и недетерминированные, расширенные КА, Statecharts. Задачи тестирования на основе моделей: проверка на соответствие конечному автомату, построение дерева переходов, построение различающей последовательности, метод Василевского, uio-последовательности, проверка на соответствие обобщенному конечному автомату. Формальные спецификации как источник для построения тестовых наборов.

^ Формальная спецификация структур данных. Спецификация и тестирование трансляторов и других языковых процессоров. Спецификация языков программирования. Абстрактный синтаксис, статическая семантика, динамическая семантика. Денотационная семантика, операционная семантика. Well-formed-функции. Атрибутные грамматики как средство описания статической и динамической семантики.

ЧАСТЬ ВТОРАЯ (8-семестр)

^ Обзор основных этапов объектно-ориентированного процесса разработки программного обеспечения. Этап анализа требований. Этап системного анализа. Этап системного проектирования. Этап детального проектирования. Структурная и функциональная точки зрения при составлении описаний программных средств.

^ Сценарные модели. Сбор требований к проектируемой программной системе. Функциональные и нефункциональные требования. Основные понятия сценарных моделей: агент, сценарий, интерфейс. Неформальные диаграммы сценарных моделей. Табличное представление сценария. Словарь системы. Формализация сценарных моделей.

^ Язык диаграмм взаимодействия. Понятие графической грамматики. Графический синтаксис диаграмм взаимодействия. Основные понятия диаграмм взаимодействия: объект, временная ось, событие. Основные события диаграмм взаимодействия: сообщения, действия, создание объектов, уничтожение объектов. Семантика диаграмм взаимодействия.

Состояния. Композиция и декомпозиция диаграмм взаимодействия. Формализация сценариев посредством состояний.

^ Архитектурные модели. Понятие архитектуры системы. Архитектуры системы и эволюция системы. Понятие устойчивости системы к изменениям. Компоненты системы с точки зрения информации, управления и представления. Функциональный и объектно-ориентированный подходы к организации системы. Компоненты трех видов: интерфейсные, информационные и управляющие. Выявление компонентов каждого вида. Неформальные архитектурные диаграммы.

^ Язык спецификаций и описаний (SDL). Средства описания архитектуры программной системы. Средства описания поведения программной системы. Структурные компоненты. Каналы. Сигналы, списки сигналов. Структурные типы и пакеты. Формализация архитектурных моделей.

Концепция взаимодействующих конечных автоматов. Процесс как носитель поведения. Входной порт процесса. Состояния и переходы. Помеченные переходы.

Типы данных в языке SDL. Базовые типы, структуры, массивы, таблицы, множества. Операции работы с данными. Определение переменных. Условия.

Динамическая семантика языка SDL.

^ Верификация SDL моделей. Динамическое выполнение SDL спецификации. Верификация сценарной модели.

Литература

Основная:

Кузьменкова Е.А., Петренко А.К. Формальная спецификация программ на языке RSL (методическое пособие по практикуму) – М.: Издат. отдел факультета ВМК МГУ, 2000.
Кузьменкова Е.А., Петренко А.К. Формальная спецификация программ на языке RSL (конспект ллекций) – М.: Издат. отдел факультета ВМК МГУ, 2001.
Мансуров Н.Н., Майлингова О.Л. Методы формальной спецификации программ: языки MSC и SDL – М.: Издат. отдел факультета ВМК МГУ, 1998.
Мейер Б. Объектно-ориентированное конструирование программных систем.: Пер. с англ.: – М.: "Русская Редакция", 2005, 1232 стр.
Бейзер Б. Тестирование черного ящика. Технологии функционального тестирования программного обеспечения и систем – СПб.: Издательство: Питер, 2004г., 320 стр.

Дополнительная:

The RAISE specification language. Prentice Hall, 1992.
RAISE Tools Reference Manual. LACOS/CRI/DOC/13/1/V2, 1994.
Лисков Б., Дж. Гатэг. Использование абстракций и спецификаций при разработке программ – М.: Мир, 1989.
Хоар Ч., Взаимодействующие последовательные процессы – М.: Мир, 1985.
Jacobson I. Object Oriented Software Engineering, Addison-Wesley, 1996.
Карабегов А.В., Тер-Микаэлян Т.М., Введение в язык SDL – М.: Радио и связь, 1993.
ITU-T Recommendation Z.100. Specification and Description Language (SDL), Geneva, 1993.
ITU-T Recommendation Z.120. Message Sequence Chart (MSC), Geneva, 1992.

Похожие:

	Ориентирование в пространстве и глазомерная съемка местности Сезонная полевая практика выполняется в 1 семестре (2 часа), зимняя и весенняя – во 2 семестре (4 часа)		Курс, 4-й семестр лекции (32 часа), зачет без оценки практикум на... Большое внимание уделяется трансляторам: рассматриваются элементы теории формальных языков и грамматик, их применение при построении...
	Программа специального курса «экспериментальные методы физической... «Основы термохимии» (всего 64 учебных часа, из них лекции – 34 ч, семинары – 6 ч, лабораторные занятия – 24 ч) предназначен для студентов...		Курс, 1 поток, 5-й семестр лекции (34 часа), экзамен В курсе обсуждаются общие вопросы систем управления базами данных (субд) и основы реляционных баз данных: введение в реляционные...
	Спецкурс для студентов-специалистов, читается в осеннем семестре. Лекции читаются 24 часа Целью курса является приобретение фундаментальных знаний в области построения программных систем с использованием современных языков...		Методы оптимизации, 3 курс Семинары (36 часов) проводятся в 6 семестре в учебной группе кафедры оптимального управления
	Программа курса «физическая и коллоидная химия» Курс «Физическая и коллоидная химия» (лекции – 28 ч, лабораторные – 26 ч) предназначен для студентов 2-го курса георафического факультета...		Контрольная работа 2 часа Аттестация участников (зачет) 2 часа По... Инн 2723112937 кпп 272301001 р/счет 40703810801560000705 в Филиале №2754 втб 24 (зао)
	Информационный бюллетень "новые медицинские книги в библиотеке вгма" 2-3 квартал 2009 г Основы медицинских знаний. Лекции и семинары : учебно-практическое пособие / И. М. Авраменко. Ростов н/Д. Феникс, 2008. 155 с. (Серия...		Курс, 1-й семестр лекции (51 час), экзамен практикум на ЭВМ (68 часов),... Рассматриваются формальные модели алгоритмов (машина Тьюринга, алгоритмы Маркова), язык программирования Паскаль, основные структуры...

Вы можете разместить ссылку на наш сайт:
Школьные материалы