Электронная библиотека диссертаций и авторефератов России
dslib.net
Библиотека диссертаций
Навигация
Каталог диссертаций России
Англоязычные диссертации
Диссертации бесплатно
Предстоящие защиты
Рецензии на автореферат
Отчисления авторам
Мой кабинет
Заказы: забрать, оплатить
Мой личный счет
Мой профиль
Мой авторский профиль
Подписки на рассылки



расширенный поиск

Математическое моделирование верификации процесса разработки программного обеспечения Григорьев Михаил Викторович

Математическое моделирование верификации процесса разработки программного обеспечения
<
Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения Математическое моделирование верификации процесса разработки программного обеспечения
>

Диссертация - 480 руб., доставка 10 минут, круглосуточно, без выходных и праздников

Автореферат - бесплатно, доставка 10 минут, круглосуточно, без выходных и праздников

Григорьев Михаил Викторович. Математическое моделирование верификации процесса разработки программного обеспечения : диссертация ... кандидата технических наук : 05.13.18 / Григорьев Михаил Викторович; [Место защиты: Тюмен. гос. ун-т].- Тюмень, 2009.- 135 с.: ил. РГБ ОД, 61 09-5/2216

Содержание к диссертации

Введение

Глава 1 Обзор методов и алгоритмов верификации программной инженерии .. 9

1 Методологии разработки программного обеспечения 9

2 Верификация процесса разработки программного обеспечения 18

3 Описание семантики процесса разработки 23

4 Комплексы поддержки программной инженерии 27

Выводы 30

Глава II Математическая модель верификации процесса программной инженерии 32

1 Модель разработки программного обеспечения 32

2 Динамическая модель процесса разработки программного обеспечения ...40

Выводы 51

Глава III Модель семантических отношений между артефактами проекта 53

1 Метод оценки корректности рабочих продуктов 53

2 Язык определения семантических отношений артефактов 54

3 Компилятор языка семантических отношений артефактов 61

Выводы 67

Глава IV Программный комплекс поддержки разработки программного обеспечения 69

1 Архитектура программного комплекса 69

2 Описание модулей программного комплекса 76

Выводы 85

Глава V Апробация программного комплекса 86

1 Модификация унифицированного процесса разработки программного обеспечения 86

2 Проведение эксперимента 92

3 Правила верификации процесса разработки программного обеспечения .92

4 Практика использования программного комплекса в учебных проектах...95

Выводы 104

Выводы по диссертационной работе 106

Список источников и литературы 108

Приложение

Введение к работе

Актуальность работы. В современной индустрии программного обеспечения огромное внимание уделяется процессу разработки, который сформировал в последние десятилетия самостоятельную область знаний «Программная инженерия» (В.В. Липаев, Л.А. Мацяшек, P. Naur, В. Randell, D. Parnas, W. Stevens, G. Myers, L. Constantine, А. Шалыто, И. Соммервилл, С. Бобровский и др.). На сегодняшний день нет устоявшихся принципов организации процесса разработки, многие организации пропагандируют собственные методы и процессы программной инженерии (SWEBOK, CMMI, MSF, MDA, RUP и т.д.). В тоже время большинство методологий оценивает качество организации процесса разработки по качеству программного продукта (Е.В. Крылов, В.А. Острейковский, Н.Г. Типикин, П.М. Дюваль, С. Матиас, Э. Гловер и др.).

Существует множество методов инспектирования, позволяющих выявить проблемы и недостатки программных продуктов (ГОСТ Р ИСО 9000, ГОСТ Р ИСО/МЭК 15288, ГОСТ Р ИСО/МЭК 12207, ISO/IEC TR 15504, IEEE Std 1059, С. Орлик и др.). Верификация программного обеспечения известна и широко используется (СВ. Синицын, Н.Ю. Налютин, Э.М. Кларк, О. Грамберг, Д. Пелед, Дж. Сифакис и др.). Метод верификации предоставляет эффективные средства локализации проблем программного обеспечения и поиска их потенциального решения (Е. Ashcroft, S. Owicki, D. Gries, A. Pnueli, C. Jones). Верификация процесса разработки не выделена в самостоятельный процесс программной инженерии. Требуется изучить процесс разработки программного обеспечения и создать механизм его верификации.

