Automated Code Generation for DES Controllers Modeled as Finite State Machines - Possato, Tiago; Valentini, João H.; Southier, Luiz F. P.; Teixeira, Marcelo (Anais do Simpósio Brasileiro de Métodos Formais (SBMF); 2023: Anais do XXVI Simpósio Brasileiro de Métodos Formais, 2023)
Finite State Machines (FSMs) are the foundation to design Discrete Event Systems (DESs). A FSM that designs a DES model can be further processed using Supervisory Control Theory (SCT) to synthesize correct-by-construction software. When applied to industrial-scale DESs, FSMs face limitations in the design, synthesis, and implementation steps. Supremica is a straightforward tool that facilitates design and synthesis but does not reach the implementation phase. This requires additional tools to convert FSM models into code. This paper presents the tool DEScMaker, which receives as input an FSM model outputting from Supremica and converts it into implementable C code. Our approach complements Supremica with code generation and allows taking advantage of its intuitive interface, useful simulator, and safe algorithms while automating a task that, in practice, consists of complex manual programming. An example illustrates the tool and quantifies its advantages.