Verificação de modelos aplicada ao projeto de controladores digitais implementados em processadores de ponto-fixo

Abstract

The extensive use of fixed-point digital controllers demands a growing effort to prevent design errors that appear in discrete-time domain. The present work describes a novel verification methodology, which employs bounded model checking based on boolean satisfiability and satisfiability modulo theories to verify the occurrence of design errors, due to the finite word-length format, in fixed-point digital controllers. Here, the performance of digital controllers realizations that use delta operators are compared to those that use traditional direct forms. Experimental results show that the delta-form realization substantially reduces the digital controllers’ fragility when compared to the direct-form realization. Additionally, the proposed methodology is very effective and efficient to verify real-world digital controllers, where conclusive results are obtained in nearly 89% of the benchmarks.