基于Coq的直升机形式化飞行控制数学初步探索

发布时间：2023-04-30 02:11

　　定理证明是人工智能的一个分支,它的研究目标是在计算机辅助下进行数学定理的证明。基于定理证明的形式化验证技术已经被广泛应用于数学定理的证明验证以及软件正确性验证。然而定理证明技术在工程数学中的应用还十分罕见。安全飞行控制系统在飞行控制中扮演了一个重要的角色并且被认为是飞机的“大脑”。只有该系统被验证为正确的飞机才能安全稳定的飞行。飞行控制算法是飞行控制系统的核心,它的基础是大量繁复的微积分数学推导,这些数学推导的正确性对飞行控制系统的安全性有关键性作用。欧洲曾经发生由于下降过程控制的失误导致火星着陆的失败。在直升机飞行控制数学的形式化验证方面,目前国际上是空白。本文是基于定理证明器Coq对直升机飞行控制系统中的部分数学公式的推导进行的形式化验证初步探索,主要研究内容如下:第一,对以显模型跟踪控制系统为基础的直升机自动过渡飞行控制过程进行验证。这一过程分为高度过渡和速度过渡两个方面,其中高度又分抛物线下降和指数拉平两个阶段。这两个阶段本身受相应的物理定律和控制目标约束,两者之间需要平滑的连接。下降曲线所满足的数学公式来源于在这些约束条件下的推导。我们对这一推导过程进行了形式化描述和验证。第...

【文章页数】：74 页

【学位级别】：硕士

【文章目录】：
摘要
abstract
第一章 绪论
    1.1 研究背景
        1.1.1 定理证明与形式化工程数学
        1.1.2 安全飞行控制系统
    1.2 研究现状
        1.2.1 定理证明的研究
        1.2.2 飞行控制系统的形式化及安全性研究
    1.3 研究目的和意义
    1.4 本文内容及安排
第二章 背景知识
    2.1 交互式定理证明器Coq
        2.1.1 概述
        2.1.2 实数理论及微积分
        2.1.3 对偶与复数
        2.1.4 三角函数与指数
        2.1.5 搭建基于交互式定理证明器Coq的开发环境
    2.2 直升机飞行控制系统
        2.2.1 概述
        2.2.2 显模型跟踪控制系统
    2.3 本章小结
第三章 基于Coq的直升机典型飞行控制系统数学公式验证
    3.1 直升机自动过渡飞行控制系统验证
        3.1.1 介绍
        3.1.2 高度的自动过渡
        3.1.3 前向速度的自动过渡
        3.1.4 按指数规律拉平
    3.2 直升机舰上起飞过程及轨迹生成验证
        3.2.1 Z_E轴轨迹生成
        3.2.2 X_E轴轨迹生成
    3.3 直升机着舰过程及轨迹生成验证
        3.3.1 返航进场阶段轨迹生成
        3.3.2 降落段轨迹设计
    3.4 本章小结
第四章 基于Coq的 Z变换形式化
    4.1 Z变换的形式化
        4.1.1 介绍
        4.1.2 预备措施
        4.1.3 Z变换的定义
    4.2 Z变换的性质
        4.2.1 齐次性质
        4.2.2 均匀性质
        4.2.3 线性性质
        4.2.4 复数位移性质
    4.3 本章小结
第五章 总结与展望
    5.1 研究工作总结
    5.2 未来工作展望
参考文献
致谢
在学期间的研究成果及发表的学术论文



本文编号：3806204