{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T19:40:02Z","timestamp":1748806802316,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319305271"},{"type":"electronic","value":"9783319305288"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30528-8_11","type":"book-chapter","created":{"date-parts":[[2016,3,11]],"date-time":"2016-03-11T12:27:52Z","timestamp":1457699272000},"page":"179-196","source":"Crossref","is-referenced-by-count":0,"title":["Evaluating Efficiency of ArchiMate Business Processes Verification with NuSMV"],"prefix":"10.1007","author":[{"given":"Piotr","family":"Szwed","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-69387-1_58","volume-title":"Computational Science \u2013 ICCS 2008","author":"S Morimoto","year":"2008","unstructured":"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\u2013522. Springer, Heidelberg (2008)"},{"key":"11_CR2","unstructured":"OMG: Business Process Model and Notation (BPMN) version 2.0. Technical report, OMG, January 2011"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45594-9_24","volume-title":"Business Process Management","author":"A-W Scheer","year":"2000","unstructured":"Scheer, A.-W., N\u00fcttgens, 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\u2013389. Springer, Heidelberg (2000)"},{"key":"11_CR4","unstructured":"The Open Group: Open Group Standard. Archimate 2.1 Specificattion. Van Haren Publishing, Zaltbommel (2013)"},{"issue":"4","key":"11_CR5","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Comput. Surv. (CSUR) 28(4), 626\u2013643 (1996)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 1\u201330. Springer, Heidelberg (2012)"},{"issue":"3","key":"11_CR7","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"RE Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv. (CSUR) 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"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\u20134. Open Publishing Association (2012)","DOI":"10.4204\/EPTCS.105.0"},{"key":"11_CR9","unstructured":"Beauvoir, P.: Archi, archimate modelling tool (2015). Accessed March 2015"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"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\u2013364. Springer, Heidelberg (2002)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-24369-6_11","volume-title":"Computer Information Systems and Industrial Management","author":"P Szwed","year":"2015","unstructured":"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\u2013144. Springer International Publishing, Warsaw (2015)"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"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\u20131436 (2015)","DOI":"10.15439\/2015F44"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"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\u20131180. IEEE (2011)","DOI":"10.1109\/ICSMC.2011.6083857"},{"issue":"3","key":"11_CR14","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1109\/TSMCC.2004.843181","volume":"35","author":"B Anderson","year":"2005","unstructured":"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\u2013450 (2005)","journal-title":"IEEE Trans. Syst. Man, Cybern. C Appl. Rev."},{"key":"11_CR15","unstructured":"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)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-36189-8_15","volume-title":"Web Services, E-Business, and the Semantic Web","author":"X Fu","year":"2002","unstructured":"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\u2013202. Springer, Heidelberg (2002)"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013267. ACM (2009)","DOI":"10.1145\/1514894.1514924"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1108\/14637150910931479","volume":"15","author":"MT Wynn","year":"2009","unstructured":"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\u201392 (2009)","journal-title":"Bus. Process Manag. J."},{"issue":"4","key":"11_CR19","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/j.is.2004.02.002","volume":"30","author":"WM Aalst Van der","year":"2005","unstructured":"Van der Aalst, W.M., Ter Hofstede, A.H.: YAWL: Yet Another Workflow Language. Inf. Syst. 30(4), 245\u2013275 (2005)","journal-title":"Inf. Syst."},{"key":"11_CR20","unstructured":"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\u00f3w, Poland, 8\u201311 September 2013, pp. 1103\u20131110 (2013)"},{"key":"11_CR21","first-page":"76","volume":"29","author":"R Klimek","year":"2013","unstructured":"Klimek, R., Szwed, P., Jedrusik, S.: Application of deductive reasoning to the verification of ArchiMate behavioral elements. Informatyka Ekonomiczna 29, 76\u201397 (2013)","journal-title":"Informatyka Ekonomiczna"},{"issue":"4","key":"11_CR22","first-page":"941","volume":"24","author":"R Klimek","year":"2014","unstructured":"Klimek, R.: A system for deduction-based formal verification of workflow-oriented software models. Appl. Math. Comput. Sci. 24(4), 941\u2013956 (2014)","journal-title":"Appl. Math. Comput. Sci."},{"issue":"2","key":"11_CR23","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/BF01383968","volume":"6","author":"EM Clarke","year":"1995","unstructured":"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\u2013232 (1995)","journal-title":"Formal Methods Syst. Des."},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"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\u2013181. IEEE (2001)","DOI":"10.1109\/ISRE.2001.948557"},{"key":"11_CR25","unstructured":"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)"},{"key":"11_CR26","unstructured":"Clarke, E., Heinle, W.: Modular translation of statecharts to SMV. Technical report, Citeseer (2000)"},{"key":"11_CR27","series-title":"CEUR Workshop Proceedings","first-page":"245","volume-title":"Proceedings of the 23th International Workshop on Concurrency, Specification and Programming","author":"M Szpyrka","year":"2014","unstructured":"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\u2013256. CEUR-WS.org, Berlin (2014)"},{"key":"11_CR28","unstructured":"Andersen, H.R.: An introduction to binary decision diagrams. Lecture notes, IT University of Copenhagen (1997)"},{"key":"11_CR29","unstructured":"Szwed, P., Ligeza, A.: Application of OBDD diagrams in verification of tabular rule systems. Schedae Informaticae 14 (2005)"},{"issue":"1","key":"11_CR30","doi-asserted-by":"publisher","first-page":"127","DOI":"10.7494\/automat.2013.17.1.127","volume":"17","author":"P Szwed","year":"2013","unstructured":"Szwed, P., Chmiel, W., Jedrusik, S., Kadluczka, P.: Business processes in a distributed surveillance system integrated through workflow. Automatyka\/Automatics 17(1), 127\u2013139 (2013)","journal-title":"Automatyka\/Automatics"},{"issue":"4","key":"11_CR31","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1109\/TSE.1976.233837","volume":"2","author":"T McCabe","year":"1976","unstructured":"McCabe, T.: A complexity measure. IEEE Trans. SE Softw. Eng. 2(4), 308\u2013320 (1976)","journal-title":"IEEE Trans. SE Softw. Eng."},{"key":"11_CR32","unstructured":"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\u201347. IEEE Computer Society Press (1993)"},{"key":"11_CR33","doi-asserted-by":"crossref","unstructured":"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\u2013349, June 2013","DOI":"10.1109\/HSI.2013.6577845"},{"key":"11_CR34","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-38559-9_21","volume-title":"Multimedia Communications, Services and Security","author":"P Szwed","year":"2013","unstructured":"Szwed, P., Skrzynski, P., Grodniewicz, P.: Risk assessment for SWOP telemonitoring system based on fuzzy cognitive maps. In: Dziech, A., Czy\u017cewski, A. (eds.) MCSS 2013. CCIS, vol. 368, pp. 233\u2013247. Springer, Heidelberg (2013)"}],"container-title":["Lecture Notes in Business Information Processing","Information Technology for Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30528-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T19:05:10Z","timestamp":1748804710000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30528-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319305271","9783319305288"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30528-8_11","relation":{},"ISSN":["1865-1348","1865-1356"],"issn-type":[{"type":"print","value":"1865-1348"},{"type":"electronic","value":"1865-1356"}],"subject":[],"published":{"date-parts":[[2016]]}}}