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

и

у-

КАЛЕНКОВА АННА АЛЕКСЕЕВНА

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

Специальность 05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

1 7 НОЯ 2011

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

Москва-2011

005000801

Работа выполнена в Учреждении Российской академии наук Вычислительном центре им. А. А. Дородницына РАН

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

доктор физ.-мат. наук Серебряков Владимир Алексеевич

Официальные оппоненты:

доктор физ.-мат. наук Флёров Юрий Арсениевич

Ведущая организация:

Московский физико-технический институт (государственный университет)

заседании на диссертационного совета Д 002.017.02 при Учреждении Российской академии наук Вычислительном центре им. А. А. Дородницына РАН по адресу: Москва, улица Вавилова, дом 40, конференц-зал.

С диссертацией можно ознакомиться в библиотеке ВЦ РАН.

Автореферат разослан « » ноября 2011 г. Ученый секретарь

кандидат физ.-мат. наук Гайсарян Сергей Суренович

Защита состоится «_$_» декабря 2011 года в_

час. на

диссертационного совета

Рязанов В.В.

Д 002.017.02 доктор физ.-мат. наук

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

Актуальность темы

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

Цель работы

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

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

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

3. Для унифицированного анализа блочно-графовых языков описания потоков работ используется промежуточное блочно-графовое представление. Необходимы алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и предложенным в литературе блочно-графовым базисным Формальным языком описания потоков работ.

4. Разработка алгоритмов двустороннего отображения между Формальным языком описания потоков работ и языком ВРЕЬ для оценки практического применения алгоритмов анализа потоков работ.

Научная новизна

Научной новизной обладают следующие результаты диссертационной работы:

1. Предложены новые эффективные алгоритмы верификации и оптимизации (распараллеливания независящих по данным действий) потоков работ;

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

3. Разработаны алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и блочно-графовым представлением потока управления.

Практическая ценность

Разработанные промежуточное графовое представление потока управления и потока данных, алгоритмы работы с этим представлением, алгоритмы двустороннего отображения между этим представлением и блочно-графовым Формальным языком описания потоков работ, а также алгоритмы двустороннего отображения между конструкциями языка ВРЕЬ и Формальным языком описания потоков работ позволили создать Систему автоматического анализа и преобразования ВРЕЬ-процессов. Эта система была использована для анализа и преобразования производственных процессов Электронной библиотеки «Научное наследие России», формализованных с помощью языка ВРЕЬ. На основе доступных открытых кодов был создан прототип системы исполнения ВРЕЬ-процессов Электронной библиотеки «Научное наследие России». Предложенный алгоритм оптимизации ВРЕЬ-процессов имеет большое практическое значение, так как в настоящий момент нет методов и систем, позволяющих в полном объеме распараллеливать блочно-графовую структуру потока работ.

Апробация работы

Основные положения работы докладывались на восьмой всероссийской научной конференции «Электронные библиотеки: перспективные методы и технологии, электронные коллекции» (2006 г.), на 51-ой научной конференции «Современные проблемы фундаментальных и прикладных наук» (2008 г.), на четвертой международной конференции «Информационные технологии и системы: наука и практика» (2009 г.), на 52-ой научной конференции «Современные проблемы фундаментальных и прикладных наук» (2009 г.), на 17-ой всероссийской научно-методической конференции «Телематика» (2010 г.), на 13-ой всероссийской конференции «Распределенные информационно-вычислительные ресурсы» (2010 г.). Были опубликованы работы в журналах «Труды МФТИ» (2009 г.) и «Программирование» (2010 г.)

Публикации

По теме диссертации опубликовано 8 печатных работ.

Структура и объем работы

Работа состоит из введения, трех глав, заключения, списка литературы и трех приложений. Общий объем диссертации 164 страницы. Список литературы содержит 42 наименования.

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

