Application of Deductive Reasoning to the Verification of Archimate Behavioral Elements

• Autorzy: Radosław Klimek , Piotr Szwed , Stanisław Jędrusik

Warianty tytułu

Zastosowanie wnioskowania dedukcyjnego do weryfikacji opisów zachowania w języku ArchiMate

• Języki publikacji: EN

Abstrakty

EN

The formal verification of business models has recently become an intensively researched area. It is expected that the application of formal tools may bring such benefits to organizations as the improved quality of products and services and a lower ratio of operational errors. In this paper we discuss the application of a deduction-based method for the verification of the behavioral aspects of ArchiMate models. The first step in our method consists in the translation of the ArchiMate model into Linear Temporal Logic (LTL) formulas. The resulting LTL formulas are then verified to check the expected temporal properties. The verification process is based on the semantics tableaux method and is conducted with an LTL prover. The method is discussed using an example of a business process implemented within a surveillance system.(original abstract)

Formalna weryfikacja modeli biznesowych stała się ostatnio przedmiotem intensywnych badań. Oczekuje się, że zastosowanie metod formalnych może przynieś takie korzyści, jak zwiększenie jakości produktów i usług oraz zmniejszenie liczby błędów operacyjnych. W pracy omówiono zastosowanie metody wykorzystującej wnioskowanie dedukcyjne do weryfikacji elementów behawioralnych w modelach języka ArchiMate. Pierwszy krok zaproponowanej metody polega na translacji modelu ArchiMate do postaci formuł liniowej logiki temporanej (LTL). Następnie weryfikuje się, czy spełniają one założone własności temporalne. W procesie weryfikacji używane jest narzędzie dowodzenia, w którym zastosowano technikę tablic semantycznych. Opisując metodę weryfikacji, wykorzystano przykład procesu biznesowego zaimplementowanego w systemie nadzoru.(abstrakt oryginalny)

Słowa kluczowe

EN

Software; Logic; Business models

PL

Oprogramowanie; Logika; Modele biznesowe

• Czasopismo: Informatyka Ekonomiczna / Uniwersytet Ekonomiczny we Wrocławiu
• Rocznik: 2013
• Numer: nr 3 (29)
• Strony: 76--97

Twórcy

autor

Radosław Klimek

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

autor

Piotr Szwed

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

autor

Stanisław Jędrusik

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

Bibliografia

