Automated Code Generation for DES Controllers Modeled as Finite State Machines
Abstract
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.
Keywords:
Formal modeling, Model conversion, Code generation
Published
2023-12-04
How to Cite
POSSATO, Tiago; VALENTINI, João H.; SOUTHIER, Luiz F. P.; TEIXEIRA, Marcelo.
Automated Code Generation for DES Controllers Modeled as Finite State Machines. In: BRAZILIAN SYMPOSIUM ON FORMAL METHODS (SBMF), 26. , 2023, Manaus/AM.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2023
.
p. 113-130.
