{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,17]],"date-time":"2026-08-17T15:01:14Z","timestamp":1786978874615,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031614323","type":"print"},{"value":"9783031614330","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-61433-0_21","type":"book-chapter","created":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T12:02:01Z","timestamp":1718193721000},"page":"432-444","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["CosyVerif: The Path to\u00a0Formalisms Cohabitation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8473-9555","authenticated-orcid":false,"given":"\u00c9tienne","family":"Andr\u00e9","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3019-4902","authenticated-orcid":false,"given":"Jaime","family":"Arias","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2417-3064","authenticated-orcid":false,"given":"Beno\u00eet","family":"Barbot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Francis","family":"Hulin-Hubard","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5626-828X","authenticated-orcid":false,"given":"Fabrice","family":"Kordon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Van-Fran\u00e7ois","family":"Le","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3154-5268","authenticated-orcid":false,"given":"Laure","family":"Petrucci","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,6,13]]},"reference":[{"key":"21_CR1","unstructured":"CPN Tools: a tool for editing, simulating, and analyzing colored Petri nets. https:\/\/cpntools.org"},{"key":"21_CR2","unstructured":"GreatSPN. http:\/\/www.di.unito.it\/~greatspn\/index.html"},{"key":"21_CR3","unstructured":"Repository of FML files. https:\/\/depot.lipn.univ-paris13.fr\/cosyverif\/formalisms"},{"key":"21_CR4","unstructured":"UPPAAL. https:\/\/uppaal.org"},{"key":"21_CR5","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC, pp. 592\u2013601. ACM (1993)","DOI":"10.1145\/167088.167242"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/978-3-030-81685-8_26","volume-title":"Computer Aided Verification","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9, \u00c9.: IMITATOR 3: synthesis of timing parameters beyond decidability. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 552\u2013565. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_26"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-41202-8_14","volume-title":"Formal Methods and Software Engineering","author":"\u00c9 Andr\u00e9","year":"2013","unstructured":"Andr\u00e9, \u00c9., et al.: A modular approach for reusing formalisms in verification tools of concurrent systems. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 199\u2013214. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41202-8_14"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-030-79379-1_3","volume-title":"Tests and Proofs","author":"\u00c9 Andr\u00e9","year":"2021","unstructured":"Andr\u00e9, \u00c9., Marinho, D., van de Pol, J.: A benchmarks library for extended parametric timed automata. In: Loulergue, F., Wotawa, F. (eds.) TAP 2021. LNCS, vol. 12740, pp. 39\u201350. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79379-1_3"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-63406-3_1","volume-title":"Formal Methods and Software Engineering","author":"J Arias","year":"2020","unstructured":"Arias, J., Budde, C.E., Penczek, W., Petrucci, L., Sidoruk, T., Stoelinga, M.: Hackers vs. security: attack-defence trees as asynchronous multi-agent systems. In: Lin, S.-W., Hou, Z., Mahony, B. (eds.) ICFEM 2020. LNCS, vol. 12531, pp. 3\u201319. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-63406-3_1"},{"key":"21_CR10","unstructured":"Arias, J., Penczek, W., Petrucci, L., Sidoruk, T.: ADT2AMAS: managing agents in attack-defence scenarios. In: AAMAS, pp. 1749\u20131751. ACM (2021)"},{"issue":"4","key":"21_CR11","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1145\/3543146.3543161","volume":"49","author":"P Ballarini","year":"2022","unstructured":"Ballarini, P., Barbot, B.: Cosmos: evolution of a statistical model checking platform. SIGMETRICS Perform. Eval. Rev. 49(4), 65\u201369 (2022)","journal-title":"SIGMETRICS Perform. Eval. Rev."},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.peva.2015.04.003","volume":"90","author":"P Ballarini","year":"2015","unstructured":"Ballarini, P., Barbot, B., Duflot, M., Haddad, S., Pekergin, N.: HASL: a new approach for performance evaluation and model checking from concepts to experimentation. Perform. Eval. 90, 53\u201377 (2015)","journal-title":"Perform. Eval."},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Ballarini, P., Djafri, H., Duflot, M., Haddad, S., Pekergin, N.: COSMOS: a statistical model checker for the hybrid automata stochastic logic. In: QEST, pp. 143\u2013144. IEEE Computer Society (2011)","DOI":"10.1109\/QEST.2011.24"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Cooperative verification: towards reliable safety-critical systems (invited talk). In: FTSCS, pp.\u00a01\u20132. ACM (2022)","DOI":"10.1145\/3563822.3572548"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"561","DOI":"10.1007\/978-3-030-99524-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Beyer","year":"2022","unstructured":"Beyer, D., Kanav, S.: CoVeriTeam: on-demand composition of cooperative verification systems. In: TACAS 2022. LNCS, vol. 13243, pp. 561\u2013579. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_31"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-030-99429-7_3","volume-title":"Fundamental Approaches to Software Engineering","author":"D Beyer","year":"2022","unstructured":"Beyer, D., Kanav, S., Richter, C.: Construction of verifier combinations based on off-the-shelf verifiers. In: FASE 2022. LNCS, vol. 13241, pp. 49\u201370. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99429-7_3"},{"key":"21_CR17","first-page":"9","volume":"76","author":"L Hillah","year":"2009","unstructured":"Hillah, L., Kindler, E., Kordon, F., Petrucci, L., Treves, N.T.: A primer on the Petri net markup language and ISO\/IEC 15909\u20132. Petri Net Newsl. 76, 9\u201328 (2009). (Originally Presented at the 10th International Workshop on Practical Use of Coloured Petri Nets and the CPN Tools \u2013 CPN 2009)","journal-title":"Petri Net Newsl."},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/11888116_23","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2006","author":"L Hillah","year":"2006","unstructured":"Hillah, L., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: PN standardisation: a survey. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 307\u2013322. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11888116_23"},{"key":"21_CR19","first-page":"46","volume":"6","author":"L Hillah","year":"2012","unstructured":"Hillah, L., Kordon, F., Lakos, C., Petrucci, L.: Extending PNML scope: a framework to combine Petri nets types. Trans. Petri Nets Other Model. Concurr. 6, 46\u201370 (2012)","journal-title":"Trans. Petri Nets Other Model. Concurr."},{"key":"21_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-642-13675-7_20","volume-title":"Applications and Theory of Petri Nets","author":"LM Hillah","year":"2010","unstructured":"Hillah, L.M., Kordon, F., Petrucci, L., Tr\u00e8ves, N.: PNML framework: an extendable reference implementation of the petri net markup language. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 318\u2013327. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13675-7_20"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-319-91268-4_17","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"E Kindler","year":"2018","unstructured":"Kindler, E.: ePNK applications and annotations: a simulator for YAWL nets. In: Khomenko, V., Roux, O.H. (eds.) PETRI NETS 2018. LNCS, vol. 10877, pp. 339\u2013350. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91268-4_17"},{"issue":"6","key":"21_CR22","doi-asserted-by":"publisher","first-page":"931","DOI":"10.1007\/s10009-021-00615-1","volume":"23","author":"F Kordon","year":"2021","unstructured":"Kordon, F., Hillah, L., Hulin-Hubard, F., Jezequel, L., Paviot-Adet, E.: Study of the efficiency of model checking techniques using results of the MCC from 2015 to 2019. Int. J. Softw. Tools Technol. Transf. 23(6), 931\u2013952 (2021)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/978-3-319-91908-9_20","volume-title":"Computing and Software Science","author":"F Kordon","year":"2019","unstructured":"Kordon, F., Leuschel, M., van de Pol, J., Thierry-Mieg, Y.: Software architecture of modern model checkers. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 393\u2013419. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_20"},{"issue":"1","key":"21_CR24","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/logcom\/exs029","volume":"24","author":"B Kordy","year":"2014","unstructured":"Kordy, B., Mauw, S., Radomirovic, S., Schweitzer, P.: Attack-defense trees. J. Log. Comput. 24(1), 55\u201387 (2014)","journal-title":"J. Log. Comput."},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-00768-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Lime","year":"2009","unstructured":"Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for petri nets with stopwatches. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 54\u201357. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_6"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-031-06653-5_7","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"F Pereira","year":"2022","unstructured":"Pereira, F., Moutinho, F., Costa, A., Barros, J., Campos-Rebelo, R., Gomes, L.: IOPT-tools - from executable models to automatic code generation for embedded controllers development. In: Bernardinello, L., Petrucci, L. (eds.) PETRI NETS 2022. LNCS, vol. 13288, pp. 127\u2013138. Springer, Cham (2022)"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-662-46681-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Thierry-Mieg","year":"2015","unstructured":"Thierry-Mieg, Y.: Symbolic model-checking using ITS-tools. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 231\u2013237. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_20"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets and Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-61433-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,12]],"date-time":"2024-06-12T12:05:15Z","timestamp":1718193915000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-61433-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031614323","9783031614330"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-61433-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"13 June 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"PETRI NETS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Applications and Theory of Petri Nets and Concurrency","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Geneva","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Switzerland","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":"26 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"45","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"apn2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.unige.ch\/petrinets2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}