DOI: 10.12731/wsd-2014-6.1-8 УДК 004.4'242
ИСПОЛЬЗОВАНИЕ ПЕРСПЕКТИВ РЕСУРСОВ И УПРАВЛЕНИЯ ДЛЯ ВЕРИФИКАЦИИ ПОТОКОВ РАБОТ
Галочкин М.В.
Статья посвящена актуальной на сегодняшний день проблеме автоматической верификации потоков работ. На основе изучения существующих решений было установлено, что они не позволяют объединять различные перспективы потоков работ, и чаще всего, концентрируются на потоке управления. В связи с этим был разработан метод, объединяющий перспективы потоков работ, который позволяет находить ошибки синхронизации, взаимных блокировок и т.д. Путем анализа перспективы ресурсов и потока управления генерируется код на языке PROMELA. Полученный код может быть верифицирован с помощью SPIN, и в случае обнаружения ошибки построен контр пример. Для проведения экспериментов было разработано программное средство, доступное в открытом доступе. Положения данной статьи могут быть использованы для дальнейшего развития подхода, известного как «разработка потоков работ, управляемая моделями». Статья представляет интерес для специалистов в области разработки крупных программных систем, а также в областях, где необходимо создавать, верифицировать и исполнять потоки работ.
Ключевые слова: поток работ; верификация потока работ; SPIN, PROMELA; разработка, управляемая моделями; разработка потоков работ, управляемая моделями; системы управления потоками работ.
using perspectives of resources and control-flow for verification of workflows
Galochkin M.v.
This article is devoted to the subject of automatic verification of workflows. Based on the research of existing solutions, it was found that they don't allow you to integrate different workflows perspectives, and often focused on the control-flow perspective. Based on this, we developed a method integrating different perspectives of workflows, which lets you find synchronization errors, deadlocks, and so forth. By analyzing control-flow perspectives and resources, it generated a code on PROMELA. The resulting code can be verified by using the SPIN model checker, and if an error occurs, it constructs a counterexample. For the experiments, we developed an open-source software tool. The provisions of this article may be used for further development of this approach, known as a «model-driven workflow development». This article is of interest to specialists in the development of large software systems, as well as areas where it is necessary to create, verify and execute workflows.
Keywords: workflow; verification ofworkflow; SPIN; PROMELA; MDD; model driven workflow development; workflow management system.
Введение
Проблема верификации потоков работ была поставлена давно. Методы верификации workflow рассматривались в работах Wil van der Aalst [1, 2, 3], Kees van Hee [1], H. Brinksma [4] и др. Наиболее популярными подходами, в настоящий момент являются:
1. Применение формализма сетей Петри (используются различные подклассы сетей). Является наиболее популярным подходом для нахождения циклов, ошибок синхронизации, взаимных блокировок и т.д. в потоках работ. Данный подход был использован в работах Wil van der Aalst [3], H. Brinksma [4], Горбунова О.Е. (использует различные подклассы сетей Петри для различных типов workflow) [5], Толстова Е.В. (высокоуровневые сети Петри) [6]. Данный подход несмотря на свою популярность имеет ограничения. Например, широко используемое в программирование понятие «исключение» (exception), трудно описать в классических сетях Петри.
2. Применение теории графов. Рассматривается в работе Ко-робкова К.Н. [7].
3. Применение гибридных методов: объединение теории графов и сетей Петри. Представлен в работе Каленковой А.А. [8].
4. Использование графо-аналитического подхода. Описание графов с помощью формальных грамматик. Описан в работе Афанасьева А.Н. [9].
5. Использование simple promela Interpreter (spIN) [10] для моделирования и верификации. Рассматривался в работах Catia Vaz[11], Christian Wolter[12], и др.
Входными данными для вышеописанных методов часто являются либо модель, описывающая определенную часть потока работ (перспективу), либо модель на определенном языке описания потоков работ (BPEL, BPMN и т.д.). Под перспективой понимается, та часть реального потока, которой авторы уделяют особое внимание. Выделяют 5 основных перспектив [13, 14]: перспектива потока управления (описывает последовательность выполнения задач), перспектива данных (акцент на информацию и ее характеристики, которая передается между задачами [15]), перспектива ресурсов (акцент на ресурсы, необходимые для решения задач), перспектива обработки исключений (описание возможных исключительных ситуаций), операционная перспектива (акцент на операции над данными, возникающими в процессе выполнения потока работ).
Языки описания потоков работ чаще всего позволяют придерживаться лишь определенных перспектив, но не поддерживают все. Например BPMN [16] позволяет описывать поток управления (ветвление, циклы, потоки), частично поддерживает управление исключениями, но не позволяет описать ресурсы, необходимые для исполнения потока. Возможность объединения нескольких перспектив для более качественного анализа потоков работ является важной задачей для своевременного нахождения ошибок проектирования.
В программной инженерии в настоящий момент набирает популярность подход известный как разработка, управляемая моделями (MDD[17, 18]). Основная идея, которая лежит в основе MDD, является использование различных моделей (перспектив) будущей системы для автоматической генерации исполняемого кода. Программирование осуществляется только путем построения моделей, тогда как код генерируется автоматически. Наличие всех типов моделей является необязательным. Происходит постепенное «уточнение» требований к будущей системе. Примером такого подхода является схема базы данных, когда мы в графическом режиме описываем сущности, поля в них и связи между ними, а затем получаем SQL код заточенный под конкретную СУБД.
Основные принципы MDD могут быть задействованы и при разработке потоков работ. MDD требует наличия различных типов моделей, которыми в свою очередь, могут быть различные перспективы потока работ, описанные выше. Выходом MDD является исполняемый код, тогда как для потоков работ этим кодом будут инструкции для исполнителей либо код на определенном языке. В связи с этим можно говорить о разработке потоков работ, управляемой моделями (model driven workflow development - MDWD). Этот подход является очень молодым [19], а вопрос программирования потоков работ, на основе множества различных типов моделей требует более детального изучения.
Цель работы
Целью работы является объединение перспективы потока управления и перспективы ресурсов для верификации потока ра-
бот. Верификация осуществляется путем генерации кода на языке PROMELA из этих моделей с последующим исполнением в SPIN (Simple Promela Interpreter).
Материалы и методы исследования
Для исследования вопроса объединения различных перспектив (в настоящий момент поддерживается только перспектива потока управления и перспектива ресурсов) было создано программное средство. Все исходные коды доступны по адресу https://github.com/mixail7/diagramToPromela. Для работы необходим установленный SPIN версии 6.2.6 или более новый. Для работы программы diagramToPromela необходим Microsoft .NET Framework 4 (visual studio 2012 - для работы с исходным кодом).
Результаты исследования и их обсуждение
В результате исследования были выявлены следующие положения:
1. Существуют 5 основных методов верификации потоков работ на предмет наличия ошибок синхронизации, взаимных блокировок, достижимости и т.д.: использование различных видов сетей Петри, применение теории графов, применение гибридных методов (объединение теории графов и сетей Петри), использование графо-аналитического подхода, использование SPIN.
2. Существует 5 основных перспектив потока работ: перспектива потока управления, перспектива данных, перспектива ресурсов, перспектива обработки исключений, операционная перспектива.
3. Существующие методы верификации используют либо определенные перспективы потока работ (чаще всего перспективы потока управления), либо определенные языки, которые также имеют ориентацию на одной или нескольких перспектив. Методов и средств, поддерживающих интеграцию всех пяти перспектив в настоящий момент нет.
4. Подход программной инженерии, известный как «разработка, управляемая моделями» (MDD), может быть использован для разработки потоков работ, в том числе для верификации. Некоторые авторы вводят понятие «разработка потоков работ, на основе моделей» (Model Driven Workflow Development) [19].
5. Существующие средства перевода потоков работ в PROMELA не поддерживают все перспективы, а также имеют ограничение в 255 сущностей в рамках всех потоков работ (связано с методом перевода) [11, 19, 20].
6. Подход, объединения нескольких перспектив, рассмотренный ниже позволяет производить анализ потока работ с целью нахождения ошибок синхронизации, взаимных блокировок и т.д. и обладает практической ценностью.
В связи с вышеизложенным было принято решение о разработке программного средства позволяющего строить различные перспективы потока работ (в настоящий момент поддерживается перспектива потока управления и перспектива ресурсов) и генерировать код на языке PROMELA и обходить ограничения в 255 сущностей в потоках работ. Данное ограничение связано с тем
что spin допускает наличие не более 255 одновременно запущенных потоков (связано с алгоритмом анализа), а методы, представленные в [11, 19] предлагают каждую сущность потока работ представлять в виде отдельного потока. Такой поток инициализируется сразу при начале верификации и ожидает поступление сообщения на входную очередь. После поступления сообщения поток производит его передачу в входную очередь следующей сущности.
Таким образом происходит передача управления от одного элемента потока к другому.
Каждая сущность представляется ^^ отдельным потоком ^
Поток 3
Ожидать приход сообщения в очередь 3
Выполнение дей
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.