Weryfikacja procesów biznesowych metodą dedukcyjną z wykorzystaniem logiki temporalnej

• Autorzy: Klimek R.

Warianty tytułu

EN

Deduction-based Formal Verification of Business Models using Temporal Logic

• Języki publikacji: PL

Abstrakty

PL

Praca dotyczy formalnej analizy i weryfikacji modeli biznesowych wyrażonych w notacji BPMN. Weryfikacja oparta jest na wnioskowaniu dedukcyjnym. Jako metodę wnioskowania dla modeli biznesowych zaproponowano metodę tablic semantycznych, która cechuje się apagogicznością oraz analitycznością. Została przedstawiona metoda translacji podstawowych wzorców projektowych BPMN do formuł logiki temporalnej, stanowiących logiczną specyfikację analizowanegomodelu. Zarówno logiczna specyfikacja, jak i właściwości badanych procesów są wyrażone formułami tzw. najmniejszej logiki temporalnej. Formuły te są następnie przetwarzane z wykorzystaniem metody tablic semantycznych. Innowacyjność proponowanego podejścia może istotnie wpłynąć na redukcję kosztów wytwarzania oprogramowania, ze względu na możliwość wykrycia błędów oprogramowania już w fazie jego modelowania, wyprzedzając tym samym znacznie fazy implementacji i testowania.

EN

The paper concerns formal analysis and verification of business models expressed in BPMN. This verification is based on a deductive reasoning. As a method of inference for business models semantic tableaux method is proposed. Automatic trans- formations of the basic BPMN workflow patterns to temporal logic formulas are proposed. These formulas constitute a logical specification of the analyzed model. Both the logical specification and the desired system properties are expressed as formulas of the smallest linear temporal logic. These formulas are later processed using semantic tableaux method. Applying this innovative concept might result in software development costs reduction as some errors might be addressed in the modeling phase not in implementation or testing phase.

Słowa kluczowe

PL

modele biznesowe; BPMN; SOA; wzorce projektowe; logika temporalna; wnioskowanie dedukcyjne; metoda tablic semantycznych; generowanie specyfikacji

EN

business models; BPMN; SOA; workflow design patterns; temporal logic; deductive reasoning; semantic tableaux method; generating specifications

• Wydawca: Sieć Badawcza Łukasiewicz - Przemysłowy Instytut Automatyki i Pomiarów PIAP
• Czasopismo: Pomiary Automatyka Robotyka
• Rocznik: 2011
• Tom: R. 15, nr 12
• Strony: 190--193
• Opis fizyczny: Bibliogr. 16 poz., rys.

Twórcy

autor

Klimek R.

• AGH Akademia Górniczo-Hutnicza, Wydział EAIiE, Katedra Automatyki,

Bibliografia

• 1. van der Aalst W.M.P., ter Hofstede A.H.M., Kiepusewski B., Barros A.P. (2003): Workflow Patterns. Distributed and Parallel Databases, 4(1), 2003, 5-51.
• 2. D’Agostino M., Gabbay D.M., Hanle R., Posegga J. (eds) (1999): Handbook of Tableau Methods, Kluwer Academic Publishers 1999.
• 3. van Benthem J. (1995): Temporal Logic. Clarendon Press 1993-95, 241-350.
• 4. Business Process Modeling Notation Specification. Version 1.2, January 2009, OMG Document dtc/2009-01-03.
• 5. Chellas B. (1980): Modal Logic, Cambridge University Press 1980.
• 6. Clarke E.M.Jr., Grumberg O., Peled D.A. (1999): Model Checking. MIT Press 1999.
• 7. Clarke E.M., Wing J.M. et al. (1996): Formal methods: State of the art and future directions, ACM Computing Surveys, 28(4), 1996, 626-643.
• 8. Emerson E.A. (1990): Temporal and Modal Logic, Elsevier, MIT Press 1990, 995-1072.
• 9. Hahnle R. (1998): Tableau-based Theorem Proving. ESSLLI Course 1998.
• 10. Klimek R. (1999): Wprowadzenie do logiki temporalnej, Wydawnictwa Naukowo-Techniczne AGH 1999.
• 11. Klimek R., Skrzyński P., Turek M. (2010): Deduction based verification of business models, [w:] Korczak J., Dudycz H., Dyczkowski M. (red.): Advanced Information Technologies for Management, (Research Papers of Wrocław University of Economics, 147), Publishing House of Wrocław University of Economics 2010, 173-188.
• 12. Ouyang C., Dumas M., ter Hofstede A.H.M., van der Aalst W.M.P. (2006): From BPMN Process Models to BPEL Web Services. IEEE International Conference on Web Services (ICWS’06), IEEE Computer Society 2006, 285-292.
• 13. Pelletier F.J. (1993): Semantic Tableau Methods for Modal Logics that Include the B and G Axioms. AAAI Technical Report FS-93-01, 1993.
• 14. Riehle D., Zullighoven H. (1996): Understanding and Using Patterns in Software Development. Theory and Practice of Object Systems, 2(1), 1996, 3-13.
• 15. 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 , 2006.
• 16. White S.A. (2005): Using BPMN to Model BPEL Process. BPTrends, 2005, 3, 1-18.