{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:46:28Z","timestamp":1764873988975,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031150074"},{"type":"electronic","value":"9783031150081"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-15008-1_7","type":"book-chapter","created":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:02:47Z","timestamp":1662332567000},"page":"86-102","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formal Verification of\u00a0an\u00a0Industrial UML-like Model using mCRL2"],"prefix":"10.1007","author":[{"given":"Anna","family":"Stramaglia","sequence":"first","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5772-9527","authenticated-orcid":false,"given":"Jeroen J. A.","family":"Keiren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocab":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,9,5]]},"reference":[{"key":"7_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-030-78089-0_3","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"M Bouwman","year":"2021","unstructured":"Bouwman, M., Luttik, B., van der Wal, D.: A formalisation of SysML state machines in mCRL2. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 42\u201359. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_3"},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-030-58298-2_10","volume-title":"Formal Methods for Industrial Critical Systems","author":"O Bunte","year":"2020","unstructured":"Bunte, O., Gool, L.C.M., Willemse, T.A.C.: Formal verification of OIL component specifications using mCRL2. In: ter Beek, M.H., Ni\u010dkovi\u0107, D. (eds.) FMICS 2020. LNCS, vol. 12327, pp. 231\u2013251. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_10"},{"issue":"2","key":"7_CR4","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992). https:\/\/doi.org\/10.1016\/0890-5401(92)90017-A","journal-title":"Inf. Comput."},{"key":"7_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., et al.: 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). https:\/\/doi.org\/10.1007\/3-540-45657-0_29"},{"key":"7_CR6","doi-asserted-by":"publisher","unstructured":"Dubrovin, J., Junttila, T.: Symbolic model checking of hierarchical UML state machines. In: 2008 8th International Conference on Application of Concurrency to System Design, pp. 108\u2013117. ISSN: 1550\u20134808 (2008). https:\/\/doi.org\/10.1109\/ACSD.2008.4574602","DOI":"10.1109\/ACSD.2008.4574602"},{"issue":"12","key":"7_CR7","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/636517.636531","volume":"37","author":"JF Groote","year":"2002","unstructured":"Groote, J.F., Lisser, B.: Computer assisted manipulation of algebraic process specifications. ACM SIGPLAN Notices 37(12), 98\u2013107 (2002). https:\/\/doi.org\/10.1145\/636517.636531","journal-title":"ACM SIGPLAN Notices"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-49253-4_8","volume-title":"Algebraic Methodology and Software Technology","author":"JF Groote","year":"1998","unstructured":"Groote, J.F., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: Haeberer, A.M. (ed.) AMAST 1999. LNCS, vol. 1548, pp. 74\u201390. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49253-4_8"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014). https:\/\/mitpress.mit.edu\/books\/modeling-and-analysis-communicating-systems","DOI":"10.7551\/mitpress\/9946.001.0001"},{"issue":"1\u20132","key":"7_CR10","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s11334-009-0116-1","volume":"6","author":"HH Hansen","year":"2010","unstructured":"Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J.: Towards model checking executable UML specifications in mCRL2. Innov. Syst. Softw. Eng. 6(1\u20132), 83\u201390 (2010). https:\/\/doi.org\/10.1007\/s11334-009-0116-1","journal-title":"Innov. Syst. Softw. Eng."},{"issue":"12","key":"7_CR11","doi-asserted-by":"publisher","first-page":"2435","DOI":"10.1016\/j.scico.2012.11.009","volume":"78","author":"YL Hwong","year":"2013","unstructured":"Hwong, Y.L., Keiren, J.J.A., Kusters, V.J.J., Leemans, S., Willemse, T.A.C.: Formalising and analysing the control software of the compact muon solenoid experiment at the large hadron collider. Sci. Comput. Program. 78(12), 2435\u20132452 (2013). https:\/\/doi.org\/10.1016\/j.scico.2012.11.009","journal-title":"Sci. Comput. Program."},{"key":"7_CR12","doi-asserted-by":"publisher","unstructured":"John, K.H., Tiegelkamp, M.: The programming languages of IEC 61131\u20133. In: John, K.H., Tiegelkamp, M. (eds.) IEC 61131\u20133: Programming Industrial Automation Systems: Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids, pp. 99\u2013205. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12015-2_4","DOI":"10.1007\/978-3-642-12015-2_4"},{"key":"7_CR13","doi-asserted-by":"publisher","unstructured":"Keiren, J.J.A., Klabbers, M.D.: Modelling and verifying IEEE Std. 11073\u201320601 session setup using mCRL2. Electron. Commun. EASST 53 (2013). https:\/\/doi.org\/10.14279\/tuj.eceasst.53.793","DOI":"10.14279\/tuj.eceasst.53.793"},{"key":"7_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-38613-8_23","volume-title":"Integrated Formal Methods","author":"S Liu","year":"2013","unstructured":"Liu, S., et al.: A formal semantics for complete UML state machines with communications. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 331\u2013346. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38613-8_23"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-030-31277-0_5","volume-title":"Networked Systems","author":"A Lyazidi","year":"2019","unstructured":"Lyazidi, A., Mouline, S.: Formal verification of UML state machine diagrams using petri nets. In: Atig, M.F., Schwarzmann, A.A. (eds.) NETYS 2019. LNCS, vol. 11704, pp. 67\u201374. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31277-0_5"},{"key":"7_CR16","unstructured":"Object Management Group: OMG Unified Modelling Language (UML). Technical report Version 2.5.1 (2017). https:\/\/www.omg.org\/spec\/UML\/2.5.1\/PDF"},{"key":"7_CR17","doi-asserted-by":"publisher","unstructured":"Pore, A., et al.: Safe reinforcement learning using formal verification for tissue retraction in autonomous robotic-assisted surgery. In: 2021 IEEE\/RSJ IROS, pp. 4025\u20134031 (2021). https:\/\/doi.org\/10.1109\/IROS51168.2021.9636175. ISSN: 2153-0866","DOI":"10.1109\/IROS51168.2021.9636175"},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-319-68034-7_7","volume-title":"Formal Aspects of Component Software","author":"S de Putter","year":"2017","unstructured":"de Putter, S., Wijs, A.: Compositional model checking is lively. In: Proen\u00e7a, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 117\u2013136. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-68034-7_7"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-319-10431-7_22","volume-title":"Software Engineering and Formal Methods","author":"RJ Rodr\u00edguez","year":"2014","unstructured":"Rodr\u00edguez, R.J., Fredlund, L.\u00c5., Herranz, \u00c1., Mari\u00f1o, J.: Execution and verification of UML state machines with erlang. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 284\u2013289. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_22"},{"key":"7_CR20","doi-asserted-by":"publisher","unstructured":"Sahay, A., Indamutsa, A., Ruscio, D.D., Pierantonio, A.: Supporting the understanding and comparison of low-code development platforms. In: 2020 46th Euromicro Conference on SEAA, pp. 171\u2013178 (2020). https:\/\/doi.org\/10.1109\/SEAA51224.2020.00036","DOI":"10.1109\/SEAA51224.2020.00036"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-030-77543-8_14","volume-title":"Rigorous State-Based Methods","author":"S Salunkhe","year":"2021","unstructured":"Salunkhe, S., Berglehner, R., Rasheeq, A.: Automatic transformation of SysML model to event-B model for railway CCS application. In: Raschke, A., M\u00e9ry, D. (eds.) Rigorous State-Based Methods. LNCS, vol. 12709, pp. 143\u2013149. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_14"},{"issue":"5","key":"7_CR22","doi-asserted-by":"publisher","first-page":"688","DOI":"10.1007\/s11547-020-01314-8","volume":"126","author":"A Santone","year":"2021","unstructured":"Santone, A., et al.: Radiomic features for prostate cancer grade detection through formal verification. La radiologia medica 126(5), 688\u2013697 (2021). https:\/\/doi.org\/10.1007\/s11547-020-01314-8","journal-title":"La radiologia medica"},{"key":"7_CR23","doi-asserted-by":"publisher","unstructured":"Santos, L.B.R., J\u00fanior, V.A.S., Vijaykumar, N.L.: Transformation of UML behavioral diagrams to support software model checking. In: FESCA 2014. EPTCS, vol. 147, pp. 133\u2013142 (2014). https:\/\/doi.org\/10.4204\/EPTCS.147.10, arXiv: 1404.0855","DOI":"10.4204\/EPTCS.147.10"},{"issue":"3","key":"7_CR24","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1016\/S1571-0661(04)00262-2","volume":"55","author":"T Sch\u00e4fer","year":"2001","unstructured":"Sch\u00e4fer, T., Knapp, A., Merz, S.: Model checking UML state machines and collaborations. ENTCS 55(3), 357\u2013369 (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00262-2","journal-title":"ENTCS"},{"key":"7_CR25","unstructured":"Stramaglia, A., Keiren, J.J.A.: Formal verification of an industrial UML-like model using mCRL2 (extended version) (2022). arXiv: 2205.08146"},{"key":"7_CR26","unstructured":"Wesselink, W., Willemse, T.A.C.: Evidence extraction from parameterised Boolean equation systems. In: Benzm\u00fcller, C., Otten, J. (eds.) proceedings of ARQNL 2018 affiliated with IJCAR 2018, Oxford, UK, 18 July 2018. CEUR, vol. 2095, pp. 86\u2013100. CEUR-WS.org (2018). http:\/\/ceur-ws.org\/Vol-2095\/paper6.pdf"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15008-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:09:11Z","timestamp":1662332951000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15008-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150074","9783031150081"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15008-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"5 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmics2022.fsa.win.tue.nl\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"13","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"59% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}