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

Презентация:



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

Лекция Методы разработки ПО. ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко2 План лекции Методы разработки.
Постановка задачи Построение алгоритма Составление программы на языке программирования О т л а д к а и тестирование программы Математическая формализация.
Языки и методы программирования Преподаватель – доцент каф. ИТиМПИ Кузнецова Е.М. Лекция 7.
Разработка программного обеспечения (Software Engineering) Часть 2. Создание ПО.
Онтологии: понятие, методы, применение. Онтологии предметных областей. Лекция 5.
Структурный подход к программированию Подготовила студентка группы Э-108 Правилова Анастасия.
Лекция RAISE Development Method: некоторые виды спецификаций и проверка согласованности моделей.
1 Курс: Модели и методы дискретной оптимизации Лектор: д.т.н., профессор Овчинников Владимир Анатольевич Структура курса: 17 лекций – 17 семинаров – экзамен.
1 МОДЕЛИРОВАНИЕ ПРОЦЕССОВ УПРАВЛЕНИЯ ПРОЕКТАМИ ПО РАЗРАБОТКЕ ПРОДУКЦИИ НА ОСНОВЕ CALS и CASE ТЕХНОЛОГИЙ (Курсовая работа) «Проектирование интегрированных.
9 класс Урок 4 Матвеева В.П.. Постановка задачи Построение алгоритма Составление программы на языке программирования О т л а д к а и тестирование программы.
Этапы моделирования. Постановка задачи: Описание задачи; Цель моделирования; Анализ объекта Разработка информационной модели Разработка компьютерной модели.
Даталогическое проектирование. 1. Представление концептуальной модели средствами модели данных СУБД Общие представления о моделях данных СУБД С одной.
Жизненный цикл программного обеспечения Подготовил студент 1 курса Лось Павел.
Жизненный цикл программного обеспечения Лекция 4.
Алгоритмизация и требования к алгоритму Алгоритм и алгоритмизация Алгоритм и алгоритмизация.
Дисциплина «Технология разработки программного обеспечения» Тема 1 « Основы разработки Тема 1 « Основы разработки программного продукта » программного.
Н.В. Курмышев, С.В. Попов МОДЕЛЬ ОРГАНИЗАЦИИ ПРАВ ДОСТУПА В ВЕБ-ПРИЛОЖЕНИЯХ ДЛЯ ДИСКРЕЦИОННЫХ И РОЛЕВЫХ СХЕМ Новгородский государственный университет Докладчик:
РАЗРАБОТКА ЭЛЕКТРОННОГО КУРСА ПО UML– ПРОЕКТИРОВАНИЮ. МОДЕЛЬ КУРСА С ТОЧКИ ЗРЕНИЯ ДИАГРАММ АКТИВНОСТИ И ВАРИАНТОВ ИСПОЛЬЗОВАНИЯ. БУДИНКЕВИЧ А. В. НАУЧНЫЙ.
Языки и методы программирования Преподаватель – доцент каф. ИТиМПИ Кузнецова Е.М. Лекция 8.
Транксрипт:

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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