Практичность программной инженерии складывается из многочисленных аспектов, связанных как с особенностями организации процессов разработки программного обеспечения, так и с реализацией

конечных продуктов. В работах Б. Боэма, Р. Фатрелла, Э. Брауде, Л. Локвуда, Д. Шафера убедительно показано, что успешная разработка программного обеспечения зависит не только от получения удачного программного продукта, но также от получения удачных процессов разработки программных систем. При отсутствии обратной связи и усовершенствований даже самый практичный проект обречен на неудачу. Существуют методы, которые косвенным образом дают возможность оценить качество организации процессов: аттестация, аудит, валидация, верификация, рецензирование, тестирование, экспертиза. Как правило, эти методы привязаны лишь к некоторым дисциплинам программной инженерии и носят декларативный характер.

Современный уровень формализации методов программной инженерии создает все предпосылки для разработки формальных методов инспектирования качества организации процесса разработки программного обеспечения.

Целью работы является повышение качества программной инженерии путем формализации верификации процесса командной разработки проектов.

Для достижения поставленной цели определены следующие задачи исследования:

  1. модификация модели процесса разработки для обеспечения возможности проверки корректности организации процессов программной инженерии;

  2. создание метода инспектирования процесса разработки программного обеспечения и построение математической модели, формализующей этот метод;

  3. разработка комплекса программ поддержки процесса создания программного обеспечения в команде, который позволит проводить оценку организации этого процесса;

  4. проведение испытания программного комплекса, с целью проверки адекватности разработанных методов и моделей.

Методы исследований. При решении поставленных задач использовались эффективные математические методы теории формальных языков и автоматов, алгебры темпоральной логики, теории компиляторов, теории графов.

Достоверность и обоснованность результатов подтверждается
использованием и применением опробованных методов проектирования и
разработки информационных систем, унифицированного языка
моделирования, архитектуры, управляемой моделями, а также
вычислительным экспериментом, подтвердившим адекватность

предложенного метода верификации и математических моделей, реализующих его.

Научная новизна работы заключается в следующем:

  1. модифицирована метамодель процесса инжиниринга программного обеспечения, которая дает возможность реализовать верификацию процесса за счет идентификации отношений между артефактами разработки;

  2. разработан метод верификации процесса создания программного обеспечения, основанный на выявлении пути в модели Крипке с помощью алгебры темпоральной логики, что дает возможность отобразить динамику процесса в пространстве артефактов;

  3. обосновано архитектурное решение проверки семантических отношений артефактов проекта путем оценки выполнения правил, записанных в грамматике формального языка ограничений.

Практическая значимость работы:

1) разработан компилятор языка fOCL, который позволяет выявить
синтаксические и семантические ошибки при написании правил
взаимодействия рабочих продуктов. Интеграция

скомпилированного правила дает возможность выполнять проверку артефактов в однозначных проектах без модификации самого правила;

  1. создан программный комплекс, организация которого впервые охватывает все уровни архитектуры моделирования Object Management Group (OMG), позволяющий выполнить верификацию процесса командной разработки проектов;

  2. модифицирован унифицированный процесс разработки программного обеспечения для небольших проектных групп, который включает предложенный метод верификации процесса создания программного обеспечения.

Реализация и внедрение результатов работы. Комплекс программ опробован в курсе «Проектирование информационных систем» при подготовке студентов по специальности 080801.65 «Прикладная информатика в экономике», что подтверждается соответствующим актом внедрения, выданным Тюменским государственным университетом. Модифицированный унифицированный процесс для небольших проектных групп внедрен в виде методического пособия по предмету «Проектирование информационных систем», на которое получен гриф УМО для специальности «Прикладная информатика (по областям)».

