5）µ4&&OWVFEFM%0$503A5%&% MJWSé QBS：航空航天高级研究所与佐治亚理工学院（美国）共同辅导1SéTFOUEF FU TPVUFOVF QBS：拉斐尔·P. 科恩2018年12月3日星期一5JUSF：用于模型预测控制的凸优化算法的形式验证与确认应用于预测控制的凸优化算法的形式化验证与确认EDPMF EPDUPSBMF和学科或专业：ED MITT：软件安全和高性能计算6OJUEE EF SFDIFSDIF：ISAE-ONERA MOIS接待团队%JSFDUF VS（T）EFTF：M. Eric FERON（论文主任）M. Pierre-Loïc Garoche（论文主任）陪审团：M. Panagiotis Tsiotras佐治亚理工学院教授-主席M. Pierre-Loïc GAROCHE ONERA研究工程师-博士生导师M. Eric FERON佐治亚理工学院教授-论文主任M. Marcus Holzinger佐治亚理工学院教授M. Tim WANG UTRC研究工程师MI. Cesar Munoz NASA研究员-报告员Hasnaa ZIDANI女士ENST ParisTech教授-报告员用于模型预测控制的凸优化算法的形式验证和确认论文提交至学术教员由拉斐尔·P. 科恩部分履行哲学博士学位的要求在航空航天工程佐治亚理工学院2019年5月公司PYrigHTC 2019年由拉斐尔·科恩用于模型预测控制的凸优化算法的形式验证和确认批准人：Eric Feron教授，佐治亚理工学院航空航天工程学院顾问Panagiotis Tsiotras航空航天工程学院格鲁吉亚理工学院Pierre-Lo c Garoche博士，DTIS联合顾问法国航空Tim Wang博士系统部联合技术研究中心佐治亚理工学院航空航天工程学院Marcus Holzinger教授博士 凯撒A. Munoz安全关键航空电子系统分公司NASA兰利研究中心批准日期：2018年12月iii致我亲爱的祖母黛西iv已知的基因首先，我要感谢我的委员会成员，Holzinger教授、Tsiotras教授、HasnaaZidani博士、Cesar Munoz博士和Tim Wang博士，感谢他们接受成为本博士委员会的一员。本文所做的工作处于多个不同领域的前沿，包括最优控制、优化理论和形式方法。因此，有这样的专家在控制系统，最优控制，空间系统和计算机科学在我的委员会是一个荣誉，我完全意识到我有机会。我的顾问Eric Feron博士感谢您对我的信任，并愿意作为您的博士生与您一起工作。接下来的工作给我带来了很多，从专业和个人的角度来看。我相信，你极其敏锐的知识和研究经验给了我一定程度的成熟，这是我在其他地方无法获得的，我为此感到荣幸。也谢谢你每天给我带来的所有机会，没有你，这些机会都不可能。因为一个完整而健全的博士学位不可能没有一点教学的味道，我想非常感谢你有我作为你的助教。正如你已经知道的，我真的很享受这部分的工作，并期待着再次这样做。对于我的联合顾问Pierre-Lo ic Garoche博士，我觉得很多余，但我想非常感谢你，感谢你对我的信任，感谢你愿意让我在图卢兹的Onera与你从Feron教授告诉我这个与你合作你的指导给我带来了很多，我想表达我对你的感激之作为你的博士生和你一起工作v这是一次令人兴奋和非常足智多谋的旅行。这篇博士论文是在格鲁吉亚技术研究所和法国图卢兹的航空航天研究所（ISAE）的共同监督下完成的，我想对这两个机构的所有员工表示感谢，他们使这一共同监督成为我提前为我将要忘记的每一个人道歉，但我想感谢我在佐治亚理工学院的所有朋友，汤姆，海伦，加布里埃尔，埃洛德，路易斯，菲利普，特雷，通德，科尔宾，马克，凯文，哈罗德，何塞，大卫，朱塞佩，阿尤什，等等。. . ...此外，我想真诚地感谢奥内拉的每一个人，当我到达图卢兹时，他们欢迎我，特别是纪尧姆，雨果，马修，埃马努埃莱，凯文，珍妮，奥斯卡和更多......Guillaume，再次感谢你在我到达图卢兹时欢迎我，并在整个论文过程中提供帮助，特别是使用正式的方法。此外，有你在我身边，像我一样痛苦，并与Frama-C战斗给了我一些安慰，使我避免了严重的崩溃。我还要感谢Pierre Roux和ArnaudDieumegard，感谢他们的帮助，感谢他们一直为我服务。像往常一样，如果没有资金，这一切都是不可能的，所以我要感谢赞助商，国家科学基金会（NSF）和法国航空航天实验室（ONERA）。妈妈，爸爸，Rebecca，Eva，还有我亲爱的兄弟，尼腓和侄女，圣斯蒂芬，亚伦，诺姆和塔希尔。谢谢你们所有人给我的爱和支持。在离你们很远的地方做这篇博士论文是困难和痛苦的，我很想念你们。vi每天。黛西妈妈，我会永远记得你是一个多么美丽的女人和慈爱的祖母。我很难过你不得不这么残忍地去，你不能看到这一切。阿玛拉，我爱你。我的世界对我来说意味着一切。谢谢你每天给我的支持。vii内容物奉献III表列表。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... x图XI列表符号列表xiv摘要17我的介绍。 . . . . . . . . . . . . . . . . . . . . . . . . . . ... ...2可信的自动编码框架。 . . . . . . . . . . . . . . . . . ... ...31.2形式验证。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...51.2.1软件语义学。 . . . . . . . . . . . . . . . . . . . ... ...51.2 Hoare逻辑。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...61.2.3最弱前提条件。 . . . . . . . . . . . . . . . . . . . ... ...91.3最新技术水平和论文101.3.1基于实时优化的控制1.3.2控制系统软件的正式验证1.3.3正式验证和软件认证13IILTI系统的基于优化的控制2.1线性时间不变（LTI）系统182.1.1LTI理论与状态空间实现2.1.2LTI系统的稳定性192.2凸优化问题222.3基于实时凸优化的控制和MPC232.3.1MPC和路径规划之间的26viiiIII 椭圆体方法及其语义学3.1优化理论简史303.2椭圆体方法313.3与椭圆体方法38相关的ACSL理论构建3.3.1线性代数公理化383.3.2优化理论公理化413.4注释椭圆体方法的43IV浮动点分析484.1过去的系统故障和动机484.1.1美国爱国者48导弹4.1.2阿丽亚娜5号火箭494.1.3动机504.2控制条件编号504.2.1单值的边界514.2.2相应条件编号554.2.3C55上的对应规范4.2.4对代码55的影响4.3通过算法传播舍入误差574.3.1第58章第一次见面4.3.2标准和边界584.3.3基本变换的浮点循环594.4数值稳定的必要条件614.4.1问题公式614.4.2覆盖范围的等效和充分条件614.4.3覆盖的分析充分条件64V自动编码器和闭环管理ix5.1闭环管理5.1.1参数化线性约束695.1.2二阶圆锥约束745.2运行时间评估765.3GENEMO编程语言语法775.3.1使用Genemo和Autocode可信地实现操作定时算法5.3.2自动编码器79的内部外观5.4实时模拟和示例805.4.1弹簧质量系统805.4.2三自由度直升机825.4.3四轴飞行器无人机86VI结论90附录A- ACSL线性代数理论92附录BACSL优化和椭圆化-ORY......................................................................100附录C-用于生成C代码的输入文件。106参考文献109VITA113x表列表1不同问题大小的性能822浮点考虑823不同视野的性能xi图列表1用于可信自动编码的。 . . . . . . . . . . . . . . ... ...42可信自动编码算法。 . . . . . . ... ...5 - 3三重Hoare。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...64在ACSL中表示三重Hoare示例1 . . . . . . . . . . . . ... ...75在ACSL中表示的三重Hoare示例2 . . . . . . . . . . . . ... ...76ACSL中的内存分配问题示例。 . . . . . . . . . . ... ...87更正了内存分配检查的功能合同。... ...88ACSL职能合同示例。... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ... ...99最弱的前提条件插图。. . . . . . . . . . . . . . . . . . .910闭环系统.................. 2011一些凸优化问题的分类12MPC闭环系统2513MPC技术图2514弹簧质量系统2515闭环位置与时间2716闭环速度与时间的关系17输入力与时间的关系2818Ellispoid方法交易关闭3319椭圆体切割3420LP设置中的椭圆体切割3521包含和包含球3722ACSL线性代数理论3923椭圆体类型定义4024存在向量ACSL Lemma4125椭圆体方法ACSL Lemma4126ACSL优化类型定义42xii27ACSL可行谓词定义43xiii28getNorm 2标头C代码文件...............................................................................4429getNorm 2正文C代码文件...............................................................................4530getp.c正文C代码文件4531getp.h标头文件4632美国爱国者49导弹33欧洲阿丽亚娜5火箭5034校正的椭圆体5435getFrobeniusNorm注释C函数5736椭圆体增宽6237Pu和Pl多面体组7138单位球R27639二阶圆锥体40弹簧质量系统的常数截面7741弹簧质量系统的目标部分7842弹簧质量系统的约束截面7843弹簧质量系统信息部分7844弹簧质量系统的输入/输出部分7945Autocoder80的内部外观463自由度直升机82473 DOF直升机轴和尺寸8348用于Quanser仿真的文件8549状态向量与时间8550低西高度与时间8651无人机87上的圆锥约束5289四轴飞行器的MPC模拟53线性代数ACSL理论9254线性代数ACSL理论（第2部分）93xiv55线性代数ACSL理论（第3部分）9456线性代数ACSL理论（第4部分）95xv57线性代数ACSL理论（第5部分）9658线性代数ACSL理论（第6部分）9759线性代数ACSL理论（第7部分）9860优化ACSL理论10061ACSL优化理论（第2部分）10162ACSL优化理论（第3部分）10263ACSL优化理论（第4部分）10364ACSL优化理论（第5部分）10465ACSL优化理论（第6部分）10566单点优化文本文件10667Spring质量自动编码器输入文件107683自由度直升机着陆问题：自动编码器输入文件108xvi符号列表符号描述R是所有实数的集合R+所有正实数的集合。R*+所有严格意义上的真实和真实的集合。Rn长度为n的实向量集。Rm×n是大小为m × n的实数矩阵的集合。矩阵A的Frobenius正规。矩阵A的两个归一化。xn维单位欧几里得球。Bn={z奏效Rn：z≤ 1}。Br（x）半径为r的球以x为中心。Br（x）={z奏效Rn：z−x≤r}。Ell（B，c）椭圆体集定义为：Ell（B，c）={Bu+c：u奏效Bn}Vol（）一套给定的卷。fl（）浮点舍入到给定实数的最接近值。σmax（A）矩阵A的最大奇异值。σmin（A）矩阵A的最小奇异值。k（A）矩阵A的条件数。x 植物状态向量。N模型预测控制水平。x到地平线的sta tev向量的集合：x =[x1. ... ... XN]。工厂输入。u在地平线上的输入集合：u=[u1. ... ... n−1]。xviiX优化问题的原始决策向量优化问题的Z投影决策向量Xf优化问题的可行集。一个优化问题的XEpsilon最优集ACSL在本地合同或功能合同中引入前提条件。在局部契约或函数契约中引入后置条件。列出在函数约定中分配的内存。\result引用C函数的输出循环不变量引入循环不变量，即循环每次迭代时为true的属性。循环变量在可 计数集（通常为N）中引入严格正的递减量。需要证明终止。循环分配列出在循环中分配的公理化定义一种新的ACSL理论。包含新的类型、函数、公理、引理、定理。定义一个新的引理。需要证明。定义一个新定理。需要证明。定义一个新的公理。假设是真的。逻辑定义新的ACSL函数。谓词定义和命名给定的ACSL属性。xviii基因文件介绍可以定义常量的部分。变量定义优化问题的决策变量。输入定义MPC输入的可选部分。输出定义MPC输出的可选部分。最小化引入要最小化的成本。SubjectTo介绍了优化问题的约束条件。信息介绍了验证所需的标量。首字母缩略词ANSI/C规范语言。AST抽象语法树。CPS网络物理系统。自由度HLR高级要求 LP线性编程。LTI线性时间不变。LLR低级别要求。MPC模型预测控制。QCQP二次约束二次规划。QP二次规划。RHC回收地平线控制。SDP半定义编程。SMT 可满足性模理论。SOCP二阶圆锥编程。xix摘要现代优化方法的效率，加上计算资源的增加，导致了实时优化算法扮演安全关键角色的可能性。然而，如果不适当地关注这些算法的合理性，这是不可能发生的。本博士论文讨论了凸优化算法的形式化验证，特别强调了接收视界控制器。此外，我们演示了如何使用实时优化算法的理论证明来描述代码级的函数属性，从而使形式化方法社区能够访问它。在寻找零错误软件时，我们使用了可信的Au- tocoding方案。在这个框架中，通过使用可信的我们将注意力集中在求解二阶圆锥体Pro-gram（SOCP）的椭圆体方法上。此外，我们还介绍了原始椭圆体方法的修改版本，以考虑和控制其数值误差。在此之后，对该算法进行了浮点分析，并提出了一个框架来数值验证该方法。
我的内容管理
展开
