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

003469609

На правах рукописи

ГРИГОРЬЕВ Михаил Викторович

МАТЕМАТИЧЕСКОЕ МОДЕЛИРОВАНИЕ ВЕРИФИКАЦИИ ПРОЦЕССА РАЗРАБОТКИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ

05.13.18 - Математическое моделирование, численные методы и комплексы программ

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

1 4 МАЯ 2000

Тюмень - 2009

003469609

Работа выполнена на кафедре информационных систем Института математики и компьютерных наук ГОУ ВПО Тюменский государственный университет

Научный руководитель: доктор технических наук, доцент

Ивашко Александр Григорьевич Официальные оппоненты: доктор технических наук, профессор

Захаров Александр Анатольевич кандидат технических наук Примаков Сергей Сергеевич

Ведущая организация: ГОУ ВПО Новосибирский

государственный университет экономики и управления - «НИНХ»

Защита диссертации состоится 29 мая 2009 г. в 1400 часов на заседании диссертационного совета Д 212.274.14 при Тюменском государственном университете по адресу 625003, г. Тюмень, ул. Перекопская, 15А, ауд. 410.

С диссертацией можно ознакомиться в библиотеке Тюменского государственного университета.

Автореферат разослан апреля 2009 г.

Ученый секретарь диссертационного совета

Н.Н. Бутакова

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность работы. В современной индустрии программного обеспечения огромное внимание уделяется процессу разработки, который сформировал в последние десятилетия самостоятельную область знаний «Программная инженерия». На сегодняшний день нет устоявшихся принципов организации процесса разработки, многие организации пропагандируют собственные методы и процессы программной инженерии (Б\УЕВОК, СММ1, МБР, МБА, 1ЩР и т.д.). В тоже время большинство методологий оценивает качество организации процесса разработки по качеству программного продукта. Для этого применяются методы инспектирования программного обеспечения, широко представленные в литературе: аттестация, аудит, валидация, верификация, рецензирование, тестирование, экспертиза.

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

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

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

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

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

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

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

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

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

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

На защиту выносятся:

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

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

3) математическая модель верификации процесса разработки;

4) архитектурное решение проверки правил взаимосвязи между рабочими продуктами проекта, на основе оценки исполнения правил, описанных формальным языком ГОСЦ

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

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

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

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

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

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

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

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

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

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

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

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

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

Структура и объем работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы. Объем диссертации составляет 119 страниц,

содержит 34 рисунка, 3 приложения. В библиографии представлено 113 наименований работ российских и зарубежных авторов.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

В первой главе диссертационной работы проводился анализ различных методологий программной инженерии. Рассматривались методологии, поддерживающие объектно-ориентированную парадигму разработки. Наиболее перспективными из современных методов программной инженерии признаны agile -методы, основной целью которых является результат разработки, т.е. программный код и необходимая документация. К ним относятся такие методологии как RUP, ХР, SCRUM, DSDM, OpenUP, Agile и т.д. Большая часть перечисленных методов поддерживает концепцию архитектуры управляемую моделями, разрабатываемую и поддерживаемую консорциумом OMG, членами которой являются все ведущие компании-разработчики программных продуктов. Четырехуровневая модель Model-Driven Architecture (MDA) была выбрана контекстной основой проводимого исследования.

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

Проведен анализ обязанностей, которые выполняет каждый уровень MDA. Показано, что на уровне М2, который реализует возможность описания метамодели контекста разработки на метаязыке, формализованного уровнем МЗ, не определена семантическая связь между артефактами. Такая организация метамодели М2, с одной стороны, дает возможность более гибко реализовать модели процессов уровня Ml, но, с другой стороны, требует выполнить описание семантических связей в процессе конкретизации модели разработки. Тем самым ограничивается возможность применения метода верификации в программной инженерии.

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

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

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

В соответствии с четырехуровневой архитектурой моделирования OMG, для обеспечения возможности верификации всех процессов необходимо реализовать поддержку инспектирования на уровне М2, определяющем метамодель Software Process Engineering Model (SPEM).

Утверждение 1. Верификация процесса разработки осуществима при определении отношений между артефактами.

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

Реализация семантических отношений между артефактами представляет математическую модель процесса разработки в следующем виде:

РМ = (ME, С, О, AS, WPK, WD,S, РР, PR, A, WP, Е, D, АЕ), (1)