• Anderson B., Hansen J.V., Lowry P., Summers S., Model checking for e-business control and assurance, "Systems, Man, and Cybernetics, Part C: Applications and Reviews", IEEE Transactions on 2005, vol. 35, no. 3, pp. 445-450.
• Archi, ArchiMate modelling tool, 2013, http://archi.cetis.ac.uk/download.html [accessed: 23 April 2013].
• Azevedo C., Almeida J., Van Sinderen M., Quartel D., Guizzardi G., An ontology-based semantics for the motivation extension to ArchiMate, [in:] Enterprise Distributed Object Computing Conference (EDOC), 2011 15th IEEE International, 2011, pp. 25-34.
• Clarke E., Grumberg O., Peled D., Model Checking, MIT Press, 1999.
• Clarke E., Wing J. et al., Formal methods: State of the art and future directions, "ACM Computing Surveys" 1996, vol. 28 (4), pp. 626-643.
• d'Agostino M., Gabbay D., Hähnle R., Posegga J., Handbook of Tableau Methods, Kluwer Academic Publishers, 1999.
• De Boer F., Bonsangue M., der Doest H., Groenewegen L., Jonkers H., Stam A., van der Torre L., Analysis of Enterprise Architectures (q4), 2003, https://doc.telin.nl/dscgi/ds.py/Get/File-31618 [accessed: 15 June 2013].
• Deutsch A., Hull R., Patrizi F., Vianu V., Automatic verification of data-centric business processes, [in:] Proceedings of the 12th International Conference on Database Theory ACM, 2009, pp. 252-267.
• Emerson E., Handbook of Theoretical Computer Science, Elsevier, MIT Press, 1990, vol. B, Temporal and Modal Logic, pp. 995-1072.
• Ettema R., Dietz J., ArchiMate and DEMO - Mates to date?, [in:] Advances in Enterprise Engineering III, ser. Lecture Notes in Business Information Processing, eds. A. Albani, J. Barjis, J. Dietz, Springer Berlin Heidelberg, 2009, vol. 34, pp. 172-186, http://dx.doi.org/10.1007/978-3-642-01915-9_13 [accessed: 20 June 2013].
• Wolter F., Wooldridge M., Temporal and dynamic logic, "Journal of Indian Council of Philosophical Research" 2011, vol. XXVII(1), pp. 249-276.
• Fu X., Bultan T., Su J., Formal verification of e-services and workflows, [in:] Web Services, E-Business, and the Semantic Web, Springer, 2002, pp. 188-202.
• Gruninger M., Fox M.S., An activity ontology for enterprise modelling, Department of Industrial Engineering, University of Toronto, 1994.
• Huth M., Ryan M., Logic in Computer Science. Modelling and Reasoning about Systems, Cambridge University Press, 2004.
• Mongiello M., Castelluccia D., Modelling and verification of BPEL business processes, [in:] Model-Based Development of Computer-Based Systems and Model-Based Methodologies for Pervasive and Embedded Software, 2006, MBD/MOMPES 2006, Fourth and Third International Workshop on IEEE, 2006, p. 5.
• Morimoto S., A survey of formal verification for business process modeling, [in:] Proceedings of the 8th International Conference Computational Science (ICCS 2008), June 23-25, 2008, Kraków, Poland, Part II, ser. Lecture Notes in Computer Science, eds. M. Bubak, G.D. van Albada, J. Dongarra, P.M.A. Sloot, vol. 5102, Springer Verlag, 2008, pp. 514-522.
• Nick M., Will there be a battle between ArchiMate and the UML?, 2009, http://blogs.msdn.com/b/nickmalik/archive/2009/04/17/will-there-be-a-battle-between-ArchiMate-and-the-uml.aspx [accessed 10 June 2013].
• OMG, Business Process Model and Notation (BPMN) version 2.0, OMG, Tech. Rep., January 2011. http://www.omg.org/spec/BPMN/2.0 [accessed 10 June 2013].
• Rumbaugh J., Jacobson I., Booch G., Unified Modeling Language Reference Manual, 2nd edition. Pearson Higher Education, 2004.
• Scheer A., Aris - Business Process Modeling, ser. ARIS - Business Process Modeling, Springer, 1999.
• Scheer A.-W., Nüttgens M., ARIS architecture and reference models for business process management, [in:] Business Process Management, Springer, 2000, pp. 376-389.
• Shankar N., Automated deduction for verification, "ACM Computing Surveys" 2009, vol. 41 (4), pp. 20:1-20:56.
• Szwed P., Chmiel W., Jedrusik S., Kadluczka P., Business processes in a distributed surveillance system integrated through workflow, "Automatyka/Automatics", in press, 2013.
• The Open Group, Open Group Standard, ArchiMate 2.0 Specificattion, 2012, http://www.opengroup.org [accessed: 11 July 2013].
• The Workflow Management Coalition, Process Definition Interface - XML Process Definition Language, Workflow Management Coalition Workflow Standard, version 2.1a, The Workflow Management Coalition, Tech. Rep., 2008, http://www.wfmc.org/Download-document/.
• Van Benthem J., Handbook of Logic in Artificial Intelligence and Logic Programming, ser. 4. Clarendon Press, 1993-95, ch. Temporal Logic, pp. 241-350.
• Van Den Berg H., Bosma H., Dijk G., Van Drunen H., Van Gijsen J., Langeveld F., Luijpers J., Nguyen T., Oosting R., Gerand Slagter and et al., ArchiMate made practical,Work, 2007.
• Van der Aalst W.M., Desel J., Kindler E., On the semantics of EPCs: A vicious circle, [in:] Proceedings of the EPK, 2002, pp. 71-80.
• Watahiki K., Ishikawa F., Hiraishi K., Formal verification of business processes with temporal and resource constraints, [in:] Systems, Man, and Cybernetics (SMC), 2011 IEEE International Conference on IEEE, 2011, pp. 1173-1180.
• WFMC-TC-1025-Oct-10-08-A-Final-XPDL-2.1-Specification.html [accessed: 11 July 2013].