{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T18:49:47Z","timestamp":1761677387728,"version":"build-2065373602"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T00:00:00Z","timestamp":1759276800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T00:00:00Z","timestamp":1761091200000},"content-version":"vor","delay-in-days":21,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2025,10]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>The proprietary State Machine Modelling Tool (SMMT), developed and maintained at Canon Production Printing, can be used to model software components using state machines and generate executable production code. We provide an operational semantics of the language supported by SMMT, derived from already existing code generators and discussions with engineers. By subsequently formalising this operational semantics in the mCRL2 language, we unlock the ability to apply formal verification to SMMT models during their design using the mCRL2 toolset. Using the mCRL2 formalisation, we have found various subtle bugs in the implementation of the SMMT tool, affecting its correctness, and proposed fixes for SMMT.<\/jats:p>","DOI":"10.1007\/s10009-025-00829-7","type":"journal-article","created":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T13:33:28Z","timestamp":1761140008000},"page":"511-532","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalising and analysing SMMT models using the mCRL2 toolset"],"prefix":"10.1007","volume":"27","author":[{"given":"J. E. P. M.","family":"van Laarhoven","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"O.","family":"Bunte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"L. C. M.","family":"van Gool","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T. A. C.","family":"Willemse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,22]]},"reference":[{"issue":"4","key":"829_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.A., 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":"829_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1007\/978-3-319-67113-0_14","volume-title":"FMICS-AVoCS","author":"R. van Beusekom","year":"2017","unstructured":"van Beusekom, R., Groote, J.F., Hoogendijk, P.F., Howe, R., Wesselink, W., Wieringa, R., Willemse, T.A.C.: Formalising the Dezyne modelling language in mCRL2. In: FMICS-AVoCS. Lecture Notes in Computer Science, vol.\u00a010471, pp.\u00a0217\u2013233. Springer, Berlin (2017)"},{"key":"829_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/11589976_12","volume-title":"IFM","author":"J. Bodeveix","year":"2005","unstructured":"Bodeveix, J., Filali, M., Lawall, J., Muller, G.: Formal methods meet domain specific languages. In: IFM. Lecture Notes in Computer Science, vol.\u00a03771, pp.\u00a0187\u2013206. Springer, Berlin (2005)"},{"key":"829_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1007\/978-3-030-78089-0_3","volume-title":"FORTE","author":"M. Bouwman","year":"2021","unstructured":"Bouwman, M., Luttik, B., van der Wal, D.: A formalisation of SysML state machines in mCRL2. In: FORTE. Lecture Notes in Computer Science, vol.\u00a012719, pp.\u00a042\u201359. Springer, Berlin (2021)"},{"key":"829_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/978-3-030-58298-2_10","volume-title":"FMICS","author":"O. Bunte","year":"2020","unstructured":"Bunte, O., van Gool, L.C.M., Willemse, T.A.C.: Formal verification of OIL component specifications using mCRL2. In: FMICS. Lecture Notes in Computer Science, vol.\u00a012327, pp.\u00a0231\u2013251. Springer, Berlin (2020)"},{"issue":"3","key":"829_CR6","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/s10009-022-00658-y","volume":"24","author":"O. Bunte","year":"2022","unstructured":"Bunte, O., van Gool, L.C.M., Willemse, T.A.C.: Formal verification of OIL component specifications using mCRL2. Int. J. Softw. Tools Technol. Transf. 24(3), 441\u2013472 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"829_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-030-17465-1_2","volume-title":"TACAS (2)","author":"O. Bunte","year":"2019","unstructured":"Bunte, O., Groote, J.F., Keiren, J.J.A., Laveaux, M., Neele, T., de Vink, E.P., Wesselink, W., Wijs, A., Willemse, T.A.C.: The mCRL2 toolset for analysing concurrent systems - improvements in expressivity and usability. In: TACAS (2). Lecture Notes in Computer Science, vol.\u00a011428, pp.\u00a021\u201339. Springer, Berlin (2019)"},{"key":"829_CR8","doi-asserted-by":"publisher","unstructured":"Bunte, O., van Laarhoven, J., Van Gool, L., Willemse, T.: A formalisation of the SMMT language and an instance model in mCRL2 (2025). https:\/\/doi.org\/10.5281\/zenodo.15322352","DOI":"10.5281\/zenodo.15322352"},{"issue":"9","key":"829_CR9","doi-asserted-by":"publisher","first-page":"1426","DOI":"10.1016\/j.ic.2007.05.001","volume":"205","author":"R. Cleaveland","year":"2007","unstructured":"Cleaveland, R., L\u00fcttgen, G., Natarajan, V.: Priority and abstraction in process algebra. Inf. Comput. 205(9), 1426\u20131458 (2007)","journal-title":"Inf. Comput."},{"key":"829_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"TACAS","author":"S. Cranen","year":"2013","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: TACAS. Lecture Notes in Computer Science, vol.\u00a07795, pp.\u00a0199\u2013213. Springer, Berlin (2013)"},{"key":"829_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-030-92124-8_24","volume-title":"SEFM","author":"J. Denkers","year":"2021","unstructured":"Denkers, J., Brunner, M., van Gool, L., Visser, E.: Configuration space exploration for digital printing systems. In: SEFM. Lecture Notes in Computer Science, vol.\u00a013085, pp.\u00a0423\u2013442. Springer, Berlin (2021)"},{"key":"829_CR12","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9946.001.0001","volume-title":"Modeling and Analysis of Communicating Systems","author":"J.F. Groote","year":"2014","unstructured":"Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)"},{"key":"829_CR13","series-title":"Lecture Notes in Computer Science","first-page":"25","volume-title":"FACS","author":"J.F. Groote","year":"2019","unstructured":"Groote, J.F., Keiren, J.J.A., Luttik, B., de Vink, E.P., Willemse, T.A.C.: Modelling and analysing software in mCRL2. In: FACS. Lecture Notes in Computer Science, vol.\u00a012018, pp.\u00a025\u201348. Springer, Berlin (2019)"},{"issue":"1\u20132","key":"829_CR14","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/s11334-009-0116-1","volume":"6","author":"H.H. 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)","journal-title":"Innov. Syst. Softw. Eng."},{"key":"829_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-642-04425-0_33","volume-title":"MoDELS","author":"F. Hermans","year":"2009","unstructured":"Hermans, F., Pinzger, M., van Deursen, A.: Domain-specific languages in practice: a user study on the success factors. In: MoDELS. Lecture Notes in Computer Science, vol.\u00a05795, pp.\u00a0423\u2013437. Springer, Berlin (2009)"},{"key":"829_CR16","first-page":"471","volume-title":"ICSE","author":"J.E. Hutchinson","year":"2011","unstructured":"Hutchinson, J.E., Whittle, J., Rouncefield, M., Kristoffersen, S.: Empirical assessment of MDE in industry. In: ICSE, pp.\u00a0471\u2013480. ACM, New York (2011)"},{"issue":"12","key":"829_CR17","doi-asserted-by":"publisher","first-page":"2435","DOI":"10.1016\/j.scico.2012.11.009","volume":"78","author":"Y. Hwong","year":"2013","unstructured":"Hwong, Y., Keiren, J.J.A., Kusters, V.J.J., Leemans, S.J.J., 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)","journal-title":"Sci. Comput. Program."},{"key":"829_CR18","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2023.103057","volume":"233","author":"P. James","year":"2024","unstructured":"James, P., Moller, F., Pantekis, F.: OnTrack: reflecting on domain specific formal methods for railway designs. Sci. Comput. Program. 233, 103057 (2024). https:\/\/doi.org\/10.1016\/j.scico.2023.103057","journal-title":"Sci. Comput. Program."},{"key":"829_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-319-10431-7_7","volume-title":"SEFM","author":"S. Keshishzadeh","year":"2014","unstructured":"Keshishzadeh, S., Mooij, A.J.: Formalizing DSL semantics for reasoning and conformance testing. In: SEFM. Lecture Notes in Computer Science, vol.\u00a08702, pp.\u00a081\u201395. Springer, Berlin (2014)"},{"key":"829_CR20","first-page":"314","volume-title":"ICEIS","author":"M.J. Klein","year":"2014","unstructured":"Klein, M.J., Sawicki, S., Roos-Frantz, F., Frantz, R.Z.: On the formalisation of an application integration language using Z notation. In: ICEIS, vol.\u00a01, pp.\u00a0314\u2013319. SciTePress (2014)"},{"key":"829_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/3-540-45441-1_19","volume-title":"UML","author":"S. Kuske","year":"2001","unstructured":"Kuske, S.: A formal semantics of UML state machines based on structured graph transformation. In: UML. Lecture Notes in Computer Science, vol.\u00a02185, pp.\u00a0241\u2013256. Springer, Berlin (2001)"},{"key":"829_CR22","unstructured":"van Laarhoven, J.: Formalising the State Machine Modelling Tool (SMMT). Master\u2019s thesis, Eindhoven University of Technology (December 2023)"},{"key":"829_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/978-3-031-68150-9_4","volume-title":"FMICS","author":"J.E.P.M. van Laarhoven","year":"2024","unstructured":"van Laarhoven, J.E.P.M., Bunte, O., van Gool, L.C.M., Willemse, T.A.C.: Formalising the industrial language SMMT in mCRL2. In: FMICS. Lecture Notes in Computer Science, vol.\u00a014952, pp.\u00a063\u201379. Springer, Berlin (2024)"},{"issue":"6","key":"829_CR24","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. Form. Asp. Comput. 11(6), 637\u2013664 (1999)","journal-title":"Form. Asp. Comput."},{"key":"829_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-38088-4_17","volume-title":"NASA Formal Methods","author":"D. Remenska","year":"2013","unstructured":"Remenska, D., Templon, J., Willemse, T.A.C., Homburg, P., Verstoep, K., Ramo, A.C., Bal, H.E.: From UML to process algebra and back: an automated approach to model-checking software design artifacts of concurrent systems. In: NASA Formal Methods. Lecture Notes in Computer Science, vol.\u00a07871, pp.\u00a0244\u2013260. Springer, Berlin (2013)"},{"key":"829_CR26","series-title":"Lecture Notes in Computer Science","first-page":"223","volume-title":"SLE","author":"F.P.M. Stappers","year":"2011","unstructured":"Stappers, F.P.M., Weber, S., Reniers, M.A., Andova, S., Nagy, I.: Formalizing a domain specific language using SOS: an industrial case study. In: SLE. Lecture Notes in Computer Science, vol.\u00a06940, pp.\u00a0223\u2013242. Springer, Berlin (2011)"},{"key":"829_CR27","first-page":"13","volume-title":"ITSLE@SPLASH","author":"J. Stoel","year":"2016","unstructured":"Stoel, J., van der Storm, T., Vinju, J.J., Bosman, J.: Solving the bank with Rebel: on the design of the Rebel specification language and its application inside a bank. In: ITSLE@SPLASH, pp.\u00a013\u201320. ACM, New York (2016)"},{"key":"829_CR28","series-title":"Lecture Notes in Computer Science","first-page":"383","volume-title":"GTTSE","author":"M. Voelter","year":"2011","unstructured":"Voelter, M.: Language and IDE modularization and composition with MPS. In: GTTSE. Lecture Notes in Computer Science, vol.\u00a07680, pp.\u00a0383\u2013430. Springer, Berlin (2011)"},{"key":"829_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/978-3-319-68499-4_7","volume-title":"RSSRail","author":"L.H. Vu","year":"2017","unstructured":"Vu, L.H., Haxthausen, A.E., Peleska, J.: A domain-specific language for generic interlocking models and their properties. In: RSSRail. Lecture Notes in Computer Science, vol.\u00a010598, pp.\u00a099\u2013115. Springer, Berlin (2017)"},{"key":"829_CR30","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)","journal-title":"IEEE Access"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00829-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-025-00829-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-025-00829-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T15:40:23Z","timestamp":1761666023000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-025-00829-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10]]},"references-count":30,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2025,10]]}},"alternative-id":["829"],"URL":"https:\/\/doi.org\/10.1007\/s10009-025-00829-7","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2025,10]]},"assertion":[{"value":"7 October 2025","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 October 2025","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}