Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking

• Iury Bessa UFAM
• Hussama Ibrahim UFAM
• Lucas Cordeiro UFAM
• João Edgar Chaves Filho UFAM

Resumo

The extensive use of fixed-point digital controllers demands a growing effort to prevent design's errors that appear in the discrete-time domain. This paper presents a novel verification methodology that employs Bounded Model Checking (BMC) based on the Satisfiability Modulo Theories to verify the occurrence of design's 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. The experimental results show that the delta form realization reduces substantially the digital controllers' fragility. Additionally, the proposed methodology can be very effective and efficient to verify real-world digital controllers, where conclusive results are obtained in nearly 95% of the benchmarks.

Palavras-chave: Stability analysis, Limit-cycles, Model checking, Control systems, Numerical stability, Quantization (signal), Time factors, fixed-point digital controllers, delta form, formal methods, bounded model checking