Use of tableau algorithm for business process verification

Abstract

The aim of this work is to develop the verification method of a businessprocess model applying the description logic instrument. The task of verification is to determine the presence of inconsistencies in the models, which can lead to unreachable actions. The article considers five main types of inconsistencies that arise from a business process modeling due to incorrect business-process representation and modification of a formalization method of the business process diagrams in BPMN and UML Activity notations as most widely-used. Limitations of existing approaches for verification are given, in particular the instrument of Petri Nets. The new method of verification with the help of only description logic formalism is suggested. The special software forming the knowledge base in OWL was developed for testing the above method. The tableaux algorithm was used as the instrument for reasoning and model inconsistencies detection. Examples of test models of different classes depending on their dimension and results of method testing are presented.

Целью работы является разработка метода верификации моделей бизнес-процессов с применением аппарата дескрипционных логик. Задача верификации заключается в определении наличия в моделях ошибок, которые могут привести к недостижимости тех или иных действий. В статье рассмотрены 5 основных типов ошибок, возникающих при моделировании в результате неправильного отображения бизнес-процесса, модифицирован метод формализации диаграмм бизнес-процессов в нотациях BPMN и UMLActivity как наиболее популярных среди используемых. Отмечены недостатки существующих подходов для верификации, в частности, инструмента сетей Петри. Предложен новый метод верификации моделей с помощью только лишь формализма дескрипционных логик. Для тестирования метода разработано программное обеспечение, формирующее базу знаний на языке OWL. Для осуществления логического вывода и поиска ошибок в моделях использовался табличный алгоритм. Представлены примеры тестовых моделей разных классов в зависимости от их размерности, а также результаты тестирования метода.