Use of tableau algorithm for business process verification

Title:

Authors: Alexander G. Ivashko, Andrey V. Grigoryev, Alexander A. Kropotin, Ekaterina O. Ovsyannikova

About the authors:

Alexander G. Ivashko, Dr. Sci. (Tech.), Professor, Department of Program and System Engineering, University of Tyumen; a.g.ivashko@utmn.ru

Andrey V. Grigoryev, postgraduate student, Institute of Mathematics, Humanities and Information Technologies, Tyumen State University
Alexander A. Kropotin, Cand. Sci. (Phys.-Math.), Senior Lecturer, Department of Software and Systems Engineering, University of Tyumen; a.a.kropotin@utmn.ru

Ekaterina O. Ovsyannikova, postgraduate student, Institute of Mathematics, Humanities and Information Technologies, Tyumen State University

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.

References:

1. Wynn, M.T., Verbeek, H.M.W., W.M.P. van der Aalst, A.H.M. ter Hofstede, Edmond,

D. Business Process Verification — Finally a Reality! // Business Process Management Journal, Vol. 15(1), Pp.74-92.

2. Dijkman, R.M., Dumas, M., Ouyang, C. Formal Semantics and Analysis of BPMN Process Models using Petri Nets // Intelligent Information Technology Application. IITA '08. Second International Symposium. 2008. Pp. 70-74.

3. Lopez-Grao, J.P., Merseguer, J., Campos, J. From UML Activity Diagrams To Stochastic Petri Nets: Application To Software Performance Engineering* // Intelligent Information Technology Application, 2008. IITA '08. Second International Symposium. 2008. P 70-74.

4. Object Management Group. Business Process Model and Notation (BPMN) Version 2.0 // http://www.omg.org/spec/BPMN/2.0/PDF (дата обращения: 18.05.2013)

5. Beeri, C., Eyal, A., Kamenkovich, S., Milo, T. Querying business processes // In VLDB 06. 2006. Pp. 343-354.

6. Dimitrov, M., Simov, A., Stein, S., Konstantinov, M. A bpmo based semantic business process modeling environment // In Proceedings of the Workshop on Semantic Business Process and Product Lifecycle Management at the ESWC, vol. 251 of CEUR-WS, 2007.

7. Koschmider, A., Oberweis, A. Ontology based business process description // In Proceedings of the CAiSE-05 Workshops, LNCS. 2005. Pp. 321-333.

8. Markovic, I. Advanced querying and reasoning on business process models.

In W. Abramowicz and D. Fensel, editors, BIS. Vol. 7 of Lecture Notes in Business Information Processing. 2008. Pp. 189-200.

9. De Nicola, A., Lezoche, M., Missikoff, M. An ontological approach to business process modeling // In Proceedings of the 3d Indian International Conference on Artificial Intelligence (IICAI). 2007. Pp 1794-1813.

10. Thomas, O., Fellmann, M. Semantic epc: Enhancing process modeling using ontology languages // In Proceedings of the Workshop on Semantic Business Process and Product Lifecycle Management (SBPM). 2007. Pp. 64-75.

11. Weber, I., Hoffmann, J., Mendling, J. Semantic business process validation // In Proceedings of the Workshop on Semantic Business Process and Product Lifecycle Management (SBPM). 2008.

12. Wong, P.Y.H., Gibbons, J. A relative timed semantics for BPMN // In Proceedings of 7th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA08). 2008.

13. Born, M., Dorr, F., Weber, I. User-friendly semantic annotation in business process modeling // In Hf-SDDM-07: Proceedings of the Workshop on Human-friendly Service Description, Discovery and Matchmaking WISE-07. 2007.

14. Di Francescomarino, C., Ghidini, C., Rospocher, M., Serafini, L., P. Tonella. Reasoning on semantically annotated processes // In Proc. of the 6th Int. Conference on Service Oriented Computing (ICSOC’08), Vol. 5364 of LNCS. 2008. Pp. 132-146.

15. Di Francescomarino, C., Ghidini, C., Rospocher, M., Serafini, L., Tonella, P. Semanticallyaided business process modeling // In Proceedings of 8th International Semantic Web Conference (ISWC 2009). 2009. Pp. 114-129.

16. Ghidini, C., Rospocher, M., Serani, L. A formalisation of BPMN in description logics // Technical Report TR 2008-06-004, FBK, 2008.

17. Bozzato, L., Ferrari, M., Trombetta, A. Building a domain ontology from glossaries: a general methodology // In Proceedings of 5th Workshop on Semantic Web Applications and Perspectives, 2008.

18. Van Dongen, B.F. and Verbeek, H.M.W. Verification of EPCs: Using Reduction Rules and Petri Nets // Proceedings of the 17th Conference on Advanced Information Systems Engineering (CAiSE’05), Vol. 3520 of Lecture Notes in Computer Science. 2005. Pp. 372-386;

19. White, S. Process Modeling Notations and Workflow Patterns // In Workflow Handbook, 2004. Pp. 265-294.

20. MDT Papyrus Group. Papyrus // URL: http://www.eclipse.org/papyrus/ (дата обращения: 20.05.2013).

21. Baader, F., Calvanese, D., McGuinness, D., Nardi, D. and Patel-Schneider, P.F. (editors). The Description Logic Handbook: Theory, Implementation and Applications. CUP, 2003.

22. Schmidt-Schau, M. and Smolka, G. Attributive concept descriptions with complements // Artificial Intelligence, Vol. 48(1). 1991. Pp. 1-26.

23. Horrocks, I., Motik, B., Wang, Z. The HermiT OWL Reasoner // In Proc. ORE 2012.

Pp. 136-141. references

1. Wynn, M.T., Verbeek, H.M.W., W.M.P. van der Aalst, A.H.M. ter Hofstede, Edmond,

D. Business Process Verification — Finally a Reality! Business Process Management Journal. Vol. 15(1), Pp. 74-92.

2. Dijkman, R.M., Dumas, M., Ouyang, C. Formal Semantics and Analysis of BPMN

Process Models using Petri Nets. Intelligent Information Technology Application. IITA '08. Second International Symposium. 2008. Pp. 70-74.

3. Lopez-Grao, J.P., Merseguer, J., Campos, J. From UML Activity Diagrams To StochasticPetri Nets: Application To Software Performance Engineering*. Intelligent Information Technology Application, 2008. IITA '08. Second International Symposium. 2008. Pp.70-74.

4. Object Management Group. Business Process Model and Notation (BPMN) Version 2.0 // http://www.omg.org/spec/BPMN/2.0/PDF (дата обращения: 18.05.2013)

5. Beeri, C., Eyal, A., Kamenkovich, S., Milo, T. Querying business processes // In VLDB

06. 2006. Pp. 343-354.

6. Dimitrov, M., Simov, A., Stein, S., Konstantinov, M. A bpmo based semantic business

process modeling environment. In Proc. of the Workshop on Semantic Business Process and Product Lifecycle Management at the ESWC. Vol. 251 of CEUR-WS, 2007.