Апробация работы. Основные результаты диссертационной работы были представлены на следующих научных конференциях: Всероссийская научная конференция молодых ученых «Наука. Технологии. Инновации» (Россия, Новосибирск, декабрь 2006); Межвузовская научно-практическая конференция студентов, аспирантов и молодых ученых «Безопасность информационного пространства» (Россия, Тюмень, ноябрь 2007); Всероссийская научно-практическая конференция с международным участием «Дистанционные образовательные технологии: опыт применения и перспективы развития» (Россия, Тюмень, февраль 2008); Научно-практическая конференция молодых ученых «Современные проблемы математического и информационного моделирования. Перспективы разработки и внедрения инновационных IT-решений» (Россия, Тюмень, май

2008); Научно-методические семинары кафедры информационных систем Тюменского государственного университета (2005-2009 гг.).

Публикации. Основное содержание работы отражено в 13 публикациях, из которых 3 свидетельства о государственной регистрации программы для ЭВМ и 1 статья, опубликованная в журнале из списка ВАК.

Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы. Объем диссертации составляет 119 страниц, содержит 34 рисунка, 3 приложения. В библиографии представлено 113 наименований работ российских и зарубежных авторов.

Верификация процесса разработки программного обеспечения

OpenUP делит жизненный цикл проекта на четыре фазы: начальная фаза, фазы уточнения, конструирования и передачи. Жизненный цикл проекта обеспечивает предоставление заинтересованным лицам и членам коллектива точек ознакомления и принятия решений на протяжении всего проекта. Это позволяет эффективно контролировать ситуацию и вовремя принимать решения о приемлемости результатов. План проекта определяет жизненный цикл, а конечным результатом является окончательное приложение. OpenUP делит проект на итерации: планируемые, ограниченные во времени интервалы, длительность которых обычно измеряется неделями. План итерации определяет, что именно должно быть сдано по окончании итерации, а результатом является работоспособная версия. Коллективы разработчиков OpenUP строятся по принципу самоорганизации, решая вопросы выполнения задач итераций и передачи результатов. Для этого они сначала определяют, а затем решают хорошо детализированные задачи из списка элементов работ. Базовый процесс OpenUP является независимым от инструментов, малорегламентированным процессом, который может быть расширен для удовлетворения потребностей широкого диапазона типов проектов [77].

Методология Dynamic System Development Method Dynamic System Development Method (DSDM) основан консорциумом из 17 английских компаний, пропагандирующим RAD и принципами итеративной разработки- [76, 81, ПО]. Процесс DSDM делится на три взаимосвязанных цикла: цикл функциональной модели отвечает за создание аналитической документации и прототипов, цикл проектирования и конструирования — за приведение системы в рабочее состояние, и наконец, последний цикл — цикл реализации — обеспечивает развертывание программной системы. Базовые принципы, на которых строится DSDM, это активное взаимодействие с пользователями, частые выпуски версий, самостоятельность разработчиков в принятии решений и тестирование в течение всего цикла работ. Как и большинство других гибких методологий, DSDM использует короткие итерации, продолжительностью от двух до шести недель каждая. Особый упор делается на высоком качестве работы и адаптируемости к изменениям в требованиях. Agile-методологии

Agile-методология разработки представляет собой концептуальный каркас, в рамках которого выполняется разработка программного обеспечения. Требования к программному обеспечению очень изменчивы в процессе его создания. Для этого продукт и система его создания должны быть гибкими для своевременных изменений и учета новых требований. Методы agile позволяют разрабатывать гибкие процессы по разработке программного обеспечения, которые отвечают требованиям современного бизнеса. Методология Agile нацелена на минимизацию рисков путем сведения разработки к серии коротких итераций, которые обычно длятся одну-две недели. Каждая итерация сама по себе выглядит как программный проект в миниатюре, и включает все задачи, необходимые для выдачи мини-прироста по функциональности: 1) планирование; 2) анализ требований; 3) проектирование; 4) кодирование; 5) тестирование; 6) документирование.

Хотя отдельная итерация, как правило, недостаточна для выпуска новой версии продукта, подразумевается что гибкий программный проект готов к выпуску в конце каждой итерации. По окончании каждой итерации, команда выполняет переоценку приоритетов разработки [15, 28, 78]. Методология SCRUM

