{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:40:03Z","timestamp":1748619603525,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243689"},{"type":"electronic","value":"9783319243696"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24369-6_11","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T22:46:37Z","timestamp":1441925197000},"page":"132-144","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Verification of ArchiMate Behavioral Elements by Model Checking"],"prefix":"10.1007","author":[{"given":"Piotr","family":"Szwed","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,30]]},"reference":[{"issue":"3","key":"11_CR1","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 Transactions on Systems, Man, and Cybernetics, Part C: Applications and Reviews 35(3), 445\u2013450 (2005)","journal-title":"IEEE Transactions on Systems, Man, and Cybernetics, Part C: Applications and Reviews"},{"key":"11_CR2","unstructured":"Beauvoir, P.: Archi, archimate modelling tool (2015). http:\/\/www.archimatetool.com\/ (accessed March 2015)"},{"key":"11_CR3","unstructured":"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)"},{"issue":"3","key":"11_CR4","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 Computing Surveys (CSUR) 24(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"11_CR5","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_CR6","unstructured":"Clarke, E., Heinle, W.: Modular translation of statecharts to smv. Tech. rep., Citeseer (2000)"},{"issue":"2","key":"11_CR7","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 in System Design 6(2), 217\u2013232 (1995)","journal-title":"Formal Methods in System Design"},{"key":"11_CR8","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":"4","key":"11_CR9","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 Computing Surveys (CSUR) 28(4), 626\u2013643 (1996)","journal-title":"ACM Computing Surveys (CSUR)"},{"key":"11_CR10","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"},{"key":"11_CR11","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_CR12","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_CR13","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_CR14","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, September 8\u201311, 2013, pp. 1103\u20131110 (2013). http:\/\/fedcsis.org\/2013\/"},{"key":"11_CR15","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"},{"key":"11_CR16","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-pp. IEEE (2006)"},{"key":"11_CR17","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_CR18","unstructured":"OMG: Business Process Model and Notation (BPMN) version 2.0. Tech. rep., OMG, January 2011. http:\/\/www.omg.org\/spec\/BPMN\/2.0"},{"key":"11_CR19","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education (2004)"},{"key":"11_CR20","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, Chemnitz, Germany, September 29 - October 1, 2014. CEUR Workshop Proceedings, vol. 1269, pp. 245\u2013256. CEUR-WS.org (2014). http:\/\/ceur-ws.org\/Vol-1269\/paper245.pdf"},{"issue":"1","key":"11_CR21","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"},{"key":"11_CR22","unstructured":"The Open Group: Open Group Standard. Archimate 2.1 Specificattion. Van Haren Publishing, Zaltbommel (2013)"},{"key":"11_CR23","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"}],"container-title":["Lecture Notes in Computer Science","Computer Information Systems and Industrial Management"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24369-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T15:09:07Z","timestamp":1748617747000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24369-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243689","9783319243696"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24369-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"30 October 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}