где ME - множество проектируемых элементов, С - множество классификаторов, О - множество операций, AS - множество состояний действия, WPK с ME - набор видов артефактов, U WD с О - определение работы, S с AS - множество шагов, РР = {(pp,wd)| рр =U wdj}, где £ = 1 ..п и РР с С - множество исполнителей процесса, PR с. РР - набор ролей, А с WD = {(а,рг)| а =U S;}, где i = 0..n - набор деятельностей, WP = {(иф/Срргу,Ь)||1| = 1,|у| = О..!} - множество артефактов процесса, wp:

е =и игр, и/р £ 1УР - набор атомарных артефактов, е Е Е - множество классификаторов, О - отношение, АЕ = {(и/р;,и «¿у)||£'| = 2,й 6 О} -определение направленных отношений.

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

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

В модели (1) каждый рабочий продукт связан со следующим некоторым отношением, проверка корректности артефакта осуществима за счет проверки семантических отношений, их связывающих, посредством формализации правил проверки отношений, формирующих систему правил для всего процесса. Утверждение доказано.

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

Модель Крипке формализует поведение динамической системы за счет определения множества состояний системы и переходов между этими состояниями. Каждое состояние модели помечается набором свойств, характеризующих данное состояние. При проверке каждого рабочего продукта, ему должна быть сопоставлена одна из оценок домена меток В = {— 1,0,1}, где -1 означает несоблюдение критичного правила, 0 - рекомендательного, а 1 -успешное выполнение любого правила. Состоянием проекта по разработке программного обеспечения будет являться набор артефактов состояния с сопоставленными оценками: 5: ШР -> О, я 6 где 5 - множество всех состояний проекта.

Таким образом, модель реализации процесса разработки имеет следующий вид модели Крипке:

К = (2)

где 5 - множество состояний процесса разработки; 50 £ 5 - начальное состояние; Я с 5 х 5 - отношение переходов для всевозможных состояний, т.е. для каждого состояния 5 € 5 должно существовать такое состояние б' £ Б, что имеет место Т:Б -> 2уп - функция интерпретации состояния

системы как набора оценок артефактов КД. Утверждение доказано.

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

Утверждение 4. Результатом верификации процесса разработки является оценка темпорального отношения на модели Крипке.

Семантика темпоральной формулы на модели (2) соответствует следующему отношению:

t=: {V х S х Formula) -> {True, False), (3)

где Formula определяет корректность пути за счет оценки пути темпоральной формулой вида EG. Таким образом, результатом проверки формулы является однозначная идентификация допустимости пути. Утверждение доказано.

Утверждение 5. Верификация осуществима за конечное количество итераций.

Семантическое отношение для приведенной формулы будет определяться следующим образом:

3(sj -» s2 -»•■•)(* = sa)Vi((JVf, st) t= ф). (4)

Проверка одного правила корректности артефакта определяется в отдельный момент времени, для этого используется семантика чередования. Оценка каждого артефакта wp[ состояния определяется формулой wp[ = fi(_WP). Семантика чередования отражается в дизъюнкции вида:

R(WP,WP') = %.0(WP,WP') V ...VJl^WP.WP'), (5)

где:

Я; (WP, WP') = (wpi « fi (wp)) Л ЛM{wp'j « wpj). (6)

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

F,s0 1= ф, raes0 £ S. (7)

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

Построение модели Крипке для процесса разработки:

1) определяется перечень верифицируемых артефактов (атомарные высказывания, характеризующие состояния);

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

3) устанавливаются переходы между каждой парой состояний, а также дуги для каждого состояния, указывающие на это состояние.

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

1) каждое состояние модели Крипке однозначно преобразуется в состояние автомата, причем каждое состояние автомата помечается как допускающее;

2) каждая дуга (э, б') £ Я преобразуется в переход автомата (в, а, в'), где а - атомарное изменение набора оценок артефактов состояния;

3) формулируется выходной алфавит конечного автомата, каждый символ которого соответствует совокупности оценок артефактов соответствующего состояния;

4) определяется функция выходов, отображающая каждое состояние автомата в символ выходного алфавита.

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

М= (ЕЛД^оЛС), (8)

где: 5 - конечное множество состояний; 50 6 5 - начальное состояние; Е -конечный входной алфавит; Д£5хЕх5 - отношение переходов; С: 5 -> 5 - функция выходов.

В работах Э.М. Кларка, О. Грамберга и Д. Пеледа показано, что модель Крипке однозначно представима конечным автоматом.

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

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

Алгоритм работы автомата представляет следующую последовательность:

1) определение текущего состояния процесса разработки, т.е. выбор начального состояния конечного автомата Мура, соответствующего текущим оценкам набора артефактов. Для неопределенной оценки артефакта ставится оценка «-1», таким образом, первое состояние процесса будет представлено артефактами, оценка каждого из которых будет равной «-1»;

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