В Главе 1 рассказывается об основных понятиях предметной области (потоки работ, системы управления потоками работ), приводится описание основных известных языков представления потоков работ. Для анализа и преобразования потоков управления вводятся Размеченные графы анализа потоков работ.

Определение 1. Графом анализа потока работ (графом анализа) называется шестерка АО = {И,Т,15,С,М,Р)\ N - конечное множество вершин, Гс N - конечное множество заданий, ^еГ - начальное задание, СсЛ' - конечное множество вершин выбора, Мс]У - конечное множество вершин слияния, Fc:iVxiV - поток управления (множество дуг). При этом выполнены условия: у начального задания нет входящих дуг, для каждой вершины кроме начального задания п € N \ } существует путь из ^ в п, только у заданий

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

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

перемещаются по Графу анализа согласно определенным правилам.

V

Выбор Слияние

Рис. 1. Элементы Графа анализа потока работ

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

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

Определение 2. Поток работ, заданный с помощью Формального языка описания потоков работ, определяется шестеркой Ш = (1,0, \, Ф,0, ¥):

1. Множество X - множество всех локальных генерируемых в процессе выполнения потока работ событий.

2. Множество действий А = состоит из

множества составных и простых действий, для которых определены формулы.

3. Начальное действие Действие, с которого начинается выполнение потока работ.

4. Множество переменных, определенных уровне экземпляра потока работ Ф.

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

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

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

Приводятся алгоритм построения Размеченного графа анализа потока работ по Формальному описанию потока работ (Алгоритм 1) и обратный алгоритм получения Формального описания потока работ по Размеченному графу анализа

(Алгоритм 2). Доказано утверждение об обратимости преобразований.

