Formalising the Industrial Language SMMT in mCRL2

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 have reverse-engineered the semantics that is associated to models specified in SMMT and subsequently formalised their semantics in the mCRL2 language. Using this formalisation, we have been able to detect subtle bugs in the implementation of the SMMT tool. Moreover, our formalisation allows for verifying the models specified in SMMT before the code is generated, offering users the option to thoroughly verify their designs.