3) проверка допустимости оценки состояния: если оценка допустима, то она удаляется из стека. Данный этап повторяется для всех допустимых оценок последовательности состояний;

4) проверка отсутствия элементов в стеке, что свидетельствует о выполнении темпоральной формулы, и, соответственно, о положительном исходе верификации.

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

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

Предложен метод оценки корректности разработки артефактов, включающий три этапа:

1) определение семантических отношений артефактов процесса (уровень М1). Задается либо шаблоном разработки, либо определяется командой разработчиков перед выполнением каждой итерации;

2) задание правил проверки семантических отношений (уровень М1). Определяются либо паттерном разработки, либо участником проекта в процессе создания артефакта;

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

Правило определяется кортежем:

СЯ = {as,af,rule,ínfo,type), (9)

где as 6 WR - артефакт, являющийся исходным артефактом семантической связи с проверяемым артефактом, af 6 WR - оцениваемый артефакт, rule - запись инварианта отношения формальным языком, info -описание подсказки, по избеганию нарушения данного правила, type € {критичное, рекомендательное} - тип правила.

Алгоритм выставления оценки представлен следующей последовательностью действий:

1) артефакту выставляется оценка «-1»,

2) осуществляется проверка инварианта для правила:

a) если результат положительный, то оценка = «/»;

b) если результат отрицательный:

гО, если type = рекомендательное, оценка = J ,

И.если type = критичное.

Для получения оценки артефакта разработан язык formal Object Constraint Language (fOCL) описания правил выполнения семантического отношения, заданных в модели (1). За основу взят язык Object Constraint Language (OCL), реализующий всю декларативную мощность записи ограничений (в формате инвариантов) на классы (объекты). Формализация правил, декларированных в OCL, дало возможность выполнять верификацию артефактов, поддерживающих объектную модель разработки в автоматическом режиме. Дополнительно реализована возможность записи инвариантов для классификаторов, таким образом, расширена грамматика языка.

Преобразование исходного текста правила на языке fOCL в исполняемый код обеспечивается посредством компиляции. Работа компилятора реализуется в 4 этапа: лексический анализ, синтаксический анализ, семантический анализ, генерация целевого кода.

На вход компилятора подается правило, записанное на языке fOCL. На этапе лексического анализа осуществляется проверка текста правила на соответствие формальной грамматике языка. Для выполнения синтаксического анализа компилятор подгружает шаблоны артефактов и классификаторов, которые используются в описании правила. Классификаторы, представляющие как документы, так и модель в нотации UML, представлены в стандарте XML metadata interchange (XMI, консорциум OMG). На семантическом этапе проводится сопоставление конструкций выражения элементам модели артефакта, проверка типов и действительных ассоциаций, используемых классификаторов. Результатом работы компилятора является готовый набор инструкций, записанных исполняемым кодом, соответствующим исходному тексту выражения языка fOCL.

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

Четвертая глава посвящена разработке архитектурного решения и практике создания комплекса программ поддержки реализации процессов программной инженерии.

Четырехуровневая архитектура моделирования консорциума ОМО реализует концепцию модельно-ориентированного подхода МБА к разработке программного обеспечения. Компонентная организация архитектурного решения программного комплекса соответствует технологии МБА, где каждая подсистема реализует обязанности, закрепленные за уровнями модели ОМО.

Уровень М2 модели ОМв обеспечивается подсистемой «Разработка процессов программной инженерии», которая реализует инструментарий, формирующий модифицированную модель БРЕМ (1). Сформированный процесс, передается в другие подсистемы в виде набора структурированных ХМЬ-файлов, каждый из которых представляет отдельный метод процесса. Подсистема предоставляет обеспечивающий интерфейс работы с этими файлами.

Уровень М1 обеспечивается подсистемой «Среда верификации процесса», которая предоставляет инструмент для создания правил и выполнения оценки корректности артефактов в соответствии с разработанным методом верификации, представленным конечным автоматом (8). Подсистема дает возможность конкретизировать модель, созданную на уровне М2 путем редактирования семантических отношений и правил. Компонент разработки правил подсистемы «Среда верификации процесса» позволяет описать инварианты для всех семантических отношений, заданных моделью (1), в формальной грамматике ГОСЬ. В этой же подсистеме реализуется компилятор, описанный в главе 3.

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

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

Для проведения эксперимента была разработана модификация Rational Unified Process (RUP), включающая изменения, ориентированные на небольшую команду разработчиков. Учитывается возможность использования данной модификации в учебных проектах. В ходе решения задачи по разработке проекта информационной системы, группа из 3 человек должна выполнить работу в двух фазах RUP: «Начало», «Исследование». Каждым участником, в ходе реализации проекта, выполнялись различные ролевые задачи.

