Formal verification of a controller implementation in fixed-point arithmetic

TL;DR

This paper presents a formal verification method for controller implementations in fixed-point arithmetic, ensuring overflow-free computations and correctness on digital processors for safety-critical applications.

Contribution

It introduces a computer-certified inductive definition for control functions in fixed-point arithmetic, enabling formal verification of controller correctness on digital processors.

Findings

Verified overflow-free control algorithms in fixed-point arithmetic

Supported polynomial control functions within arbitrary fixed-point structures

Demonstrated the method on a practical case study

Abstract

For the implementations of controllers on digital processors, certain limitations, e.g. in the instruction set and register length, need to be taken into account, especially for safety-critical applications. This work aims to provide a computer-certified inductive definition for the control functions that are implemented on such processors accompanied with the fixed-point data type in a proof assistant. Using these inductive definitions we formally ensure correct realization of the controllers on a digital processor. Our results guarantee overflow-free computations of the implemented control algorithm. The method presented in this paper currently supports functions that are defined as polynomials within an arbitrary fixed-point structure. We demonstrate the verification process in the case study on an example with different scenarios of fixed-point type implementations.