Диссертация (1152223), страница 78

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 78)

Поскольку мы ранее доказали, что BP-сеть относится именно к этому классу, мы можем воспользоваться этой теоремой, которая постулирует[305]: сеть Петри свободного выбора является живой и безопасной тогда и только тогда, когда­Сеть является связной и включает хотя бы одну позицию и один переход;­Существует позитивный P-инвариант матрицы инцидентности;­Существует позитивный T-инвариант матрицы инцидентности;­Ранг матрицы инцидентности RangА = |X| - 1, где |X| число кластеров сети.Покажем, что если BP-сеть является живой, безопасной, реверсивной и сохраняющей, тоBP-сеть обладает свойством нормального завершения.­Поскольку все начальные переходы tСi достижимы из начальной маркировки т.к.

связаны сней непосредственно входящими дугами (M0 [σr> MСi), учитывая, что сеть является активной,можно сделать вывод, что для каждого tСi существует своя последовательность срабатываний,обеспечивающая завершение (MСi [σr> M0).­Поскольку сеть является живой, то для каждого терминального перехода tТj существуеттакая маркировка, в которой этот терминальный переход tТj разрешён, иными словами, все терминальные состояния являются достижимыми.­Поскольку сеть является ограниченной, в любой позиции может находиться не более од-ного маркера. Теперь представим, что на одно входное воздействие в сети появилось несколькомаркеров, которые делают разрешёнными сразу несколько терминальных переходов tТj.

Еслисработает только один из них, то начальная позиция p0 будет достигнута, однако в сети останется по крайней мере один маркер, что противоречит критерию реверсивности. Если оба перехода сработают одновременно, то в домашней позиции p0 окажется сразу два маркера, что противоречит свойству ограниченности.Вычисление инвариантов матрицы инцидентностиИсходная сеть является чистой, ни одна из позиций не связана ни с одним переходом одновременно входящими и исходящими дугами, это важно при составлении матрицы инцидентности. Алгоритмы вычисления инвариантов [314], вычисления ранга матрицы и нахождения еёкластеров известны и описаны в литературе.

Рассмотри алгоритм Мартинеса-Сильвы [315].Принимая во внимание, что фундаментальное уравнение для нахождения P-инварианта показано в формуле (5.43):xT A = 0 .­(5.43)Шаг 1: Добавить (n × n) единичную матрицу к матрице инцидентности A, чтобы получить[A: I ].307­Шаг 2: Обнулить i столбец полученной матрицы [A: I ], складывая попарно любые строки[A: I ].­Шаг 3: Повторить последнюю операцию для всех столбцов j = 1,2,...,m (остановится, когда первые m столбцов будут обнулены).­Шаг 4: Удалить все обнуленные m столбцов, В результате останутся столбцы не обнуленные.­Шаг 5: Ранг полученной матрицы равен (n − r) .

Таким образом (n − r) строк являются линейно независимыми, мы получим минимальный P-инвариант.Следует обратить внимание, что этот алгоритм не гарантирует получение минимальногоинварианта, поскольку нет гарантии, что полученная матрица имеет именно (n – r) строк. Ноэто не опасно, во-первых, нам достаточно доказать существование любого положительного инварианта, во-вторых, нам заранее известен нужный размер, так что можно обнаружить линейнонезависимые строки.Поиск T-инварианта матрицы инцидентности осуществляется аналогично, с учётом того,что Ay = 0 ⇒ yT AT = 0 .

Необходимо вначале транспонировать матрицу инцидентности, затемвыполнить 5 шагов алгоритма Мартинеса-Сильвы, который приведён выше, с тем различием,что шаг 3 мы будем повторять i = 1,2,...,n раз, пока не обнулим i столбцов.Научная новизна предлагаемого аналитического метода формальной верификации моделипроцесса определяется следующим:В главе 2 мы сформулировали онтологические допущения, которые позволили теоретически обосновать критерии нормального завершения бизнес-процесса.

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

Таким образом, удалось теоретически обосновать класс СП, структурно эквивалентный модели процесса в нотации BPMN.–Установлено, что СП, структурно эквивалентная исходной диаграмме BPMN, являетсячистой (pure), не сдержит петель самозацикливания.308–Дано определение BP-сетей, которые адаптированы для анализа исполняемых моделейпроцессов в нотации BPMN. Сформулированы условия бездефектного завершения BP-сетей;–Найдены свойства, которые позволяют произвести исследование возможности бездефект-ного завершения BP-сети аналитическими методами;–Доказано, что эти условия являются необходимыми и достаточными для бездефектногозавершения BP-сетей;–Предложен алгоритм для проверки бездефектной завершаемости BP-сети.–Предложен аналитический метод формальной верификации модели процесса.

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

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

Поэтому мы опишем процедуру валидации,которая может быть выполнена на этапе макетирования.Будем помнить, что в основе разработки СУБП лежит модельно-ориентированный подход,так что описание функциональных требований происходит с использованием графических моделей, на основании которых генерируется программный код [316]. Разработка СУБП осуществляется в соответствии с коротким замкнутым циклом разработки. Короткий — означает, что разработка осуществляется в соответствии с принципами экстремального программирования. Замкну-309тый — означает, что изменения вносятся в исходную модель, программирование логики процессасведено к минимуму [317].

Данный подход к разработке СУБП позволяет изменить порядок фаз исостава проекта, по сравнению с традиционным водопадным подходом. Таким образом необходимо разработать новую методику ведения проекта по разработке внедрению СУБП.Валидация осуществляется с использованием прототипа СУБП, базирующегося на исполняемой модели бизнес-процесса в СУБП. Для валидации достаточно простейших пользовательских интерфейсов, автоматически создаваемых СУБП.

Интеграция на этом этапе осуществляется с помощью программных заглушек, реализующих режим ручного ввода данных. Дело в том,что проверка полноты данных на экранных формах должна осуществляться до начала работграфическому оформлению этих экранных форм. В отличие от метода читатель-писатель, применяемого при классическом реинжиниринге, валидация путём прототипирования позволяетбыстро и точно проверить логику процесса. Этапы разработки СУБП и участие в них бизнесаналитика и разработчика показаны на рисунке 5.30.Рисунок 5.30 - Валидация модели бизнес-процессаИсточник: составлено автором.Только после завершения валидации можно переходить к графическому оформлениюэкранных форм и интеграции процесса в ИТ инфраструктуру предприятия. Эти этапы так жевыполняются итерационно, периодически приходится возвращаться на предыдущий шаг с целью внесения изменений в исходную модель.Спиральная модель не различает разработку программного продукта и его сопровождение[297].

Положительное свойство метода в том, что он предлагает рассматривать поддержку, какразвитие и доработку системы. В то же время, этот подход затрудняет фиксацию окончательнойфункциональности в исходном задании на систему. Как следствие, у заказчика могут возникнуть ложные представления о трудозатратах и стоимости реализации полного проекта.Практическая значимость метода валидации исполняемой модели бизнес-процессаРанее было показано, что моделеориентированная разработка процессно-ориентирован-310ных систем заключается в том, что непосредственно из визуальной, графической модели бизнеспроцесса, созданной в стандартной для отрасли нотации моделирования бизнес-процессовBPMN, генерируется исполняемый программный код. Благодаря замкнутому циклу Моделирование ИсполнениеАнализ Модернизация, в СУБП реализована новая парадигма моделе-ориентированной разработки информационных систем с коротким и замкнутым циклом. В результате, центр тяжести в разработке перемещается с программиста на бизнес аналитика.

Характеристики

Список файлов диссертации