Для решения задачи эксперимента определен минимальный набор артефактов, являющихся значимыми результатами в контексте учебных проектов. Данный набор представлен артефактами: модель бизнес-прецедентов, модель бизнес-анализа, документ «Видение», модель прецедентов, дополнительные спецификации, диаграмма деятельности, модель проектирования, диаграмма последовательности. Для данного набора артефактов определены правила, задающие их семантические отношения, которые позволяют выявить не только ошибки в разрабатываемых рабочих продуктах, но и дают возможность контролировать корректность выполнения процесса.

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

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

120

о 100 Ю X

О 80

О

ю

§ 60 у

5

5

О 40 X

20

о

12345678:

Итерация

1 - серия, в которой ошибки выявлялись участниками проекта (2 - линия тренда), 3 - серия, в которой ошибки выявлялись системой (4 - линия тренда). Рис. 1. Среднее количество ошибок проектов, выявленных на различных этапах

эксперимента

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

По результатам исследований могут быть сделаны следующие выводы:

1) модифицирована метамодель БРЕМ, формализующая семантические отношения между артефактами, что дает возможность реализовать верификацию процесса разработки программного обеспечения;

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

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

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

4) создан язык ГОСЬ, формализующий правила проверки артефактов, инкапсулирующий декларативную грамматику объектного языка ограничений ОСХ. Разработан компилятор, который позволяет выявить синтаксические и семантические ошибки при написании правила. Интеграция скомпилированного правила дает возможность выполнять проверку артефактов в однозначных проектах без модификации самого правила;

5) разработан программный комплекс, реализующий возможности верификации процесса командной разработки проектов. Организация программного комплекса охватывает все уровни архитектуры моделирования ОМв;

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

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

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Григорьев М.В., Коломиец И.И. Виртуальная среда исследования бизнес-процессов // Междунар. школа-конф. по приоритетным направлениям развития науки и техники с участием молодых ученых, аспирантов и студентов. Тезисы докладов. - Москва, 2006. - С. 22-24.

2. Григорьев М.В., Коломиец И.И. Специализированный учебный программный комплекс исследования и командного проектирования бизнес-процессов // Наука. Технологии. Инновации. М-лы Всерос. науч. конф. молодых ученых в 7-ми частях. Часть. 1. - Новосибирск. Изд-во НГТУ, 2006. - С. 137-138.

3. Григорьев М.В.. Ивашко А.Г., Коломиец И.И. Бизнес-моделирование проектирования информационной системы в команде // Проблемы информатики в образовании, управлении, экономике и технике: Сбор. ст. VI Всерос. науч.-техн. конф. - Пенза. Изд-во АНОО «Приволжский Дом знаний», 2006. - С. 16-19.

4. Григорьев М.В., Ивашко А.Г. Унифицированный процесс проектирования программного обеспечения в команде // Безопасность информационного пространства VI: Сбор. тр. межвуз. научно-практ. конф. студентов, аспирантов и молодых ученых. Тюмень, 22-23 ноября 2007 г. - Тюмень. Изд-во ТюмГУ, 2007. - С. 159-162.

5. Ивашко А.Г., Григорьев М.В., Коломиец И.И. Проектирование информационных систем: Учебно-метод. пособ. - Тюмень. Изд-во ТюмГУ, 2007.-328 с.

6. Григорьев М.В., Ивашко А.Г. Электронное справочное руководство «Учебный унифицированный процесс» // Информационные технологии и телекоммуникации в экономике, управлении и социальной сфере: М-лы II межрегион, научно-практ. конф. 15 ноября - 15 декабря 2007 г. - Тюмень. Изд-во ТюмГУ, 2008. - С. 121-124.

7. Григорьев М.В., Урзиков А.В. Технология методологической поддержки командной разработки программных проектов // Проблемы информатики в образовании, управлении, экономике и технике: Сбор. ст. VIII Всерос. науч.-техн. конф. - Пенза. Изд-во АНОО «Приволжский Дом знаний», 2008. - С. 98-100.

8. Григорьев М.В., Гладич О.И. Об одном подходе к реализации редактора объектного языка ограничений // Проблемы информатики в образовании, управлении, экономике и технике: Сбор. ст. VIII Всерос. науч.-техн. конф. -Пенза. Изд-во АНОО «Приволжский Дом знаний», 2008. - С. 100-102.

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

моделирование. Сбор. науч. тр. Вып. 10. - Тюмень. Изд-во «Вектор Бук», 2008.-С. 98-106.

