Разделы презентаций
- Разное
- Английский язык
- Астрономия
- Алгебра
- Биология
- География
- Геометрия
- Детские презентации
- Информатика
- История
- Литература
- Математика
- Медицина
- Менеджмент
- Музыка
- МХК
- Немецкий язык
- ОБЖ
- Обществознание
- Окружающий мир
- Педагогика
- Русский язык
- Технология
- Физика
- Философия
- Химия
- Шаблоны, картинки для презентаций
- Экология
- Экономика
- Юриспруденция
Формальные спецификации программ
Содержание
- 1. Формальные спецификации программ
- 2. ЛекцияВведение. Место формальных спецификаций в промышленной разработке ПО
- 3. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ - I. Лекция 1Кластер термина «Формальные спецификации программ»
- 4. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 5. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ - I. Лекция 1Проблемы современной индустрии ПО
- 6. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ - I. Лекция 1Производство ПО. Процессы «прямой инженерии»
- 7. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 8. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ - I. Лекция 1Виды использования моделей жизненном цикле ПО
- 9. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 10. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 11. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 12. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 13. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 14. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 15. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 16. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ - I. Лекция 1Кластер термина «Формальные спецификации программ»
- 17. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ -
- 18. ВМиК МГУ,Сентябрь-декабрь 2002А.К.Петренко. Формальные спецификации программ - I. Лекция 1Интернет ресурсыhttp://www.ispras.ru/~RedVerst/ (в русском варианте см. Лекции...)http://coursework.cs.ncl.ac.uk/module/2004/CSC264
- 19. Скачать презентанцию
ЛекцияВведение. Место формальных спецификаций в промышленной разработке ПО
Слайды и текст этой презентации
Слайд 3ВМиК МГУ,
Сентябрь-декабрь 2002
А.К.Петренко. Формальные спецификации программ - I. Лекция 1
Кластер
термина
Слайд 4ВМиК МГУ,
Сентябрь-декабрь 2002
А.К.Петренко. Формальные спецификации программ - I. Лекция 1
План
лекции
Разработка ПО как отрасль промышленности
Проблемы разработки ПО
Моделирование и спецификация
Формализация
Структура курса
Слайд 5ВМиК МГУ,
Сентябрь-декабрь 2002
А.К.Петренко. Формальные спецификации программ - I. Лекция 1
Проблемы
современной индустрии ПО
Слайд 6ВМиК МГУ,
Сентябрь-декабрь 2002
А.К.Петренко. Формальные спецификации программ - I. Лекция 1
Производство
ПО. Процессы «прямой инженерии»
Слайд 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
Интернет
ресурсы
http://www.ispras.ru/~RedVerst/ (в русском варианте см. Лекции...)
http://coursework.cs.ncl.ac.uk/module/2004/CSC264
