Model-Driven (Software) Engineering (MDSE) is gaining popularity in industry. More and more companies acknowledge the benefits of using MDSE to develop their software components. A company that exploits model-driven software engineering is Canon Production Printing (Venlo, The Netherlands). At Canon Production Printing, the State Machine Modelling Tool (SMMT) was developed to enable the modelling of software components using state machines. In this graduation report, we present SMMT and formally define a subset of the SMMT language. A translation from SMMT specifications to mCRL2 specifications is defined to allow for model checking on the SMMT specifications. We show that this translation can correctly generate mCRL2 specifications for the existing SMMT specifications at Canon Production Printing. Furthermore, we show how the mCRL2 toolset can be used to prove the correctness of SMMT specifications.