Гибкая методология разработки программного обеспечения SCRUM используется с целью улучшения продуктивности команды разработчиков, делая упор не на качественно определенный, а на качественно контролируемый процесс разработки [76, 110]. Методология Object Management Group

Model Driven Architecture (MDA) - методология OMG, основной концепцией которой является разработка на базе моделей. Подход MDA состоит в применении четырехуровневой архитектуры моделирования, определяющей обязанности каждого уровня, и формировании для этого полной цепочки необходимых инструментов. Данная методология поддерживается ведущими вендорами. Применение данной методологии гарантирует реализацию исполняемых моделей и определяет структуру процессов разработки крупнейших компаний-разработчиков программного обеспечения [55, 56].

Динамическая модель процесса разработки программного обеспечения

Для выполнения верификации необходимо задать оценку каждого состояния системы. Последовательность положительных оценок различных состояний будет свидетельствовать о корректном (допустимом) выполнении процесса. Поскольку состояние процесса характеризуется набором артефактов, для выставления оценки состояния необходимо оценить каждый артефакт в отдельности, и, на основании выставленных оценок дать совокупную оценку, характеризующую состояние. Утверждение 2. Оценка корректности рабочего продукта, должна включать результат проверки правильности его разработки, что требует формирования системы формальных правил оценки процесса разработки. В модели (2.2) каждый рабочий продукт связан со следующим некоторым отношением, проверка корректности артефакта осуществима за счет проверки семантических отношений, их связывающих, посредством формализации правил проверки отношений, формирующих систему правил для всего процесса. Утверждение доказано. Однако не достаточно только указать на неправильное выполнение процесса, нужно определить место возникновения ошибки (ошибок), которые привели к неправильной реализации процесса. Это требует рассмотрения реализации каждого артефакта в отдельности. Таким образом, появляется возможность выявления первопричины ошибки. Для возможности проверки артефактов должны существовать формальные правила, проверка которых позволяет сформировать оценку отдельного артефакта. Для оценки состояния процесса разработки нужно оценить путь достижения этого состояния. Данный путь может содержать изменение нескольких артефактов.

Процедура верификации заключается в проверке правильности разработки артефактов, таким образом, осуществляется оценка корректности пути осуществления проектной деятельности. Результатом верификации будет последовательность изменения оценок артефактов. Утверждение 3. Динамическая модель процесса разработки программного продукта, включающая оценку корректности артефакта, может быть представлена в виде модели Крипке. Формализация поведения динамической системы задается моделью Крипке. Большинство современных методов верификации программного и аппаратного обеспечения базируются на обходе всевозможных состояний системы, представленной в виде модели Крипке [89-92]. Основу модели представляет граф, вершины которого представляют состояния системы, дуги — переходы между состояниями.

Функция интерпретации отображает каждую вершину во множество свойств, соответствующих состоянию. Модель Крипке представляется четверкой: где: S — конечное множество состояний, S0 Q S — множество начальных состояний, R Q S X S - отношение переходов, где Vs Є S, 3s Є S, такое что 0,s ) ЄЯ, L:S 2AP - функция интерпретации, сопоставляющая каждому состоянию s Є S набор атомарных высказываний L(s), истинных в s. Для набора оценок артефактов, совокупность которых представляет состояние процесса, модель Крипке будет иметь следующий вид: где: S — множество состояний процесса разработки; S0 Q S — начальное состояние; R с 5 х S - отношение переходов для всевозможных состояний, т.е. для каждого состояния s Є S должно существовать такое состояние s Є S, что имеет место R(s, s ); T:S - 2VR - функция интерпретации состояния системы как набора оценок артефактов; VR - набор оценок артефактов, соответствующий атомарным высказываниям модели Крипке. Для известного состояния процесса разработки необходимо сформировать все возможные состояния артефактов, переходы между которыми определяют все возможные пути реализации процесса. Оценка пути проверяет корректность (допустимость) способа выполнения процесса. Состояние процесса может быть описано при помощи оценок: s: WP - В. По заданной оценке можно записать формулу первого порядка, истинную для этой оценки.

