Louis C. M. van Gool

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.

Domain-specific languages (DSLs) promise to improve the software engineering process, e.g., by reducing software development and maintenance effort and by improving communication, and are therefore seeing increased use in industry. To support the creation and deployment of DSLs, language workbenches have been developed. However, little is published about the actual added value of a language workbench in an industrial setting, compared to not using a language workbench. In this paper, we evaluate the productivity of using the Spoofax language workbench by comparing two implementations of an industrial DSL, one in Spoofax and one in Python, that already existed before the evaluation. The subject is the Open Interaction Language (OIL): a complex DSL for implementing control software with requirements imposed by its industrial context at Canon Production Printing. Our findings indicate that it is more productive to implement OIL using Spoofax compared to using Python, especially if editor services are desired. Although Spoofax was sufficient to implement OIL, we find that Spoofax should especially improve on practical aspects to increase its adoptability in industry.