{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T04:18:46Z","timestamp":1745122726032,"version":"3.40.4"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031853555","type":"print"},{"value":"9783031853562","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-85356-2_3","type":"book-chapter","created":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T20:08:54Z","timestamp":1745093334000},"page":"32-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of\u00a0Declarative Specifications of\u00a0BPs: DCR2CPN-Based Approach"],"prefix":"10.1007","author":[{"given":"Ikram","family":"Garfatta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ka\u00efs","family":"Klai","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Walid","family":"Gaaloul","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,4,17]]},"reference":[{"issue":"1","key":"3_CR1","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1142\/S0218126698000043","volume":"8","author":"WMP van der Aalst","year":"1998","unstructured":"van der Aalst, W.M.P.: The application of petri nets to workflow management. J. Circ. Syst. Comput. 8(1), 21\u201366 (1998)","journal-title":"J. Circ. Syst. Comput."},{"issue":"4","key":"3_CR2","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1016\/j.is.2004.02.002","volume":"30","author":"WMP van der Aalst","year":"2005","unstructured":"van der Aalst, W.M.P., ter Hofstede, A.H.M.: YAWL: yet another workflow language. Inf. Syst. 30(4), 245\u2013275 (2005)","journal-title":"Inf. Syst."},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"van\u00a0der Aalst, W.M.P., Pesic, M.: Decserflow: towards a truly declarative service flow language. In: Web Services and Formal Methods, Third International Workshop, WS-FM 2006 Vienna, Austria, 8\u20139 September 2006. LNCS, vol.\u00a04184, pp. 1\u201323. Springer (2006)","DOI":"10.1007\/11841197_1"},{"issue":"2","key":"3_CR4","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/s00450-009-0057-9","volume":"23","author":"WMP van der Aalst","year":"2009","unstructured":"van der Aalst, W.M.P., Pesic, M., Schonenberg, H.: Declarative workflows: balancing between flexibility and support. Comput. Sci. Res. Dev. 23(2), 99\u2013113 (2009)","journal-title":"Comput. Sci. Res. Dev."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Boubaker, S., Klai, K., Kortas, H., Gaaloul, W.: A formal model for business process configuration verification supporting OR-join semantics. In: On the Move to Meaningful Internet Systems, OTM. LNCS, vol. 11229, pp. 623\u2013642 (2018)","DOI":"10.1007\/978-3-030-02610-3_35"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Bryans, J.W., Wei, W.: Formal analysis of BPMN models using event-B. In: Formal Methods for Industrial Critical Systems - 15th International Workshop, FMICS. LNCS, vol.\u00a06371, pp. 33\u201349. Springer (2010)","DOI":"10.1007\/978-3-642-15898-8_3"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Cosma, V.P., Hildebrandt, T.T., Slaats, T.: Transforming dynamic condition response graphs to safe petri nets. In: Application and Theory of Petri Nets and Concurrency - 44th International Conference, PETRI NETS 2023, Lisbon, Portugal, 25\u201330 June 2023. LNCS, vol. 13929, pp. 417\u2013439. Springer (2023)","DOI":"10.1007\/978-3-031-33620-1_22"},{"issue":"12","key":"3_CR8","doi-asserted-by":"publisher","first-page":"1281","DOI":"10.1016\/j.infsof.2008.02.006","volume":"50","author":"RM Dijkman","year":"2008","unstructured":"Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281\u20131294 (2008)","journal-title":"Inf. Softw. Technol."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Evangelista, S.: High level petri nets analysis with Helena. In: Applications and Theory of Petri Nets 2005, pp. 455\u2013464. Berlin, Heidelberg (2005)","DOI":"10.1007\/11494744_26"},{"issue":"1","key":"3_CR10","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/TSC.2010.1","volume":"3","author":"W Gaaloul","year":"2010","unstructured":"Gaaloul, W., Bhiri, S., Rouached, M.: Event-based design and runtime verification of composite service transactional behavior. IEEE Trans. Serv. Comput. 3(1), 32\u201345 (2010)","journal-title":"IEEE Trans. Serv. Comput."},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Goedertier, S., Vanthienen, J.: Declarative process modeling with business vocabulary and business rules. In: On the Move to Meaningful Internet Systems 2007: OTM 2007 Workshops, Part I, vol.\u00a04805, pp. 603\u2013612. Springer (2007)","DOI":"10.1007\/978-3-540-76888-3_83"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Hildebrandt, T.T., Mukkamala, R.R.: Declarative event-based workflow as distributed dynamic condition response graphs. In: Proceedings Third Workshop on Programming Language Approaches to Concurrency and communication-cEntric Software. EPTCS, vol.\u00a069, pp. 59\u201373 (2010)","DOI":"10.4204\/EPTCS.69.5"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Hildebrandt, T.T., Slaats, T., L\u00f3pez, H.A., Debois, S., Carbone, M.: Declarative choreographies and liveness. In: Formal Techniques for Distributed Objects, Components, and Systems FORTE 2019. LNCS, vol. 11535, pp. 129\u2013147. Springer (2019)","DOI":"10.1007\/978-3-030-21759-4_8"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"101765","DOI":"10.1016\/j.is.2021.101765","volume":"104","author":"S Houhou","year":"2022","unstructured":"Houhou, S., Baarir, S., Poizat, P., Qu\u00e9innec, P., Kahloul, L.: A first-order logic verification framework for communication-parametric and time-aware BPMN collaborations. Inf. Syst. 104, 101765 (2022)","journal-title":"Inf. Syst."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Jensen, K., Kristensen, L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems, 1st edn. Springer (2009)","DOI":"10.1007\/b95112_1"},{"key":"3_CR16","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/j.ins.2016.12.044","volume":"385","author":"A Kheldoun","year":"2017","unstructured":"Kheldoun, A., Barkaoui, K., Ioualalen, M.: Formal verification of complex business processes based on high-level petri nets. Inf. Sci. 385, 39\u201354 (2017)","journal-title":"Inf. Sci."},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Morimoto, S.: A survey of formal verification for business process modeling. In: Computational Science - ICCS 2008, 8th International Conference. LNCS, vol.\u00a05102, pp. 514\u2013522. Springer (2008)","DOI":"10.1007\/978-3-540-69387-1_58"},{"key":"3_CR18","unstructured":"Mukkamala, R.R.: A formal model for declarative workflows dynamic condition response graphs. Ph.D. thesis (2012)"},{"issue":"4","key":"3_CR19","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1109\/5.24143","volume":"77","author":"T Murata","year":"1989","unstructured":"Murata, T.: Petri nets: properties, analysis and applications. Proc. IEEE 77(4), 541\u2013580 (1989)","journal-title":"Proc. IEEE"},{"key":"3_CR20","unstructured":"OMG: Business process model and notation (BPMN) 2.0 (2014). https:\/\/www.omg.org\/spec\/BPMN\/"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"3763","DOI":"10.1080\/00207540701199677","volume":"46","author":"C Ou-Yang","year":"2008","unstructured":"Ou-Yang, C., Lin, Y.D.: BPMN-based business process model feasibility analysis: a petri net approach. Int. J. Prod. Res. 46, 3763\u20133781 (2008)","journal-title":"Int. J. Prod. Res."},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Pesic, M., van\u00a0der Aalst, W.M.P.: A declarative approach for flexible business processes management. In: BPM 2006 International Workshops, BPD, BPI, ENEI, GPWW, DPM, semantics4ws. LNCS, vol.\u00a04103, pp. 169\u2013180. Springer (2006)","DOI":"10.1007\/11837862_18"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Pesic, M., Schonenberg, H., van\u00a0der Aalst, W.M.P.: DECLARE: full support for loosely-structured processes. In: 11th IEEE International Enterprise Distributed Object Computing Conference, pp. 287\u2013300. IEEE Computer Society (2007)","DOI":"10.1109\/EDOC.2007.14"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Pichler, P., Weber, B., Zugal, S., Pinggera, J., Mendling, J., Reijers, H.A.: Imperative versus declarative process modeling languages: an empirical investigation. In: Business Process Management Workshops - BPM 2011 International Workshops, Clermont-Ferrand, France, 29 August 2011, vol.\u00a099, pp. 383\u2013394 (2011)","DOI":"10.1007\/978-3-642-28108-2_37"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symposium on Foundations of Computer Science, Providence, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Puhlmann, F., Weske, M.: Using the pi-calculus for formalizing workflow patterns. In: Business Process Management, 3rd International Conference, BPM 2005, Nancy, France, 5\u20138 September 2005, vol.\u00a03649, pp. 153\u2013168 (2005)","DOI":"10.1007\/11538394_11"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Russo, V., Ciampi, M., Esposito, M.: A business process model for integrated home care. In: The 6th International Conference on Emerging Ubiquitous Systems and Pervasive Networks. Procedia Computer Science, vol.\u00a063, pp. 300\u2013307 (2015)","DOI":"10.1016\/j.procs.2015.08.347"},{"key":"3_CR28","unstructured":"Sch\u00f6nig, S., Jablonski, S.: Comparing declarative process modelling languages from the organisational perspective. In: Business Process Management Workshops - BPM 2015, 13th International Workshops, Innsbruck, Austria, 31 August\u20133 September 2015, Revised Papers. LNBIP, vol.\u00a0256, pp. 17\u201329. Springer (2015)"},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"Verbeek, E., van\u00a0der Aalst, W.M.P.: Woflan 2.0: a petri-net-based workflow diagnosis tool. In: Application and Theory of Petri Nets 2000, ICATPN 2000. LNCS, vol.\u00a01825, pp. 475\u2013484. Springer (2000)","DOI":"10.1007\/3-540-44988-4_28"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"Ye, J., Sun, S., Song, W., Wen, L.: Formal semantics of BPMN process models using yawl. In: 2008 Second International Symposium on Intelligent Information Technology Application, vol.\u00a02, pp. 70\u201374 (2008)","DOI":"10.1109\/IITA.2008.68"}],"container-title":["Lecture Notes in Computer Science","Verification and Evaluation of Computer and Communication Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-85356-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T20:09:02Z","timestamp":1745093342000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-85356-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031853555","9783031853562"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-85356-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"17 April 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VECoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification and Evaluation of Computer and Communication Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Djerba","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tunisia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 October 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 October 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vecos2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.vecos-world.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}