Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking
2014 Brazilian Symposium on Computing Systems Engineering (SBESC) (2014)
Manaus, Amazonas, Brazil
Nov. 3, 2014 to Nov. 7, 2014
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SBESC.2014.14
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.
Stability analysis, Limit-cycles, Model checking, Control systems, Numerical stability, Quantization (signal), Time factors
I. V. Bessa, H. I. Ismail, L. C. Cordeiro and J. E. Filho, "Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking," 2014 Brazilian Symposium on Computing Systems Engineering (SBESC), Manaus, Amazonas, Brazil, 2014, pp. 49-54.