Trabalho em anais de eventoOpen Access
SMT-based bounded model checking of fixed-point digital controllers
BESSA, IURY; ABREU, RENATO; FILHO, JOAO EDGAR; CORDEIRO, LUCAS
Resumo
Resumo
Digital controllers have several advantages with respect to their flexibility and design's simplicity. However, they are subject to problems that are not faced by analog controllers. In particular, these problems are related to the finite word-length implementation that might lead to overflows, limit cycles, and time constraints in fixed-point or floating-point processors. This paper proposes a new method to detect design's errors in fixed-point digital controllers using a state-of-the art bounded model checker based on satisfiability modulo theories. The experiments with a commercial plant demonstrate that the proposed method can be effective in finding errors in digital controllers than other existing approaches, which are based on traditional simulations tools. The verification results are conclusive in 93.5% of the benchmarks, determining the absence or occurrence of errors.
Autoria
Autores do grupo (3)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
bounded model checkingsatisfiability modulo theoriesfinite word length effectsoverflowlimit cyclescontroller verificationdesign error detectiondigital controller synthesis
Status
Published
links
Links e arquivos
Trabalho em anais de evento