Формальные спецификации программ. А.К.Петренко МГУ ВМиК, ИПМ РАН, ИСП РАН

Лекция 1 Введение. Место формальных спецификаций в промышленной разработке ПО

3 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Кластер термина «Формальные спецификации программ»

4 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 План лекции Есть ли разница между программированием и машиностроением ? Проблемы разработки ПО Моделирование и спецификация Формализация Языки формальных спецификаций Структура курса

5 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Различия в организации производства в программировании и в машиностроении

6 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Проблемы современной индустрии ПО ПО Новые приложения Качество Сроки Стоимость Надежность Соответствие требованиям Первая версия Очередная версия Собственно разработка Дополнительная работа re-work Описание требований Управление требованиями Верификация Валидация

7 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Производство ПО. Процессы «прямой инженерии» Основной поток работ Дополнительные поток - re-work Анализ требований Спецификация системы Приемные испытания Системное проектирование Реализация ПО Проектирование ПО Комплексирование Системное тестирование Тестирование модулей

8 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Как снизить стоимость дополнительного потока? Стоимость исправления ошибки зависит от «расстояния» между моментом ее возникновения и моментом обнаружения. Формальные методы дают возможность сократить латентный период существования ошибок за счет: моделирования и приемов и средств анализа

9 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Виды использования моделей жизненном цикле ПО

10 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Спецификация - основные принципы Абстракция (abstraction) Строгость (rigour) Формальность (formality)

11 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Абстракция в строительной инженерии При моделировании мостов отвлекаются (абстрагируются) от Знаю УточняюУзнал

12 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Абстракция в программировании При моделировании Системы Резервирования Билетов (СРБ) отвлекаются (абстрагируются) от Знаю УточняюУзнал

13 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Абстракция в программировании. Пример Неформальная постановка задачи: СРБ используется транспортными агентами. В СРБ вводятся данные о пунктах вылета и назначения, о дате и времени полетов. Система контролирует соответствие заказов расписанию рейсов и тарифам. Абстракция: Совокупность пунктов вылета и назначения представлена графовой структурой. Каждый узел содержит ссылки на узлы, соответствующие пунктам назначения. Расписание рейсов представлено hash- таблицей...

14 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Строгость Модель/ спецификация должна позволять Объективный анализ Воспроизводимость анализа Машинную поддержку Язык спецификаций должен быть строго определен

15 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Формальность Под «формальностью» мы понимаем возможность строить модели, анализировать их свойства однозначным образом. Формальность должна допускать широкий набор методов анализа, включая математические доказательства. Это подразумевает формальное определение семантики языка спецификаций.

16 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Кластер термина «Формальные спецификации программ»

17 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 План курса Введение в формальные методы разработки ПО Язык RSL и RAISE метод Формальные спецификации в тестировании и реверс-инженерии Общие вопросы тестирования Тестирование на основе спецификаций Спецификация наследованного ПО

18 ВМиК МГУ, Сентябрь-декабрь 2001 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Интернет ресурсы (в русском варианте см. Лекции...) 01/csc227/ /csc227/