Deduction Based Verification of Business Models

• Autorzy: Radosław Klimek , Paweł Skrzyński , Michał Turek

Warianty tytułu

Weryfikacja modeli biznesowych metodą dedukcyjną

• Języki publikacji: EN

Abstrakty

EN

The paper presents a formal verification of the business processes expressed in BPMN. Verification is based on deductive reasoning. Automatic transformations of basic BPMN workflow patterns to temporal logic formulae are introduced. These formulae constitute a system specification and they are later processed using semantic tableaux method. In general, such reasoning technique has many advantages over the traditional approach, i.e., the resolution method. The paper provides automatic transformations for five basic BPMN workflow patterns and the example process is provided with description in BPMN diagram. The related temporal logic formula is obtained through automatic transformations, then the algorithm of reasoning using semantic tableaux methodology is applied to verify the business model. (original abstract)

Praca przedstawia formalną weryfikację procesów biznesowych wyrażonych w notacji BPMN. Weryfikacja jest oparta na wnioskowaniu logicznym. Została wprowadzona automatyczna transformacja wzorców procesowych BPMN do formuł logiki temporalnej. Formuły te składają się na logiczną specyfikację całego systemu i następnie są przetwarzane z wykorzystaniem metody tablic semantycznych. W ogólności, takie podejście do wnioskowania logicznego ma wiele zalet w porównaniu do podejścia tradycyjnego, opartego na metodzie rezolucji. W pracy pokazano automatyczną transformację formuł logicznych dla pięciu podstawowych wzorców procesowych BPMN, a także przedstawiono na diagramie BPMN pewien prosty model biznesowy. Odpowiednie formuły logiki temporalnej uzyskiwane są w sposób automatyczny, po czym proces wnioskowania logicznego z wykorzystaniem metody tablic semantycznych pozwala poddać weryfikacji sam model biznesowy. (abstrakt oryginalny)

Słowa kluczowe

EN

Business models; Logical analysis

PL

Modele biznesowe; Analiza logiczna

• Czasopismo: Prace Naukowe Uniwersytetu Ekonomicznego we Wrocławiu
• Rocznik: 2010
• Numer: nr 147 Advanced Information Technologies for Management - AITM 2010
• Strony: 173--188

Twórcy

autor

Radosław Klimek

• AGH University of Science and Technology Kraków, Poland

autor

Paweł Skrzyński

• AGH University of Science and Technology Kraków, Poland

autor

Michał Turek

• AGH University of Science and Technology Kraków, Poland

Bibliografia

• Booch G., Rumbaugh J., Jacobson R. (1998), The Unified Modeling Language User Guide, Addison-Wesley, Reading, MA.
• Business Process Modeling Notation Specification. Version 1.2 (2009), January, OMG Document dtc/2009-01-03.
• Clarke E.M. Jr., Grumberg O., Peled D.A. (1999), Model Checking, MIT Press, Cambridge, MA.
• Clarke E.M., Wing J.M. et al. (1996), Formal methods: State of the art and future directions, ACM Computing Surveys, Vol. 28, No. 4, pp. 626-643.
• Emerson E.A. (1990), Temporal and modal logic, [in:] Handbook of Theoretical Computer Science, Vol. B: Formal Models and Semantics, Elsevier, MIT Press, Amsterdam-Cambridge, MA, pp. 995-1072.
• Eshuis R., Wieringa R. (2003), Tool support for verifying UML activity diagrams, IEEE Transactions on Software Engineering, Vol. 30, No. 7, pp. 437-447.
• Gamma E., Helm R., Johnosn R., Vlissides J. (1995), Design Patterns: Elements of Reusable Object-Oriented Software, Addison-Wesley, Reading, MA.
• Handbook of Tableau Methods, Eds. M. D'Agostino, D.M. Gabbay, R. Hähnle, J. Posegga, Kluwer Academic Publishers, Dordrecht 1999.
• Klimek R. (1999), Wprowadzenie do logiki temporalnej, Wydawnictwo Akademii Górniczo-Hutniczej, Kraków.
• Klimek R., Skrzyński P., Turek M. (2010), Automatyczna weryfikacja modelu na etapie analizy wymagań, [in:] Inżynieria oprogramowania w procesach integracji systemów informatycznych, Eds. J. Górski, C. Orłowski, Pomorskie Wydawnictwo Naukowo-Techniczne, Gdańsk, pp. 209-216.
• Ma S., Zhang L., He J. (2008), Towards formalization and verification of unified business process model based on pi calculus, [in:] Proceedings of ACIS International Conference on Software Engineering Research, Management and Applications, 2008, 1, IEEE Computer Society, pp. 93-101.
• Riehle D., Zullighoven H. (1996), Understanding and using patterns in software development, Theory and Practice of Object Systems, Vol. 2, No. 1, pp. 3-13.
• Russell N., ter Hofstede A.H.M., van der Aalst W.M.P., Mulyar N. (2006), Workflow Control-Flow Patterns: A Revised View, BPM Center Report BPM-06-22, BPMcenter.org.
• Van Benthem J. (1995), Temporal logic, [in:] Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4, Eds. Dov M. Gabbay, C.J. Hogger, J.A. Robinson, Clarendon Press, Oxford, pp. 241-350.
• Van der Aalst W.M.P. (1998), The application of Petri nets to workflow management, The Journal of Circuits, Systems and Computers, Vol. 8, No. 1, pp. 21-66.
• Van der Aalst W.M.P. (2002), Making work flow: On the application of Petri nets to business process management, Lecture Notes in Computer Science, Vol. 2360: Application and Theory of Petri Nets, pp. 1-12, Springer-Verlag.
• Van der Aalst W.M.P., ter Hofstede A.H.M., Kiepusewski B., Barros A.P. (2003), Workflow patterns, Distributed and Parallel Databases, Vol. 4, No. 1, pp. 5-51.
• Wolper P. (1985), The tableau method for temporal logic: An overview, Logique et Analyse, Vol. 28, pp. 119-136.