Application of deductive reasoning to the verification of archimate behavioral elements

• Authors: Radosław Klimek , Piotr Szwed , Stanisław Jędrusik
• Languages of publication: EN

Abstracts

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.

Keywords

EN

Deductive temporal reasoning; software verification; ArchiMate; semantics table¬aux method; Linear Temporal Logic

• Publisher: Wydawnictwo Uniwersytetu Ekonomicznego we Wrocławiu
• Journal: Informatyka Ekonomiczna
• Year: 2013
• Issue: 3(29)
• Pages: 76-97

Contributors

author

Radosław Klimek

• AGH University of Science and Technology, Krakow

author

Piotr Szwed

• AGH University of Science and Technology, Krakow

author

Stanisław Jędrusik

• AGH University of Science and Technology, Krakow

References

• 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].