论文标题
验证和验证模型预测控制的凸优化算法
Verification and Validation of Convex Optimization Algorithms for Model Predictive Control
论文作者
论文摘要
高级嵌入式算法的复杂性正在增长，它们是许多领域自治的增长的重要贡献。但是，如果没有适当关注关注的应用（例如航空航天系统）是安全至关重要的，这些算法所持有的承诺就无法保留。正式验证是通过计算机对其某些数学描述来证明或反驳算法的“正确性”的过程。本文讨论了椭圆形方法的正式验证，凸优化算法及其适用于恢复视野控制的代码实现。详细介绍了编码代码属性及其证明的选项。这些代码属性和证明的适用性和局限性也会提出。最后，在椭球算法的数值分析中考虑了浮点误差。提出了对算法的修改，可用于控制其数值稳定性。
Advanced embedded algorithms are growing in complexity and they are an essential contributor to the growth of autonomy in many areas. However, the promise held by these algorithms cannot be kept without proper attention to the considerably stronger design constraints that arise when the applications of interest, such as aerospace systems, are safety-critical. Formal verification is the process of proving or disproving the ''correctness'' of an algorithm with respect to a certain mathematical description of it by means of a computer. This article discusses the formal verification of the Ellipsoid method, a convex optimization algorithm, and its code implementation as it applies to receding horizon control. Options for encoding code properties and their proofs are detailed. The applicability and limitations of those code properties and proofs are presented as well. Finally, floating-point errors are taken into account in a numerical analysis of the Ellipsoid algorithm. Modifications to the algorithm are presented which can be used to control its numerical stability.
