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

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

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

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

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

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

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

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

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

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

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

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

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

13 13 ВМиК МГУ, Сентябрь-декабрь 2002 А.К.Петренко. Формальные спецификации программ - I. Лекция 1 Модель vs. Спецификация Модель – материальная или ментальная сущность, использующаяся для проектирования или анализа свойств целевой системы (реализации) Спецификация – описание (представление) модели (спецификация задает модель) Спецификация – описание свойств реализации с точностью до уровня абстракции, заданного моделью. Для краткости «модель» и «спецификация» часто рассматриваются как синонимы

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

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

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

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

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