{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,4]],"date-time":"2025-12-04T18:44:29Z","timestamp":1764873869958,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030780883"},{"type":"electronic","value":"9783030780890"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"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":[[2021]]},"DOI":"10.1007\/978-3-030-78089-0_3","type":"book-chapter","created":{"date-parts":[[2021,6,9]],"date-time":"2021-06-09T14:26:35Z","timestamp":1623248795000},"page":"42-59","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["A Formalisation of SysML State Machines in mCRL2"],"prefix":"10.1007","author":[{"given":"Mark","family":"Bouwman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bas","family":"Luttik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Djurre","family":"van der Wal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,8]]},"reference":[{"issue":"4","key":"3_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/s10009-012-0243-0","volume":"15","author":"I Abdelhalim","year":"2013","unstructured":"Abdelhalim, I., Schneider, S., Treharne, H.: An integrated framework for checking the behaviour of fUML models using CSP. Int. J. Softw. Tools Technol. Transf. 15(4), 375\u2013396 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0243-0","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"3_CR2","unstructured":"Belinfante, A.: JTorX: Exploring Model-Based Testing. Ph.D. thesis, University of Twente, Enschede, Netherlands (2014). http:\/\/purl.utwente.nl\/publications\/91781"},{"key":"3_CR3","unstructured":"Bouwman, M.: mCRL2 model capturing the generic semantics of EULYNX SysML. https:\/\/github.com\/markuzzz\/SysML-to-mCRL2"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Bouwman, M., van der Wal, D., Luttik, B., Stoelinga, M., Rensink, A.: What is the point: formal analysis and test generation or a railway standard. In: Baraldi, P., Di Maio, F., Zio, E. (eds.) Proceedings of ESREL2020-PSAM15, pp. 921\u2013928. Research Publishing, Singapore (2020). https:\/\/doi.org\/10.3850\/978-981-14-8593-0_4410-cd","DOI":"10.3850\/978-981-14-8593-0_4410-cd"},{"key":"3_CR5","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 (TACAS 2019)","author":"O Bunte","year":"2019","unstructured":"Bunte, O., et al.: The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019). Lecture Notes in Computer Science, vol. 11428, pp. 21\u201339. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17465-1_2"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press (2014)","DOI":"10.7551\/mitpress\/9946.001.0001"},{"issue":"1\u20132","key":"3_CR7","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. ISSE 6(1\u20132), 83\u201390 (2010). https:\/\/doi.org\/10.1007\/s11334-009-0116-1","journal-title":"ISSE"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-25271-6_12","volume-title":"Formal Methods for Components and Objects","author":"HH Hansen","year":"2010","unstructured":"Hansen, H.H., Ketema, J., Luttik, B., Mousavi, M.R., van de Pol, J., dos Santos, O.M.: Automated verification of executable UML models. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. Lecture Notes in Computer Science, vol. 6957, pp. 225\u2013250. Springer, Cham (2010). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_12"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/3-540-45648-1_26","volume-title":"ZB 2002: Formal Specification and Development in Z and B. ZB 2002","author":"S Kim","year":"2002","unstructured":"Kim, S., Carrington, D.A.: A formal model of the UML metamodel: the UML state machine and its integrity constraints. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002: Formal Specification and Development in Z and B. ZB 2002. Lecture Notes in Computer Science, vol. 2272, pp. 497\u2013516. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_26"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1007\/3-540-45441-1_19","volume-title":"UML 2001\u2014The Unified Modeling Language. Modeling Languages, Concepts, and Tools","author":"S Kuske","year":"2001","unstructured":"Kuske, S.: A Formal Semantics of UML State Machines Based on Structured Graph Transformation. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 241\u2013256. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45441-1_19"},{"issue":"6","key":"3_CR11","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1007\/s001659970003","volume":"11","author":"D Latella","year":"1999","unstructured":"Latella, D., Majzik, I., Massink, M.: Automatic verification of a behavioural subset of UML statechart diagrams using the SPIN model-checker. Formal Asp. Comput. 11(6), 637\u2013664 (1999). https:\/\/doi.org\/10.1007\/s001659970003","journal-title":"Formal Asp. Comput."},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Lilius, J., Paltor, I.: vUML: a tool for verifying UML models. In: The 14th IEEE International Conference on Automated Software Engineering, ASE 1999, Cocoa Beach, Florida, USA, 12\u201315 October 1999, pp. 255\u2013258. IEEE Computer Society (1999). https:\/\/doi.org\/10.1109\/ASE.1999.802301","DOI":"10.1109\/ASE.1999.802301"},{"key":"3_CR13","unstructured":"Lilius, J., Paltor, I.P.: The semantics of UML state machines (1999)"},{"key":"3_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., Liu, Y., Andr\u00e9, \u00c9., Choppy, C., Sun, J., Wadhwa, B., Dong, J.S.: 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":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-030-02146-7_11","volume-title":"Formal Aspects of Component Software","author":"T Neele","year":"2018","unstructured":"Neele, T., Willemse, T.A.C., Groote, J.F.: Solving parameterised boolean equation systems with infinite data through quotienting. In: Bae, K., \u00d6lveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 216\u2013236. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02146-7_11"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Object Managament Group: OMG Unified Modeling Language, version 2.5.1 (2017). https:\/\/www.omg.org\/spec\/UML\/","DOI":"10.1016\/B978-1-78548-171-0.50001-3"},{"key":"3_CR17","unstructured":"Object Managament Group: Precise Semantics of UML State Machines (PSSM), version 1.0 (2019). https:\/\/www.omg.org\/spec\/PSSM\/"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/3-540-46852-8_31","volume-title":"UML\u201999\u2014The Unified Modeling Language","author":"J Lilius","year":"1999","unstructured":"Lilius, J., Paltor, I.P.: Formalising UML state machines for model checking. In: France, R., Rumpe, B. (eds.) UML 1999. LNCS, vol. 1723, pp. 430\u2013444. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-46852-8_31"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Pedroza, G., Apvrille, L., Knorreck, D.: AVATAR: A SysML environment for the formal verification of safety and security properties. In: 11th Annual International Conference on New Technologies of Distributed Systems, NOTERE 2011, Paris, France, 9\u201313 May 2011, pp. 1\u201310. IEEE (2011). https:\/\/doi.org\/10.1109\/NOTERE.2011.5957992","DOI":"10.1109\/NOTERE.2011.5957992"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Remenska, D., et al.: From UML to process algebra and back: an automated approach to model-checking software design artifacts of concurrent systems. In: Brat, G., Rungta, N., Venet, A. (eds.) NASA Formal Methods. NFM 2013. LNCS, vol. 7871, pp. 244\u2013260. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38088-4_17","DOI":"10.1007\/978-3-642-38088-4_17"},{"issue":"3","key":"3_CR21","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. Electron. Notes Theor. Comput. Sci. 55(3), 357\u2013369 (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00262-2","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"3_CR22","unstructured":"van der Wal, D., Bouwman, M., Stoelinga, M., Rensink, A.: On capturing the EULYNX railway standard with an internal DSL in Java. In: preparation for submission (2021)"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"16561","DOI":"10.1109\/ACCESS.2019.2892745","volume":"7","author":"H Wang","year":"2019","unstructured":"Wang, H., Zhong, D., Zhao, T., Ren, F.: Integrating model checking with SysML in complex system safety analysis. IEEE Access 7, 16561\u201316571 (2019). https:\/\/doi.org\/10.1109\/ACCESS.2019.2892745","journal-title":"IEEE Access"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Objects, Components, and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-78089-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,8]],"date-time":"2025-06-08T22:04:33Z","timestamp":1749420273000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-78089-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030780883","9783030780890"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-78089-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"8 June 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FORTE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Techniques for Distributed Objects, Components, and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 June 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18 June 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"41","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"forte2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2021\/forte","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":"26","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":"9","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":"4","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":"35% - 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","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)"}},{"value":"Due to the Corona pandemic this event was held virtually.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}