Formal verification of a controller implementation in fixed-point arithmetic
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.
Keywords
Cite
@article{arxiv.2112.01204,
title = {Formal verification of a controller implementation in fixed-point arithmetic},
author = {Lars Flessing and Grigory Devadze and Stefan Streif},
journal= {arXiv preprint arXiv:2112.01204},
year = {2021}
}