10.Ивашко А.Г., Григорьев М.В. Объектно-ориентированный язык ограничений для верификации процесса командной разработки программного обеспечения // Вестник ТюмГУ. - 2008. - №6. - Тюмень. Изд-во ТюмГУ. -С. 152-158.

11 .Григорьев М.В., Урзиков A.B. Свидетельство о государственной регистрации программы для ЭВМ №2008613269 «Viewer for Eclipse» от 09.07.2008.

М.Григорьев М.В., Гладич О.И. Свидетельство о государственной регистрации программы для ЭВМ №2008613270 «Tools for EUR» от 09.07.2008.

13.Григорьев М.В., Мусин Ф.Ф. Свидетельство о государственной регистрации баз данных №2009620056 «Веб-представление учебного процесса разработки программного обеспечения» от 22.01.2009.

Подписано в печать 23.04.2009г. Формат 60x84/16. Печать цифровая. Бумага Ballet. Усл. п. л. 1,0. Тираж 100. Заказ 28.

ООО «Вектор Бук». 625004, г. Тюмень, ул. Володарского, 45. Тел. (3452) 46-54-04, 46-90-03.

Введение.

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

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

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

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

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

Выводы.

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

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

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

Выводы.

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

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

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

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

Выводы.

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

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

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

Выводы.

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

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

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

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

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

Выводы.

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

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

Актуальность работы. В современной индустрии программного обеспечения огромное внимание уделяется процессу разработки, который сформировал в последние десятилетия самостоятельную область знаний «Программная инженерия» (В.В. Липаев, JI.A. Мацяшек, 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). Верификация процесса разработки не выделена в самостоятельный процесс программной инженерии. Требуется изучить процесс разработки программного обеспечения и создать механизм его верификации.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1. Модифицирована метамодель SPEM, формализующая семантические отношения между артефактами, что дает возможность реализовать верификацию процесса разработки ПО.

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

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

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

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

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

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

1. Г. Буч. UML. Классика CS. 2-ое изд. / Г. Буч, А. Якобсон, Дж. Рамбо: Пер. с англ.; Под общей редакцией проф. С. Орлова СПб.: Издательство: «Питер», 2006. — 736 е.: ил.

2. Г. Буч. Язык UML. Руководство пользователя. 2-ое изд. / Г. Буч, Д. Рамбо, И. Якобсон.: Пер. с англ. Мухин Н. М.: Издательство: «ДМК Пресс», 2007. - 496 е.: ил.

3. Г. Буч. Язык UML. Руководство пользователя. / Г. Буч, Д. Рамбо, А. Джекобсон.: Пер. с англ. Слинкин А.А. 2-ое изд., стер. - М.: Издательство: «ДМК Пресс»; СПб.: Издательство: «Питер», 2004, — 432 е.: ил.

4. Д. Рамбо. UML. Специальный справочник. / Д. Рамбо, А. Якобсон, Г. Буч. СПб.: Издательство: «Питер», 2002. - 656 с.

5. Д. Рамбо. UML 2.0. Объектно-ориентированное моделирование и разработка. 2-ое изд. / Д. Рамбо, М. Блаха. СПб.: Издательство: «Питер», 2007 - 544 е.: ил.

6. А. Якобсон. Унифицированный процесс разработки программного обеспечения. / А. Якобсон, Г. Буч, Д. Рамбо. СПб.: Издательство: «Питер», 2002, - 496 е.: ил.

7. Дж. Шмуллер. Освой самостоятельно UML за 24 часа, 3-е изд. : Пер. с англ. М.: Издательский дом «Вильяме», 2005. — 416 е.: ил. — Парал. тит. англ.

8. К. Ларман. Применение UML и шаблонов проектирования. 2-ое изд.: Пер. с англ. М.: Издательский дом "Вильяме", 2004. — 624 е.: ил. -Парал. тит. англ.

9. К. Ларман. Применение UML 2.0 и шаблонов проектирования.: Пер. с англ. — М.: Издательский дом "Вильяме", 2008. — 736 е.: ил. — Парал. тит. англ.

10. М. Фаулер. UML. Основы. 2-ое изд. Краткое руководство по унифицированному языку моделирования / М. Фаулер, К. Скотт.: Пер. с англ. СПб.: Издательство: «Символ-Плюс», 2006. — 192 е.: ил.

11. М. Фаулер. UML. Основы. 3-е изд. Краткое руководство по стандартному языку объектного моделирования.: Пер. с англ. — СПб.: Издательство: «Символ-Плюс», 2002. 192 е.: ил.

