Лекция Методы разработки ПО

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко2 План лекции Методы разработки ПО Пример: метод пошаговой детализации Критерии выбора метода разработки ПО Эволюция методов разработки ПО RAISE: пример метода разработки ПО с использованием формальных спецификаций

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко3 Методы разработки ПО Прежде чем подробно изучать язык, необходимо составить представление о том, для чего он предназначен, как его использовать Язык обычно сопряжен с некоторым методом разработки ПО. Языки формальных спецификаций не являются исключением из этого правила

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко4 Методы разработки ПО Метод – процедура или процесс, направленные на достижение цели (Merriam-Websters Collegiate® Dictionary) В нашем случае цель – разработка ПО, удовлетворяющего заданным характеристикам

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко5 Метод пошаговой детализации (МПД) МПД – один из первых методов разработки ПО, который был рекомендован для промышленного применения Идея – постепенное, пошаговое уточнение описания системы Использование «псевдокода»

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко6 Пример: МПД – шаг 0 Задача: Произвести запуск искусственного спутника Земли (ИСЗ)

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко7 Пример: МПД – первый шаг детализации Задача разбивается на подзадачи: 1. Произвести пуск 2. Выполнить полет в орбитальном режиме 3. Произвести спуск

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко8 Пример: МПД – второй шаг, подзадача Произвести тестирование наземного комплекса 1.2. Если обнаружены проблемы то отменить запуск (стоп) 1.3. Ввести полетное задание 1.4. Стартовать выполнение полетного задания

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко9 Пример: МПД – второй шаг, подзадача Вывести на орбиту 2.2. Если параметры орбиты нормальные то начать выполнение программы орбитального режима (перейти к 2.3) иначе стартовать программу аварийного спуска (перейти к 2.4)

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко10 Пример: МПД – второй шаг, подзадачи 3 и Выполнить программу орбитального режима 2.4. Выполнить программу снижения и посадки 2.5. Завершить работу (стоп)

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко11 Критерии выбора метода разработки ПО Надежность разрабатываемого ПО Эффективность (быстродействие, точность,...) разрабатываемого ПО Скорость разработки ПО Стоимость разработки ПО Соотошение цена/качество/скорость Технологичность... (и т.д.)

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

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

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

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко15 Эволюция методов разработки ПО: примеры Основным недостатком МПД явилась сложность контроля – результаты, поддающиеся оценке, появляются только на поздних стадиях На смену МПД пришел метод быстрого прототипирования, но у него проблемы с масштабируемостью Виток спирали: появление формальных методов – МПД на новом уровне

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко16 Возвращаясь к языкам формальных спецификаций Языки формальных спецификаций позволяют: строить модели и уточнять их при помощи ограничений на структуры данных описывать интерфейсы моделей в виде алгебраических спецификаций (аксиомы) неявных спецификаций (пред-, постусловия) явных спецификаций (алгоритмы)

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

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко18 RAISE Development Method – основные идеи Разработка разбивается на шаги Сначала описывается максимально простая и абстрактная модель На каждом шаге строится более подробная и конкретная модель На каждом шаге проверяется согласованность моделей

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко19 RAISE Development Method – шаги процесса разработки Шаг 0: объявление сорт-типов и определение сигнатур операций Шаг 1: аксиомы, алгебраическая спецификация Шаг 2.1: структуры данных и раздельные спецификации для каждой операции (имплицитные и эксплицитные), доказательство согласованности спецификаций шага 2.1 и шага 1... Шаг 2.i: детализация и расширение спецификаций предыдущего шага и доказательство согласованности с предыдущим шагом и с шагом 1. В конце возможна даже трансляция в код на языке программирования.

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко20 Шаги RAISE метода Шаг 0 Шаг 2.1 Шаг 1 Шаг 2.i... Проверка согласованности

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко21 RAISE Development Method – проверка согласованности Этому вопросу посвящена вся следующая лекция

ВМиК МГУ, сентябрь-декабрь 2002 Формальные спецификации программ-I, Лекция 4. А.К.Петренко22 Рефлексия Вопрос: каковы основные возможности RAISE мы уже изучили? Вопрос: чего еще не хватает, для того чтобы RAISE мог быть использован для разработки промышленного ПО? ЗнаюУточняю (дома) ЗнаюУточняю (дома)