Abstract
In this paper we investigate the problem of verification of business processes specified with ArchiMate language. The proposed solution employs model checking techniques. As a verification platform the state of the art symbolic model checker NuSMV is used. We describe a method of fully automated translation of behavioral elements embedded in ArchiMate models into a representation in NuSMV language, which is then submitted to verification with respect to requirements expressed in CTL. The requirements specification can be entered by user, but we also propose to derive some of them automatically, based on analysis of control flows within business processes. The solution was implemented as a plugin to Archi, a popular ArchiMate modeling tool. Application of the method is presented on an example of a small business process.
Chapter PDF
Similar content being viewed by others
References
Anderson, B., Hansen, J.V., Lowry, P., Summers, S.: Model checking for e-business control and assurance. IEEE Transactions on Systems, Man, and Cybernetics, Part C: Applications and Reviews 35(3), 445–450 (2005)
Beauvoir, P.: Archi, archimate modelling tool (2015). http://www.archimatetool.com/ (accessed March 2015)
Bertoli, P., Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: Mbp: a model based planner. In: Proc. of the IJCAI 2001 Workshop on Planning Under Uncertainty and Incomplete Information (2001)
Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys (CSUR) 24(3), 293–318 (1992)
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E., Heinle, W.: Modular translation of statecharts to smv. Tech. rep., Citeseer (2000)
Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D.E., McMillan, K.L., Ness, L.A.: Verification of the futurebus+ cache coherence protocol. Formal Methods in System Design 6(2), 217–232 (1995)
Clarke, E.M., Klieber, W., Nováček, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1–30. Springer, Heidelberg (2012)
Clarke, E.M., Wing, J.M.: Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR) 28(4), 626–643 (1996)
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, pp. 252–267. ACM (2009)
Fu, X., Bultan, T., Su, J.: Formal verification of e-services and workflows. In: Bussler, C.J., McIlraith, S.A., Orlowska, M.E., Pernici, B., Yang, J. (eds.) CAiSE 2002 and WES 2002. LNCS, vol. 2512, pp. 188–202. Springer, Heidelberg (2002)
Fuxman, A., Pistore, M., Mylopoulos, J., Traverso, P.: Model checking early requirements specifications in tropos. In: Proceedings of the Fifth IEEE International Symposium on Requirements Engineering, pp. 174–181. IEEE (2001)
Huuck, R.: Formal verification, engineering and business value. In: Olveczky, P.C., Artho, C. (eds.) Proceedings First International Workshop on Formal Techniques for Safety-Critical Systems, Kyoto, Japan, November 12, 2012. Electronic Proceedings in Theoretical Computer Science, vol. 105, pp. 1–4. Open Publishing Association (2012)
Klimek, R., Szwed, P.: Verification of ArchiMate process specifications based on deductive temporal reasoning. In: Ganzha, M., Maciaszek, L.A., Paprzycki, M. (eds.) Proceedings of the 2013 Federated Conference on Computer Science and Information Systems, Kraków, Poland, September 8–11, 2013, pp. 1103–1110 (2013). http://fedcsis.org/2013/
Klimek, R., Szwed, P., Jedrusik, S.: Application of deductive reasoning to the verification of ArchiMate behavioral elements. Informatyka Ekonomiczna 29, 76–97 (2013)
Mongiello, M., Castelluccia, D.: Modelling and verification of BPEL business processes. In: Fourth and Third International Workshop on Model-Based Development of Computer-Based Systems and Model-Based Methodologies for Pervasive and Embedded Software, MBD/MOMPES 2006, p. 5-pp. IEEE (2006)
Morimoto, S.: A survey of formal verification for business process modeling. In: Bubak, M., van Albada, G.D., Dongarra, J., Sloot, P.M.A. (eds.) ICCS 2008, Part II. LNCS, vol. 5102, pp. 514–522. Springer, Heidelberg (2008)
OMG: Business Process Model and Notation (BPMN) version 2.0. Tech. rep., OMG, January 2011. http://www.omg.org/spec/BPMN/2.0
Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education (2004)
Szpyrka, M., Biernacka, A., Biernacki, J.: Methods of translation of Petri nets to NuSMV language. In: Popova-Zeugmann, L. (ed.) Proceedings of the 23th International Workshop on Concurrency, Specification and Programming, Chemnitz, Germany, September 29 - October 1, 2014. CEUR Workshop Proceedings, vol. 1269, pp. 245–256. CEUR-WS.org (2014). http://ceur-ws.org/Vol-1269/paper245.pdf
Szwed, P., Chmiel, W., Jedrusik, S., Kadluczka, P.: Business processes in a distributed surveillance system integrated through workflow. Automatyka/Automatics 17(1), 127–139 (2013)
The Open Group: Open Group Standard. Archimate 2.1 Specificattion. Van Haren Publishing, Zaltbommel (2013)
Watahiki, K., Ishikawa, F., Hiraishi, K.: Formal verification of business processes with temporal and resource constraints. In: 2011 IEEE International Conference on Systems, Man, and Cybernetics (SMC), pp. 1173–1180. IEEE (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 IFIP International Federation for Information Processing
About this paper
Cite this paper
Szwed, P. (2015). Verification of ArchiMate Behavioral Elements by Model Checking. In: Saeed, K., Homenda, W. (eds) Computer Information Systems and Industrial Management. CISIM 2015. Lecture Notes in Computer Science(), vol 9339. Springer, Cham. https://doi.org/10.1007/978-3-319-24369-6_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-24369-6_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24368-9
Online ISBN: 978-3-319-24369-6
eBook Packages: Computer ScienceComputer Science (R0)