Jordi E. P. M. van Laarhoven
Research Subjects
Jordi E. P. M. van Laarhoven has a total of 3 co-authors. Here are the top co-authors by number of shared publications:
- Louis C. M. van Gool
Canon Production Printing, Venlo, The Netherlands
2 shared publications - Olav Bunte
Eindhoven University of Technology, Eindhoven, The Netherlands
2 shared publications - Tim A. C. Willemse
Eindhoven University of Technology
2 shared publications
Latest Publications
- Open Access
- 22 October 2025
- Published by Springer Nature in International Journal on Software Tools for Technology Transfer
- Vol. 27 (5) , 511-532
Formalising and analysing SMMT models using the mCRL2 toolset
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.
- 22 October 2025
- Published by Springer Nature in International Journal on Software Tools for Technology Transfer
- Vol. 27 (5) , 511-532
Open AccessFormalising and analysing SMMT models using the mCRL2 toolset
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.