12. Э. Нейбург. Проектирование баз данных с помощью UML. / Э. Нейбург, Дж. Максимчук, А. Роберт.: Пер. с англ. — М.: Издательский дом «Вильяме», 2002. 288 е.: ил. - Парал. тит. англ.

13. Hans-Erik Eriksson. Business Modeling with UML: Business Patterns at Work. / H. Eriksson, M. Penker. OMG Press. John Wiley & Sons, 2000. -459 pages.

14. Ф. Крачтен. Введение в Rational Unified Process. 2-ое изд.: Пер. с англ. М.: Издательский дом «Вильяме», 2002. — 240 е.: ил. — Парал. тит. англ.

15. Г. Поллис. Разработка программных проектов: на основе Rational Unified Process (RUP). / Г. Поллис, JI. Огастин, К. Jloy, Д. Мадхар. -М.: Издательство: ООО «Бином-Пресс», 2005 г. 256 е.: ил.

16. Электронное справочное руководство Rational Unified Process Version 7.0 Copyright (С) IBM Corporation 1987, 2005.

17. S. Ambler. The Enterprise Unified Process: Extending the Rational Unified Process. / S. Ambler, J. Nalbone, M. Vizdos. Prentice Hall PTR, 2005. -408 pages.

18. J. Warmer. The Object Constraint Language. Precise Modeling with UML. / J. Warmer, A Kleppe.: Addison-Wesley Professional, 1998. 112 pages.

19. J. Warmer. The Object Constraint Language Second Edition. Getting Your Models Ready for MDA (2nd Edition). / J. Warmer, A Kleppe.: Addison-Wesley Professional, 2003 — 206 pages.

20. Д. Хопкрофт. Введение в теорию автоматов, языков и вычислений, 2-ое изд. / Д. Хопкрофт, Р. Мотвани, Д. Ульман.: Пер. с англ. М.: Издательский дом «Вильяме», 2008. — 528 е.: ил. — Парал. тит. англ.

21. Б.А. Трахтенброт. Конечные атоматы (поведение и синтез). / Б.А. Трахтенброт, Я.М. Барздинь. — М.: Издательство: «Наука», 1970. 400 е.: ил.

22. Н.К. Верещагин. Лекции по математической логике и теории алгоритмов. Часть 1. Начала теории множеств. / .К. Верещагин, А. Щень. -М.: Издательство: «МЦНМО», 1999. 128 с.

23. А.В. Гладкий. Формальные грамматики и языки. — М.: Издательство: «Наука», 1973.-368 с.

24. Н. Хомский. Введение в формальный анализ естественных языков. / Н. Хомский, Дж. Миллер. М.: Издательство: «Едиториал УРСС», 2003. -64 с.

25. Э. Брауде. Технология разработки программного обеспечения. СПб.: Издательство: «Питер», 2004. - 655 е.: ил.

26. С. Амблер. Гибкие технологии: экстремальное программирование и унифицированный процесс разработки. Библиотека программиста. -СПб.: Издательство: «Питер», 2005. 412 е.: ил.

27. JT. Константайн. Разработка программного обеспечения. / JI. Константайн, JI. Локвуд. СПб.: Издательство: «Питер», 2004. - 592 е.: ил.

28. Scott W. Ambler. The Object Primer, Third Edition. Cambridge University Press, 2004 572 pages.

29. Э. Роллингз. Проектирование и архитектура игр. / Э. Роллингз, Д. Моррис.: Пер. с англ. М.: Издательский дом «Вильяме», 2006. — 1040 е.: ил. - Парал. тит. англ.

30. Д. Шафер. Управление программными проектами: достижение оптимального качества при минимуме затрат. / Д. Шафер, Р. Фатрелл, J1. Шафер.: Пер. с англ. — М.: Издательский дом «Вильяме», 2003. — 1136 е.: ил. Парал. тит. англ.

31. IEEE Guide to the Software Engineering Body of Knowledge -SWEBOK®. California, Computer society, 2004 version.

32. М. Bonsangue. Formal Methods for Open Object-Based Distributed Systems: 9th IFIP WG 6.1 International Conference, FMOODS 2007, Paphos, Cyprus, June 6-8, 2007, Proceedings. / M. Bonsangue, E. Johnsen.: Springer, 2007. — 317 pages.

33. B. Beckert. Verification of Object-Oriented Software. The KeY Approach: Foreword by K. Rustan M. Leino. / B. Beckert, H. Hahnle, P. Schmitt.: Springer, 2007. 658 pages.

34. E. Najm. Formal Methods for Open Object-Based Distributed Systems: 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, November 19.21, 2003, Proceedings. / E. Najm, U. Nestmann, P. Stevens.: Springer, 2003. 293 pages.