Компилятор языка семантических отношений артефактов

Разработка выражений на языке ГОСЬ должна сопровождаться преобразованием исходного текста правил в исполняемый код (компиляцией). Набор правил может уточняться и дополняться, следовательно, ставится задача создания компилятора, позволяющего получать машинный код, эквивалентный исходным правилам [39].

Обобщенная структура компилятора представляет собой последовательность из 6 этапов, представленных на рис. 3.1 [84, 85]: Рис. 3.1. Общая структура компилятора В силу того, что компилятор предназначен для генерации кода на основе узкоспециализированного языка, имеющего жесткую структуру не позволяющего создания пользовательских процедур, нецелесообразна реализация модулей генерации промежуточного кода и оптимизатора кода. Таким образом, структура компилятора языка fOCL будет иметь вид в соответствии с рис. 3.2.

Структура компилятора языка fOCL Компилятор языка fOCL реализован в виде 4 модулей: лексический анализатор, синтаксический анализатор, семантический анализатор, генератор целевого кода.

Полученная последовательность лексем передается синтаксическому анализатору, который, в свою очередь, проверяет, может ли данный поток быть порожденным грамматикой языка, используя дерево синтаксического разбора (рис. 3.3).

На этапе семантического анализа компилятор обращается непосредственно к используемой объектной модели с целью сопоставления конструкций выражения элементам модели. При этом также осуществляется проверка взаимодействия классов исходной модели, используя отношение ассоциации.

Объектная модель, представленная в графической нотации UML, преобразуется в специальный формат обмена XML Metadata Interchange (XMI), представляющий собой структурированный XML-файл, изоморфный исходной модели (приложение В, листинг 1). Анализатор обращается к содержимому файла, извлекает информацию о классах, полях и методах каждого класса и дополняет дерево синтаксического разбора полученными элементами (рис. 3.4). При включении элементов в дерево производится проверка выражения действительным ассоциациям используемых классов.

Далее синтаксическое дерево проверяется на соответствие типам. Язык использует: 1) набор стандартных типов (Integer, Real, Boolean, String) - для описания конструкций; 2) дополнительные типы (OclVoid, OclElement, OclType, Unlimitedlnteger, Collection, Set, OrderedSet, Bag, Sequence) - для реализации возможности взаимодействия с данными используемых моделей; 3) специальные типы (OclAny, Ocllnvalid, OclMessage, ExpressionTnOcl) — для реализации вывода сообщений компилятора (например, сообщений об ошибках компиляции).

Используя контекстно-свободную формальную грамматику языка, определяются типы данных для всех нетерминалов синтаксического дерева [98, 99]. Под нетерминалом понимается выражение языка, не имеющее конкретного символьного значения. Схема трансляции, описываемая в грамматике, позволяет определить тип для синтезируемых узлов дерева и порождаемых атрибутов. Все полученные идентификаторы исходного текста программы записываются в таблицу символов с указанием их типа. При несовпадении типов или невозможности их приведения выражению назначается тип Ocllnvalid, используемый для определения ошибки.

Результатом стадии семантического анализа является синтаксическое дерево, дополненное элементами извлечения данных модели, а также таблица символов, содержащая все идентификаторы исходного текста программы с указанием типа для каждого.

Генератор целевого кода основан на методе преобразования дерева. Целевой архитектурой кода выбрана архитектура х86. Данный генератор преобразует дерево, полученное после этапа семантического анализа, таким образом, чтобьг каждый узел дерева мог работать максимум с двумя ячейками памяти или регистрами для хранения объектов. Далее в это дерево вставляются адреса времени выполнения. После такого преобразования каждый лист дерева содержит константу, регистр, ячейку памяти и индекс, указывающий значение атрибута.

Полученное дерево транслируется в набор инструкций целевой архитектуры, используя правила генерации кода. Правила преобразования представляют собой шаблон поддерева и инструкцию, соответствующую данному шаблону. Применяя правила ко всему дереву, реализуя тем самым свертку дерева, генератор получает готовый набор инструкций, соответствующий исходному тексту выражения языка fOCL.