Утверждение 1. Пусть по Формальному описанию потока работ WF{ =(£1,£21,А,О,Ф1,01,ХР1) с помощью Алгоритма 1 построен Размеченный граф анализа потока работ LAG = (N,Т,ts,С,М,F,Lt,Lm,Lout,Lch,Lcond,Lf). Тогда, если к

Размеченному графу анализа потока работ LAG применить Алгоритм 2 , то он будет выполнен без ошибок, результатом его работы стает некоторое Формальное описание потока работ WF2 =(Е2,О2,А"о,Ф2,02,Ч'2).

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

Алгоритмы верификации потоков работ позволяют находить вершины графа, моделирующего поток работ, в которых могут возникать структурные конфликты. Конфликт типа «тупик» возникает в том случае, если лишь некоторые из входящих дуг синхронизирующей вершины активированы, и синхронизирующая вершина будет бесконечно долго ожидать активации других входящих дуг. Конфликт типа «недостаток синхронизации» произойдет в ациклическом Размеченном графе анализа потока работ, если вершина слияния была активирована несколько раз вследствие активации различных входящих дуг. В работе представлен новый алгоритм верификации потоков работ - АБВ (алгоритм булевой верификации) для графов без ориентированных циклов (Алгоритм 3), в ходе работы которого каждой вершине выбора се С Размеченного графа анализа потока работ LAG = (N,T,ts ,С,М, F, Lt, Lm, Lou!, Lch, Lcond, Lf) ставится в соответствие уникальный идентификатор CId (с), для каждой вершины пе N и для каждой дуги /е F определяются условие выполнения Сп(п) и условие активации CAf) соот-

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

Рис. 2. Пример работы Алгоритма 3

Для задания Е условия активации входящих дуг: true и с, различны, поэтому может возникнуть конфликт типа «тупик». Конфликт типа «недостаток синхронизации» может

возникнуть в вершине слияния Н, условия активации входящих дуг которой: true и C2&C[VCr

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

Теорема 1. Пусть дан Размеченный граф анализа потока работ без ориентированных циклов LAG = (N,T,ts,C,M ,F,LrLin, Lout

> Ал > Lcond, Lf), не содержащий структурных конфликтов. В ходе работы Алгоритма 3 было вычислено условие выполнения вершины выбора се С-Сп (с), пусть оно было представлено в виде ДНФ -Kxv...vКт. Тогда для любой вершины графа пе N представление условия ее выполнения либо содержит все дизъюнкты k&Kv..., k&Km, где к - это Си(с) или Cld(c) не более одного раза, либо не содержит ни один из этих дизъюнктов.

При слиянии потоков управления все дизъюнкты k&Kl,...,k&Km, k&Kl,...,k&Km заменяются на К1,...,Кт для сокращения представления условия выполнения вершины. После получения новых дизъюнктов должна быть проведена попытка повторного сокращения представления условия активации и так до тех пор, пока сокращение не сможет быть выполнено. Такие представления условий выполнения вершин и активации дуг называются сокращенными. Теорема 2. Пусть дан Размеченный граф анализа потока работ без ориентированных циклов, не содержащий структурных конфликтов. В ходе работы Алгоритма 3 были

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

Теорема 3. Пусть дан Размеченный граф анализа потока работ без ориентированных циклов LAG = (N,T,ts,C,M,F,L:,Lm,Lou:,Lch,Lcond,Lf), не содержащий структурных конфликтов. В ходе работы Алгоритма 3 были вычислены условия активации входящих дуг fx,f2&F

вершины пе N- Cf(fx), Cf(f2). Рассмотрим Кх и К2 - произвольные дизъюнкты представлений условий Cf (/,) и С/(/2) соответственно. Пусть К{ = ар &...&а1,

K2=bq&....&.bl и Зге N: ai^bnai или | = /? + 1<#,или i = q + \< р такое, что V/ < г, j > 1: а} = bj. Тогда дизъюнкты АГ, и К2 не являются взаимоисключающими, то есть КХ&.К2Ф false.

Количество дизъюнктов при каждом новом слиянии может расти экспоненциально, поэтому вводятся ключевое и табличное представленш условий выполнения вершин и активации дуг. Ключевое представление определяется как дизъюнкция ключевых факторов соответствующего сокращенного представления. Табличное представление - это таблица, каждая строка которой будет соответствовать некоторой вершине выбора графа, а точнее ее идентификатору. Табличное представление используется для определения конфликтов типа «недостаток синхронизации» и может быть получено по ключевому представлению. В работе доказано, что вычислительная сложность Алгоритма 3, работающего с ключевыми и табличными представлениями, составляет 0(| F | * | С |2), где | F | - количество дуг, | С | - количество вершин выбора.

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

Предлагается алгоритм автоматической оптимизации Размеченных графов анализа потоков работ (Алгоритм 5), который преобразует граф на каждом уровне вложенности циклов программы, удаляя потоки управления, формирующие избыточные пути в графе, и сохраняя зависимости по данным и управлению (условия выполнения заданий и вершин выбора). Вычислительная сложность Алгоритма 5 0(|ЛГ|2*|Ф|2+|ЛП4 + |ЛГ|2*|С|3), где \N\- количество вершин, | С | - количество вершин выбора, а | Ф | - количество переменных, используемых в качестве входных и выходных параметров вершин графа. Приводится модификация алгоритма оптимизации (Алгоритма 5), которая позволяет восстанавливать описание потока работ на Формальном языке по Размеченному графу анализа (с помощью Алгоритма 2), полученному в результате оптимизирующих преобразований. Дается обоснование того, что Алгоритм 5 не меняет функциональность (смысл) потока работ, если Размеченный граф анализа потоков работ удовлетворяет некоторым дополнительным условиям и не содержит структурных конфликтов.

В Главе 3 определяются правила прямого и обратного отображений между конструкциями языка BPEL и Формального языка описания потоков работ. Описывается Система

автоматической верификации и оптимизации, реализующая предлагаемые алгоритмы анализа, преобразования и отображения, которая может быть использована для анализа и оптимизации потоков работ, формализованных с помощью языка ВРЕЬ. Излагаются основные принципы работы Электронной библиотеки «Научное Наследие России», обосновывается необходимость использования системы управления потоками работ для формализации и автоматизации управления процессами в электронной библиотеке, в качестве такой системы предлагается специально разработанная Система управления Электронной библиотекой «Научное наследие России», отвечающая за исполнение ВРЕЬ-описаний процессов. Рассматривается пример ВРЕЬ-процесса Электронной библиотеки «Научное наследие России», проводится его анализ и оптимизация в соответствии с предлагаемыми алгоритмами.

В Приложении 1 приведен псевдокод функций используемых при построении Формального описания потока работ по Размеченному графу анализа потока работ. В Приложении 2 и Приложении 3 представлен ВРЕЬ-процесс удаления книги в Электронной библиотеке «Научное наследие России» до и после оптимизирующих преобразований соответственно. В Заключении перечисляются основные результаты работы.

Основные результаты работы:

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

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

горитмы двустороннего отображения между Формальным языком описания потоков работ и языком BPEL.

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

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

5. Была разработана Система автоматической верификации и оптимизации Размеченных графов анализа потоков работ, в которой были реализованы предложенные алгоритмы.

6. Был создан прототип Системы управления электронной библиотекой «Научное наследие России», который исполняет BPEL-процессы, координирующие работу библиотеки. Был произведен анализ этих процессов.

По теме диссертации опубликованы следующие работы:

1. Нестеренко А.К., Данилина A.A., Сысоев Т.М., Бездушный А.Н., Серебряков В.А. Автоматизация процессов интеграции распределенных информационных ресурсов // Электронные библиотеки: перспективные методы и технологии, электронные коллекции: Труды VIII всероссийской научной конференции. /Ярославский государственный университет им. П.Г. Демидова. - Суздаль, 2006. - С. 279-290.

2. Данилина A.A. Автоматическая оптимизация потоков работ // Современные проблемы фундаментальных и прикладных наук: Труды 51-й научной конференции

МФТИ. /МФТИ.- Москва-Долгопрудный , 2008.-4.VII ,Т.З - С.88-90.

3. Каленкова A.A. Операционная семантика потоков работ // Информационные технологии и системы: наука и практика: Труды IV международной конференции. /Владикавказский научный центр РАН и Правительства Республики Северная Осетия — Алания - Владикавказ, 2009 - 4.2 - С. 108-111.

4. Каленкова A.A. Оптимизация потоков работ по времени выполнения, основанная на удалении избыточных потоков управления // Труды МФТИ, 2009. - Т. 1, №. 2 - С.160-175.

5. Каленкова A.A. Метод верификации потоков работ, основанный на построении логических выражений // Современные проблемы фундаментальных и прикладных наук: Труды 52 научной конференции МФТИ. /МФТИ.- Москва-Долгопрудный , 2009. - 4.VII ,Т.2 -С.125-128.

6. Каленкова A.A., Серебряков В.А., Бездушный А.Н. Система автоматической верификации и оптимизации потоков работ // Телематика: Труды XVII всероссийской научно-методической конференции. /Санкт-Петербургский государственный университет информационных технологий механики и оптики. - Санкт-Петербург, 2010. - С. 381-382.

7. Каленкова A.A. Применение условной конверсии для верификации и оптимизации потоков работ // Программирование - 2010. - Т.36, №. 5 - С.38-53.

8. Каленкова A.A. Использование системы автоматической верификации и оптимизации потоков работ для анализа процессов обработки информационных ресурсов в электронной библиотеке // Распределенные информационно-вычислительные ресурсы" (DICR'2010). / Институт вычислительных технологий СО РАН. -Новосибирск, 2010. - С. 17.

Подписано в печать 03.11.2011. Формат 60x90/16 Бумага офсетная. Усл. печ. л. 1,25 Тираж 100 экз. Заказ 146

Отпечатано в Копировальные центры ФАН, ООО «Техноком» 119261, Москва, Ленинский проспект, д. 85

Оглавление.

Введение.

Актуальность темы.

Цель и задачи работы.

Основные результаты работы.

Научная новизна работы.

Практическая значимость.

Доклады и печатные публикации.

Структура и объем диссертации.

Краткое содержание работы.

Глава 1 Потоки работ, двустороннее отображение между формулами потоков работ и их графовым представлением.

1.1 Обзор языков описания потоков работ, системы управления потоками работ

1.2 Промежуточные представления потоков работ.

1.2.1 Размеченные графы анализа потоков работ.

1.2.2 Формальный язык описания потоков работ.

1.2.3 Сети потоков работ.

1.2.4 Графы потоков работ.

1.2.5 Выразительные возможности промежуточных представлений потока работ

1.3 Двустороннее отображение между Формальным языком описания потоков работ и Размеченными графами анализа потоков работ.

1.3.1 Алгоритм построения Размеченного графа анализа потока работ по Формальному описанию потока работ.

1.3.2 Алгоритм построения Формального описания потока работ по Размеченному графу анализа потока работ.

1.4 Выводы.

Глава 2 Алгоритмы анализа и преобразования потоков работ.

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

2.1.1 Структурные конфликты и алгоритмы верификации потоков работ.

2.1.2 Алгоритм булевой верификации (АБВ) потоков работ.

2.1.2.1 Структурные конфликты в Размеченных графах анализа потоков работ без ориентированных циклов.

2.1.2.2 Алгоритм булевой верификации потоков работ (АБВ) для графов без ориентированных циклов.

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

2.1.2.4 Алгоритм булевой верификации потоков работ (АБВ) для графов с ориентированных циклами.

2.1.2.5 Сравнение АБВ с другими алгоритмами верификации потоков работ.

2.2 Алгоритм структурной оптимизации потоков работ.

2.2.1 Алгоритм структурной оптимизации Размеченных графов анализа потоков работ.

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

2.2.3 Получение Формального описания потока работ по оптимизированному Размеченному графу анализа потока работ.

2.3 Обоснование алгоритмов верификации и оптимизации потоков работ.

2.3.1 Обоснование алгоритма булевой верификации (АБВ) для графов без ориентированных циклов.

2.3.2 Обоснование алгоритма структурной оптимизации Размеченных графов анализа потоков работ.

2.4 Выводы.

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

3.1 Преобразование BPEL-процессов в Формальное описание потоков работ

3.1.1 XML-представление Формального языка описания потоков работ.

3.1.2 Основные конструкции языка BPEL.

3.1.3 Преобразование BPEL-процесса в Формальное описание потока работ

3.1.4 Получение BPEL-процесса по Формальному описанию потока работ.

3.2 Реализация и применение алгоритмов анализа потоков работ.

3.2.1 Система автоматической верификации и оптимизации потоков работ.

3.2.2 Система управления электронной библиотекой «Научное наследие России»

3.2.3 Анализ процесса удаления книги в Электронной библиотеке «Научное

Наследие России».

3.3 Выводы.

Актуальность темы

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

Цель и задачи работы

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

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

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

3. Для унифицированного анализа блочно-графовых языков описания потоков работ используется промежуточное блочно-графовое представление. Необходимы алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и предложенным в литературе блочно-графовым базисным Формальным языком описания потоков работ.

4. Разработка алгоритмов двустороннего отображения между Формальным языком описания потоков работ и языком ВРЕЬ для оценки практического применения алгоритмов анализа потоков работ.

Основные результаты работы

В рамках диссертационной работы получены следующие результаты:

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

2. Для унифицированного анализа блочно-графовых языков описания потоков работ разработаны алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и блочно-графовым базисным языком описания потоков работ, а также алгоритмы двустороннего отображения между блочно-графовым базисным языком описания потоков работ и языком ВРЕЬ.

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

4. Была предложена теоретическая основа для эквивалентных преобразований потоков работ.

5. Была разработана Система автоматической верификации и оптимизации потоков работ, в которой были реализованы предложенные алгоритмы.

6. Был создан прототип Системы управления электронной библиотекой «Научное наследие России», который исполняет ВРЕЬ-процессы, координирующие работу библиотеки. Был произведен анализ этих процессов.

Научная новизна работы

Научной новизной обладают следующие результаты диссертационной работы:

1. Предложены новые эффективные алгоритмы верификации и оптимизации (распараллеливания независящих по данным действий) потоков работ.

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

3. Разработаны алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и блочно-графовым представлением потока управления.

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

Разработанные промежуточное графовое представление потока управления и потока данных, алгоритмы работы с этим представлением, алгоритмы двустороннего отображения между этим представлением и блочно-графовым Формальным языком описания потоков работ, а также алгоритмы двустороннего отображения между конструкциями языка ВРЕЬ и Формальным языком описания потоков работ позволили создать Систему автоматического анализа и преобразования ВРЕЬ-процессов. Эта система была использована для анализа и преобразования производственных процессов Электронной библиотеки «Научное наследие России», формализованных с помощью языка ВРЕЬ. На основе доступных открытых кодов был создан прототип системы исполнения ВРЕЬ-процессов Электронной библиотеки «Научное наследие России».

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

Доклады и печатные публикации

Основные положения работы докладывались на восьмой всероссийской научной конференции «Электронные библиотеки: перспективные методы и технологии, электронные коллекции» (2006 г.), на 51-ой научной конференции «Современные проблемы фундаментальных и прикладных наук» (2008 г.), на четвертой международной конференции «Информационные технологии и системы: наука и практика» (2009 г.), на 52-ой научной конференции «Современные проблемы фундаментальных и прикладных наук» (2009 г.), на 17-ой всероссийской научно-методической конференции «Телематика» (2010 г.), на 13-ой всероссийской конференции «Распределенные информационно-вычислительные ресурсы» (2010 г.). Были опубликованы работы в журналах «Труды МФТИ» (2009 г.) и «Программирование» (2010 г.) Всего по материалам диссертации опубликовано 8 печатных работ [1,2,3,4,5,6,7,8].

Структура и объем диссертации

Работа состоит из введения, трех глав, заключения, списка литературы и трех приложений. Общий объем диссертации 164 страницы. Список литературы содержит 42 наименования.

3.3 Выводы

Было приведено описание основных конструкций ВРЕЬ, среди них были выделены те, для которых может быть произведено отображение в конструкции Формального языка описания потоков работ и в Размеченные графы анализа потоков работ. В силу того, что ВРЕЬ является блочно-графовым языком, структурные конфликты, встречающиеся в потоках работ, которые не имеют блочной структуры, такие как «мертвый цикл», «бесконечный цикл» и «ветвящийся цикл» не будут появляться в Размеченных графах анализа потоков работ, соответствующих ВРЕЬ-процессам. Однако обратные дуги графов, сформированные связями, запрещены ВРЕЬ спецификацией и могут быть обнаружены с помощью предлагаемых алгоритмов анализа. Кроме того, в ВРЕЬ-процессах будут выявлены конфликты типа «тупик» и «недостаток синхронизации». Сохранение в ходе выполнения оптимизации специфичных для ВРЕЬ атрибутов и элементов, отвечающих за исполнение ВРЕЬ-процессов, позволяет построить алгоритм их автоматической оптимизации. Автоматическая оптимизация ВРЕЬ-процесса имеет большое практическое значение, так как в настоящее время не существует алгоритмов и систем, позволяющих автоматически в полной мере распараллеливать блочно-графовые потоки работ.

Было приведено описание Системы автоматической верификации и оптимизации потоков работ, реализующей предлагаемые алгоритмы анализа, преобразования и отображения. Были изложены основные принципы работы Электронной библиотеки «Научное Наследие России», обоснована необходимость использования системы управления потоками работ для формализации и автоматизации управления процессами в электронной библиотеке, в качестве такой системы специально была разработана Система управления Электронной библиотекой «Научное наследие России», отвечающая за исполнение ВРЕЬ-описаний процессов. Был рассмотрен ВРЕЬ-процесс удаления книги в Электронной библиотеке «Научное наследие России», проведен его анализ и автоматическая оптимизация.

Заключение

В диссертационной работе получены следующие результаты:

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

2 Разработаны алгоритмы двустороннего отображения между созданным промежуточным графовым представлением и блочно-графовым базисным Формальным языком описания потоков работ, а также алгоритмы двустороннего отображения между Формальным языком описания потоков работ и языком ВРЕЬ.

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

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

5 Была разработана Система автоматической верификации и оптимизации Размеченных графов анализа потоков работ, в которой были реализованы предложенные алгоритмы.

6 Был создан прототип Системы управления электронной библиотекой «Научное наследие России», который исполняет ВРЕЬ-процессы, координирующие работу библиотеки. Был произведен анализ этих процессов.

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

1. Нестеренко А.К., Данилина A.A., Сысоев Т.М., Бездушный А.Н., Серебряков

2. Данилина A.A. Автоматическая оптимизация потоков работ // Современные проблемы фундаментальных и прикладных наук: Труды 51-й научной конференции МФТИ. /МФТИ.- Москва-Долгопрудный , 2008.- 4.VII ,Т.З1. C.88-90.

3. Каленкова A.A. Оптимизация потоков работ по времени выполнения, основанная на удалении избыточных потоков управления // Труды МФТИ, 2009. Т.1, №. 2 - С.160-175.

4. Каленкова A.A. Метод верификации потоков работ, основанный на построении логических выражений // Современные проблемы фундаментальных и прикладных наук: Труды 52 научной конференции МФТИ. /МФТИ,- Москва-Долгопрудный , 2009. 4.VII ,Т.2 - С.125-128.

5. Каленкова A.A. Применение условной конверсии для верификации и оптимизации потоков работ // Программирование 2010. - Т.36, №. 5 -С.38-53.

6. Нестеренко А.К. Формализация потоков работ и ее применение. -Диссертация на соискание степени кандидата технических наук: 05.13.18 / А.К. Нестеренко. Москва, 2007. - 100 С.

7. Aalst W.M.P., Hirnschall A., Verbeek H.M.W. An Alternative Way to Analyze Workflow Graphs // Electronic Commerce Research 2002. - V.2, №.3 - P. 195231.

8. Terminology & Glossary / Workflow Management Coalition. 1999. - URL: http://www.wfmc.org/Download-document/WFMC-TC-101 l-Ver-3-Terminology-and-Glossary-English.html.

9. Вендров A.M. Проектирование программного обеспечения экономических информационных систем. М.: Финансы и статистика - 2005. - С. 544.

10. OMG Unified Modeling LanguageTM (OMG UML), Superstructure. FTF Version 2.4 / Object Management Group 2010. - URL: http ://w w w. omg. org/sp ec/UML/2.4/Infrastructure/B eta2/PDF.

11. Business Process Model and Notation (BPMN). FTF Beta 1 for Version 2.0 / Object Management Group 2009. - URL: http://www.omg.org/cgi-bin/doc?dtc/09-08-14.pdf.

12. Process Definition Interface XML Process Definition Language 2.1a / Ed. by Shapiro R., Swenson K., Brunt J., et al. - 2008. - URL: http://www.wfmc. org/index.php?option=comdocman&task=docdownload&Ite mid=72&gid=132.

13. Web Services Business Process Execution Language Version 2.0 / Ed. by Alves A., Arkin A., Askary S. 2007. - URL: http://docs.oasis-open.org/wsbpel/2.0/0s/wsbpel-v2.0-0s.html.

14. BPML working draft 2002. - URL: http://xml.coverpages.org/bpml.html

15. Web Services Flow Language 1.0 Specification. 2001. - URL: http://xml.coveфages.org/wsfl.html/

16. XLANG Web Services for Business Process Design 2001. - URL: http://xml.coverpages.org/XLANG-C-200106.html

17. WS-BPEL Extension for People specification, vl.O / Ed. by Agrawal A., Amend1. M., Das М.- 2007. URL: http://public.dhe.ibm.com/software/dw/specs/wsbpel4people/ BPEL4Peoplevl.pdf.

18. Russell N.C., Hofstede A.H.M:, Aalst W.M.P., derMulyar N.A. Workflow control-flow patterns: a revised view. / BPM Center Report, No. BPM-06-22. -Eindhoven: BPMcenter.org 2006. - P. 134.

19. Jensen K. Coloured Petri Nets. Springer - 1997.

20. Mendling J., Lassen K., Zdun U. Transformation strategies between block-oriented and graph-oriented process modelling languages // Multikonferenz Wirtschaftsinformatik 2006. - P. 297-312.

21. Aalst W.M.P. A class of Petri net for modeling and analyzing business processes // Computing Science Reports No. 95. / Eindhoven University of Technology -1995.

22. Aalst W.M.P. Verification of Workflow Nets //

23. Application and Theory of Petri Nets Berlin: Springer-Verlag, 1997. - V. 1248 -P. 407-426.

24. Kemper. P. Linear Time Algorithm to Find a Minimal Deadlock in a Strongly Connected Free-Choice Net // Application and Theory of Petri Nets Berlin: Springer-Verlag, 1993,-V. 691 - P. 319-338.

25. Lin H., Zhao Z., Li H., Chen Z. A Novel Graph Reduction Algorithm to Identify Structural Conflicts // Proceedings of the 35th Annual Hawaii International Conference on System Sciences 2002. - V.9 - P. 289.

26. Bi H.H., Zhao J.L. Applying Propositional Logic to Workflow Verification // Information Technology and Management. 2004. - V. 5, №. 3-4. - P. 293-318.

27. Толстов E.B. Задачи моделирования потоков работ при помощи сетей Петри. Диссертация на соискание степени кандидата технических наук: 05.13.18 / Е.В. Толстов. - Москва, 2006. - 145 С.

28. Кормен Т., Лейзерсон Ч., Ривест Р., Штайн К. Алгоритмы. Построение и анализ. Издание 2-е. М.: Вильяме, 2007.

29. Kennedy К., Allen J.R. Optimizing compilers for modern architectures: adependence-based approach. San Francisco: Morgan Kaufmann Publishers Inc., 2001.

30. Евстигнеев В.А., Касьянов B.H. Сводимые графы и граф-модели в программировании. Новосибирск.: ИДМИ, 1999.

31. Ахо А.,Сети Р., Ульман Д. Компиляторы. Принципы, технологии, инструменты — М.: Вильяме, 2003.

32. Netjes M., Reijers H.A., Aalst W.M.P. On the Formal Generation of Process Redesigns // First International Workshop on Model-Driven Engineering For Business Process Management 2008. - P. 49-60.

33. Cao H., Jin H., Wu S., Tao Y. PGWFT: A Petri Net Based Grid Workflow Verification and Optimization Toolkit // Advances in Grid and Pervasive Computing. Third International Conference 2008. - P. 48-58.

34. Chen S., Bao L., Chen P. OptBPEL: A Tool for Performance Optimization of BPEL Process // Software composition. 2008. - V. 4954. - P. 141-148.

35. Web Services Activity URL: http://www.w3.org/2002/ws/.

36. Web Services Description Language (WSDL) Version 2.0 Part 1: Core Language URL: http://www.w3.org/TR/2004/WD-wsdl20-20040326/

37. Apache ODE URL: http:// http://ode.apache.org/