35. A. Ахо. Компиляторы: принципы, технологии, инструменты. / А. Ахо, Р. Сети, Дж. Ульман. М.: Издательский дом «Вильяме», 2003. — 768 с.

36. ГОСТ Р ИСО 9000-2001 Системы менеджмента качества. Основные положения и словарь. — М.: Издательство: «Госстандарт России», 2001.

37. ГОСТ Р ИСО 9001-2001 Системы менеджмента качества. Требования. М.: Издательство: «Госстандарт России», 2001.

38. ГОСТ Р ИСО/МЭК 12207-99 Информационная технология. Процессы жизненного цикла программных средств. — М.: Издательство: «Госстандарт России», 2000.

39. ГОСТ Р ИСО/МЭК 15288-2005 Информационная технология. Системная инженерия. Процессы жизненного цикла систем. М.: Издательство «Сгандартинформ», 2006.

40. Object Management Group (OMG) (2006, May 01). Object Constraint Language Specification (OCL) Version 2.0 WWW document. URL http://www.omg.org/cgi-bin/doc7fomial/2006-05-01 46.The Object Constraint Language [WWW document].

41. URL http://www.csci.csusb.edu/dick/samples/ocl.html 47.Object Constraint Language WWW document.

42. URL http://en.wikipedia.org/wiki/ObjectConstraintLanguage

43. Some Shortcomings of OCL, the Object Constraint Language of UML WWW document.

44. URL http://www.omg.org/docs/ad/99-12-05.pdf 49.Introduction to OCL WWW document.

45. URL http://www.klasse.nl/ocl/ocl-introduction.html 50. Why Combine UML and OCL? WWW document.

46. URL http://www.klasse.nl/ocl/ocl-reasons.html 51.0bject-zto OCL dictionary WWW document.

47. URL http://www.klasse.nl/ocl/oz-ocl-mapping.pdf 52.On the Expressive Power of the Object Constraint Language OCL WWW document.

48. URL http://projekte.fast.de/Projekte/forsoft/ocl/ocl.html 53.Architecture and Design: Unified Modeling Language (UML) WWW document.

49. URL http://www.omg.Org/spec/SPEM/2.0/PDF 56.Object Management Group (OMG) (2006, January 01). Meta Object Facility (MOF) Core specification Version 2.0 WWW document. URL http://www.omg.org/spec/MOF/2-0/PDF/

50. UML to XMI Export Functionality WWW document. URL http://msdn.microsoft.com/en-us/library/aal40339.aspx

51. Eclipse Process Framework (EPF) 1.2.0 WWW document.

52. URL http://nvoynov.blogspot.eom/2007/08/eclipse-process-framework-epf-120.html

53. IBM Rational Method Composer WWW document.

54. URL http://www.interface.ru/home.asp7artI d=543 5 63.IBM Rational Requisite Pro WWW document.

55. URL http://www.interface.ru/liome.asp?artId=l0131 64.IBM Rational Requisite Pro-2 WWW document. URL http://www.interface.ru/liome.asp?artId=l 0294

56. RequisitePro средство управления требованиями URL http://www.interface.ru/home.asp?artld=4835

57. Моделирование процессов разработки ПО и процессов с помощью Rational Method Composer URL http://www.interface.ru/home.asp?artId=l 524

58. Выпуск Eclipse Process Framework (EPF) версии 1.2.0 WWW document.

59. URL http.7/www.it4business.ru/archives/444/ 68.IBM Rational Unified Process WWW document.

60. URL http://www.interface.ru/home.asp?artld=486 69.Унифицированный процесс разработки от Rational Software RUP (Rational Unified Process) WWW document. URL http://www.interface.ru/home.asp?artId=34221. WWW document.создание сайтов WWW document.

61. IBM Rational Unified Process (RUP) WWW document. URL http://www.interface.ru/home.asp?artTd=5154

62. Модель качества разработок CMM и ее поддержка линейкой продуктов Rational WWW document.

63. URL http://www.interface.m/home.asp?artld:=2304

64. Rational Unified Process как достичь 2-го уровня CMM WWW document.

65. URL http://www.interface.ru/home.asp?artId=2310

66. Rational Unified Process как достичь 3-го уровня CMM WWW document.

67. URL http://www.interface.ru/home.asp?artld=2312

68. Использование RUP для небольших проектов: расширение экстремального программирования WWW document.

69. URL http://www.interface.ru/home.asp?artld=4720

70. Динамичный RUP: Вести с передовой WWW document. URL http://www.interface.m/home.asp?artId=l9794

