Документ взят из кэша поисковой машины. Адрес оригинального документа : http://sp.cs.msu.ru/courses/progs2006/form_spec.doc Дата изменения: Tue Jul 7 15:58:40 2009 Дата индексирования: Mon Oct 1 21:51:57 2012 Кодировка: koi8-r

Методы формальной спецификации программ
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 спецификации.
Верификация сценарной модели.

Литература


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

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