Abstract
The motivation for our work was an idea of integrating formal verification with business processes modeling. In the presented approach ArchiMate was selected as a language used for definition of processes. We describe a procedure, which extracts behavioral elements from ArchiMate specification and transforms them into a corresponding representation used by NuSMV model checker. Then, we focus on time efficiency of the verification task. We give results of tests performed on a set of artificial process specifications, as well as on a complex business process, whose development was supported by the implemented solution. We compare three semantics of ArchiMate process definitions and discuss their influence on model complexity and verification time.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
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. Technical report, OMG, January 2011
Scheer, A.-W., Nüttgens, M.: ARIS architecture and reference models for business process management. In: van der Aalst, W.M.P., Desel, J., Oberweis, A. (eds.) Business Process Management. LNCS, vol. 1806, pp. 376–389. Springer, Heidelberg (2000)
The Open Group: Open Group Standard. Archimate 2.1 Specificattion. Van Haren Publishing, Zaltbommel (2013)
Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626–643 (1996)
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)
Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. (CSUR) 24(3), 293–318 (1992)
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)
Beauvoir, P.: Archi, archimate modelling tool (2015). Accessed March 2015
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)
Szwed, P.: Verification of archimate behavioral elements by model checking. In: Saeed, K., Homenda, W. (eds.) Computer Information Systems and Industrial Management. Lecture Notes in Computer Science, vol. 9339, pp. 132–144. Springer International Publishing, Warsaw (2015)
Szwed, P.: Efficiency of formal verification of archimate business processes with nusmv model checker. In: Federated Conference on Computer Science and Information Systems (FedCSIS), pp. 1427–1436 (2015)
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)
Anderson, B., Hansen, J.V., Lowry, P., Summers, S.: Model checking for e-business control and assurance. IEEE Trans. Syst. Man, Cybern. C Appl. Rev. 35(3), 445–450 (2005)
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. IEEE (2006)
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)
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)
Wynn, M.T., Verbeek, H., van der Aalst, W.M., ter Hofstede, A.H., Edmond, D.: Business process verification-finally a reality!. Bus. Process Manag. J. 15(1), 74–92 (2009)
Van der Aalst, W.M., Ter Hofstede, A.H.: YAWL: Yet Another Workflow Language. Inf. Syst. 30(4), 245–275 (2005)
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, 8–11 September 2013, pp. 1103–1110 (2013)
Klimek, R., Szwed, P., Jedrusik, S.: Application of deductive reasoning to the verification of ArchiMate behavioral elements. Informatyka Ekonomiczna 29, 76–97 (2013)
Klimek, R.: A system for deduction-based formal verification of workflow-oriented software models. Appl. Math. Comput. Sci. 24(4), 941–956 (2014)
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 Syst. Des. 6(2), 217–232 (1995)
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)
Bertoli, P., Cimatti, A., Pistore, M., Roveri, M., Traverso, P.: MBP: a Model Based Planner. In: Proceedings of the IJCAI01 Workshop on Planning under Uncertainty and Incomplete Information (2001)
Clarke, E., Heinle, W.: Modular translation of statecharts to SMV. Technical report, Citeseer (2000)
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. CEUR Workshop Proceedings, vol. 1269, pp. 245–256. CEUR-WS.org, Berlin (2014)
Andersen, H.R.: An introduction to binary decision diagrams. Lecture notes, IT University of Copenhagen (1997)
Szwed, P., Ligeza, A.: Application of OBDD diagrams in verification of tabular rule systems. Schedae Informaticae 14 (2005)
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)
McCabe, T.: A complexity measure. IEEE Trans. SE Softw. Eng. 2(4), 308–320 (1976)
Rudell, R.: Dynamic variable ordering for ordered binary decision diagrams. In: Proceedings of the 1993 IEEE/ACM International Conference on Computer-Aided Design, pp. 42–47. IEEE Computer Society Press (1993)
Szwed, P.: Application of fuzzy ontological reasoning in an implementation of medical guidelines. In: 2013 The 6th International Conference on Human System Interaction (HSI), pp. 342–349, June 2013
Szwed, P., Skrzynski, P., Grodniewicz, P.: Risk assessment for SWOP telemonitoring system based on fuzzy cognitive maps. In: Dziech, A., Czyżewski, A. (eds.) MCSS 2013. CCIS, vol. 368, pp. 233–247. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Szwed, P. (2016). Evaluating Efficiency of ArchiMate Business Processes Verification with NuSMV. In: Ziemba, E. (eds) Information Technology for Management. Lecture Notes in Business Information Processing, vol 243. Springer, Cham. https://doi.org/10.1007/978-3-319-30528-8_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-30528-8_11
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-30527-1
Online ISBN: 978-3-319-30528-8
eBook Packages: Computer ScienceComputer Science (R0)