71. RUP и другие методологии разработки ПО WWW document. URLhttp://cmcons.com/articles/obshhiestatimp/rupidrugiemetodologiiraz rabotkipo/

72. OpenUP это просто WWW document.

73. URL http://www.interface.ru/home.asp?artId=9995 78.Отличие формальных и гибких методологий разработки в картинках WWW document.

74. URL http://www.it4business.ru/lib/1299/

75. Технология разработки программного обеспечения WWW document. URL http://www.interface.i-u/home.asp?artId=4718

76. Переход от каскадной разработки к итеративной WWW document. URL http://www.interface.rn/home.asp7arUxNl 15581 .Разработка программного обеспечения группой в составе одного человека WWW document. URL http://www.interface.ru/home.asp?artId=4714

77. Нику да без трассировки: практические советы по внедрению трассируемости WWW document.

78. URL http://www.interface.ru/home.asp?artld=6769

79. В круге разработки WWW document. URL attachment:/70/attachment70.htm84.Компилятор WWW document.

80. URL http://ru.wildpedia.org/wild/KoMnmMTop85.Compiler WWW document.

81. URL http://en.wikipedia.org/wiki/Compiler

82. List of important publications in computer science WWW document. URLhttp://en.wikipedia.org/wiki/Listofimportantpublicationsincomputers cience

83. Temporal logic WWW document.

84. URL http://en.wikipedia.org/wiki/Temporallogic

85. Temporal logic in finite-state verification WWW document.

86. URL http://en.wikipedia.org/wiki/Temporallogicinfinitestateverification

87. Семантика Крипке WWW document.

88. URL http://ru.wikipedia.org/wiki/CeMaHTHKaKpHnKe

89. Kripke semantics WWW document.

90. URL http://ru.wikipedia.org/wiki/CeMaHTHKaKpHnKe

91. Kripke structure WWW document.

92. URL http://en.wikipedia.org/wiki/Kj-ipkestructure

93. J. Burgess. Kripke Models. WWW document.,

94. URL http://www.princeton.edu/~jburgess/Kripkel .doc

95. Конечный автомат WWW document.

96. URL http://ru.wikipedia.0rg/wiki/K0He4HbieaBT0MaTbi

97. Finite state machine WWW document.

98. URL http://en.wikipedia.org/wiki/Finitestatemachine

99. Moore machine WWW document.

100. URL http://en.wikipedia.org/wiki/Mooremachine

101. Алгебра логики WWW document.

102. URL http://ru.wikipedia.org/wiki/Алгебралогики

103. Boolean logic WWW document.

104. URL http://en.wikipedia.org/wiki/Booleanlogic

105. Формальная грамматика WWW document.

106. URL http://ш.wikipedia.org/wiki/Фopмaльнaягpaммaтикa

107. Formal grammar WWW document.

108. URL http://en.wikipedia.org/wiki/Formalgrammar

109. Formal verification WWW document.

110. URL http://en.wikipedia.Org/wiki/Formalverification

111. А.Г. Ивашко, М.В. Григорьев, И.И. Коломиец. Проектирование информационных систем: Учебно-методическое пособие / А.Г. Ивашко, М.В. Григорьев, И.И. Коломиец. Тюмень. Изд-во ТюмГУ,2007. 328 с.

112. А.Г. Ивашко, М.В. Григорьев. Объектно-ориентированный язык ограничений для верификации процесса командной разработки программного обеспечения // Вестник ТюмГУ, 2008. — №6. — Тюмень. С. 152-158.

113. М.В. Григорьев. Верификация процесса разработки программного обеспечения в команде // Математическое и информационное моделирование. Сборник научных трудов. Вып. 10. — Тюмень. Изд-во «Вектор Бук», 2008. С. 98-106.

114. М.В. Григорьев, О.И. Гладич. Об одном подходе к реализации редактора объектного языка ограничений // Проблемы информатики в образовании, управлении, экономике и технике: сборник статей VIII

115. Всероссийской научно-технической конференции — Пенза. Изд-во «Приволжский Дом знаний», 2008. — С. 100-102.

116. М.В. Григорьев, Ф.Ф. Мусин. Свидетельство о государственной регистрации баз данных №2009620056 «Веб-представление учебного процесса разработки программного обеспечения» от 22.01.2009.

117. М.В. Григорьев, А.В. Урзиков. Свидетельство о государственной регистрации программы для ЭВМ №2008613269 «Viewer for Eclipse» от 09.07.2008.

118. М.В. Григорьев, О.И. Гладич. Свидетельство о государственной регистрации программы для ЭВМ №2008613270 «Tools for EUR» от 09.07.2008.