М Е Т О Д Ы Ф О Р М А Л Ь Н О Й С П Е Ц И Ф И К А Ц И И

П Р О Г Р А М М

Курс, для которого читается, потоки: 4 курс, 3 поток.

Часы по семестрам: 7 семестр √ 34,

8 семестр √ 30.

Семинары в поддержку курса (часы): 7 семестр √ 34,

8 семестр √ 30.

ПЕРВАЯ ЧАСТЬ.

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

Строгий подход к индустриальной программной инженерии - RAISE методология и язык RSL. Типы, аксиомы, значения. Абстракция и уточнение. Параллельность. Недетерминизм и ╚недоспецификация╩.

Тестирование: традиционный подход. Методы ╚черного╩ и ╚белого╩ ящиков╩. Критерии полноты тестового покрытия. Декомпозиция тестовых наборов. Тестирование конечного автомата. Model checking (анализ моделей). Формальные спецификации и генерация тестов.

Динамическая верификация программ. Автоматическая генерация тестов на основе формальных спецификаций программ. Классы критериев покрытия. Генерация тестовых вариантов. Генерация тестовых драйверов. Генерация ╚оракулов╩. Генерация тестовых последовательностей.

Темпоральные спецификации. Темпоральные логики. Исчисление длительностей. Полный цикл проектирования: спецификация требований и предположений, модель и стратегия управления, корректность стратегии управления.

Литература.

1. Кузьменкова Е.А., Петренко А.К. Формальная спецификация программ на языке RSL (методическое пособие по практикуму), Издат. отдел факультета ВМиК МГУ, (готовится к печати в 1999).
2. The RAISE specification language. Prentice Hall, 1992.
3. RAISE Tools Reference Manual. LACOS/CRI/DOC/13/1/V2, 1994.

ВТОРАЯ ЧАСТЬ.

(см. материалы ко второй части курса)

Составители программы: доцент Н.Н. Мансуров

канд. физ.-мат- наук А.К. Петренко