Treffer: Formalising and analysing SMMT models using the mCRL2 toolset.

Title:
Formalising and analysing SMMT models using the mCRL2 toolset.
Authors:
van Laarhoven, J. E. P. M.1 (AUTHOR) jordi.vanlaarhoven@cpp.canon, Bunte, O.2 (AUTHOR) o.bunte@tue.nl, van Gool, L. C. M.1 (AUTHOR) louis.vangool@cpp.canon, Willemse, T. A. C.2 (AUTHOR) t.a.c.willemse@tue.nl
Source:
International Journal on Software Tools for Technology Transfer. Oct2025, Vol. 27 Issue 5, p511-532. 22p.
Subject Terms:
*SOFTWARE verification, *PROGRAMMING language semantics, *SOFTWARE validation, *CODE generators, *FINITE state machines, *COMPUTER software
Database:
Academic Search Index

Weitere Informationen

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. [ABSTRACT FROM AUTHOR]