Необходимо отметить, что при возникновении ошибки в тексте компилируемого правила, на любом этапе компиляции разработчику генерируется соответствующее сообщение.

Описание модулей программного комплекса

Стандарт OMG определяет 4 уровневую архитектуру моделирования. Каждый уровень определяет уровень абстракции моделируемого объекта, уровень МЗ определяет представление объекта на верхнем уровне абстракции, уровень М2 описывает модель структуры объекта, уровень Ml представляет функциональный каркас объекта и уровень МО представляет конкретную реализацию моделируемого объекта.

При моделировании процесса разработки программного обеспечения данная архитектура используется для определения структуры процесса разработки на уровне М2, проектирования модели процесса на уровне Ml и реализации экземпляра процесса в модели проекта на уровне МО.

В литературе описываются различные программные решения, позволяющие проводить моделирование процесса на каждом из трех уровней [58, 59, 60, 61]. Однако существующие программные решения не позволяют учитывать изменения метамодели. Таким образом, при модификации модели SPEM, описанной во второй главе, необходимо учитывать расширение набора функциональных характеристик средств моделирования. Поскольку метамодель, описывающая структуру процесса разработки, не регламентирует метод проверки модели проекта, необходимо разработать программный комплекс, учитывающий изменение метамодели процесса и позволяющий проводить его автоматическую верификацию.

Реализация отдельного программного средства для моделирования процесса на каждом уровне позволяет модифицировать отдельные части программного комплекса без изменения всей системы позволяет методика функционального дизайна, гарантирующая реализацию только одной обязанности каждого программного модуля [53].

Поскольку процесс разработки программного обеспечения предполагает командную работу и распределенный обмен артефактами применение клиент-серверной технологии является наиболее оправданным.

Так как программные средства; реализующие уровни моделирования, представляют собой программные модули, описывающие клиент-серверную архитектуру программного комплекса, для их модификации необходимо использовать многоуровневый архитектурный" шаблон, позволяющий детально рассматривать необходимые компоненты модуля [15, 27, 31].

Клиент-серверная многоуровневая архитектура представлена на рис. 4.1. Архитектурная схема комплекса Формирование абстрактной модели процесса разработки осуществляется на втором уровне моделирования. Среда разработки унифицированного процесса использует модифицированную метамодель при определении модели процесса. Среда командной разработки формирует модель процесса. Полученная модель впоследствии проверяется на первом уровне используя правила верификации процесса, описывающего конкретное исполнение абстрактной модели.

Организация верифицируемой командной, разработки программного обеспечения требует реализации модифицированной метамодели процесса, а также создания модели процесса в соответствии с архитектурной схемой. Разработка программного комплекса, реализующего архитектурную модель в виде набора инструментальных средств, позволяет представить реализацию модели процесса проектирования для каждого уровня, обеспечив при этом возможность независимого использования соответствующего функционала. Представление программного комплекса в виде набора отдельных решений позволяет не только определить круг решаемых задач каждого приложения, но и выделить типы взаимосвязей между разрабатываемыми инструментариями. Обмен данными посредством интерфейсов дает возможность повторного использования или модернизации отдельных частей программного комплекса, а также расширения существующего функционала.

Реализация архитектурной модели позволяет выделить следующие подсистемы: инструментальная среда разработки процесса, верифицируемый программный процесс, среда командной разработки проектов и модуль верификации.

Среда разработки процесса предназначена для формирования библиотеки методов, на основе которой создаются различные процессы разработки программного обеспечения. Реализованный процесс, использующий методы, разработанные в среде, построенной на модифицированной метамодели, предлагает, проектную аналитику. Среда реализации процесса обеспечивает решение задач, определяемых методами, формируя при этом набор артефактов проекта. Механизм верификации позволяет определить корректность реализации проекта для конкретного перечня артефактов.

Набор программных компонентов и интерфейсов их взаимодействия логической структуры программного комплекса представлен в виде диаграммы компонентов нотации UML на рис. 4.2.

Похожие диссертации на Математическое моделирование верификации процесса разработки программного обеспечения