Formalising and analysing SMMT models using the mCRL2 toolset
Open Access
- 22 October 2025
- journal article
- general
- Published by Springer Nature in International Journal on Software Tools for Technology Transfer
- Vol. 27 (5) , 511-532
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
This publication has 28 references indexed in Scilit:
- Formalising the Industrial Language SMMT in mCRL22024
- Configuration Space Exploration for Digital Printing Systems2021
- A Formalisation of SysML State Machines in mCRL22021
- Formal Verification of OIL Component Specifications using mCRL22020
- The mCRL2 Toolset for Analysing Concurrent Systems2019
- A Domain-Specific Language for Generic Interlocking Models and Their Properties2017
- Formalising the Dezyne Modelling Language in mCRL22017
- Formalizing DSL Semantics for Reasoning and Conformance TestingLecture Notes in Computer Science, 2014
- Formal Methods Meet Domain Specific Languages2005
- A Formal Semantics of UML State Machines Based on Structured Graph Transformation2001