Formal verification of a controller implementation in fixed-point arithmetic
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Of Good Demons and Bad Angels: Guaranteeing Safe Control under Finite Precision
As neural networks (NNs) become increasingly prevalent in safety-critical neural network-controlled cyber-physical systems (NNCSs), formally guaranteeing their safety becomes crucial. For these systems, safety must be en…
Scalable and Interpretable Verification of Image-based Neural Network Controllers for Autonomous Vehicles
Existing formal verification methods for image-based neural network controllers in autonomous vehicles often struggle with high-dimensional inputs, computational inefficiency, and a lack of explainability. These challeng…
Autonomous VehiclesDecoderRobust Verification of Controllers under State Uncertainty via Hamilton-Jacobi Reachability Analysis
As perception-based controllers for autonomous systems become increasingly popular in the real world, it is important that we can formally verify their safety and performance despite perceptual uncertainty. Unfortunately…
Verification in the Loop: Correct-by-Construction Control Learning with Reach-avoid Guarantees
In the current control design of safety-critical autonomous systems, formal verification techniques are typically applied after the controller is designed to evaluate whether the required properties (e.g., safety) are sa…
Joint Differentiable Optimization and Verification for Certified Reinforcement Learning
In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties (e.g., safety, stability) under the learned controller. However, as existing methods typica…
Bilevel OptimizationModel-based Reinforcement Learningreinforcement-learningReinforcement Learning+1