Automated Code Generation for DES Controllers Modeled as Finite State Machines

  • Tiago Possato UTFPR / IFC
  • João H. Valentini UTFPR
  • Luiz F. P. Southier UTFPR
  • Marcelo Teixeira UTFPR

Resumo


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.
Palavras-chave: Formal modeling, Model conversion, Code generation
Publicado
04/12/2023
POSSATO, Tiago; VALENTINI, João H.; SOUTHIER, Luiz F. P.; TEIXEIRA, Marcelo. Automated Code Generation for DES Controllers Modeled as Finite State Machines. In: SIMPÓSIO BRASILEIRO DE MÉTODOS FORMAIS (SBMF), 26. , 2023, Manaus/AM. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2023 . p. 113-130.