Formalising and analysing SMMT models using the mCRL2 toolset

Jordi E.P.M. van Laarhoven; Olav Bunte; Louis C.M. van Gool; Tim A.C. Willemse

doi:10.1007/s10009-025-00829-7

Formalising and analysing SMMT models using the mCRL2 toolset

Jordi E.P.M. van Laarhoven
, Olav Bunte
, Louis C.M. van Gool
, Tim A.C. Willemse (Corresponding author)

Research output: Contribution to journal › Article › Academic › peer-review

1 Citation (Scopus)

14 Downloads (Pure)

Abstract

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.

Original language	English
Pages (from-to)	511-532
Number of pages	22
Journal	International Journal on Software Tools for Technology Transfer
Volume	27
Issue number	5
DOIs	https://doi.org/10.1007/s10009-025-00829-7
Publication status	Published - Oct 2025

Keywords

Domain-specific languages
Formal verification
Model checking
Formalisation

Access to Document

10.1007/s10009-025-00829-7

pdfFinal published version, 2.3 MB

Cite this

@article{7f023cd8f9424cba8d32d113aac8ebea,

title = "Formalising and analysing SMMT models using the mCRL2 toolset",

abstract = "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.",

keywords = "Domain-specific languages, Formal verification, Model checking, Formalisation",

author = "\{van Laarhoven\}, \{Jordi E.P.M.\} and Olav Bunte and \{van Gool\}, \{Louis C.M.\} and Willemse, \{Tim A.C.\}",

year = "2025",

month = oct,

doi = "10.1007/s10009-025-00829-7",

language = "English",

volume = "27",

pages = "511--532",

journal = "International Journal on Software Tools for Technology Transfer",

issn = "1433-2779",

publisher = "Springer",

number = "5",

}

TY - JOUR

T1 - Formalising and analysing SMMT models using the mCRL2 toolset

AU - van Laarhoven, Jordi E.P.M.

AU - Bunte, Olav

AU - van Gool, Louis C.M.

AU - Willemse, Tim A.C.

PY - 2025/10

Y1 - 2025/10

N2 - 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.

AB - 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.

KW - Domain-specific languages

KW - Formal verification

KW - Model checking

KW - Formalisation

U2 - 10.1007/s10009-025-00829-7

DO - 10.1007/s10009-025-00829-7

M3 - Article

SN - 1433-2779

VL - 27

SP - 511

EP - 532

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

IS - 5

ER -

Formalising and analysing SMMT models using the mCRL2 toolset

Abstract

Keywords

Access to Document

Fingerprint

Cite this