定理證明是人工智能的一個(gè)分支,它的研究目標(biāo)是在計(jì)算機(jī)輔助下進(jìn)行數(shù)學(xué)定理的證明�；诙ɡ碜C明的形式化驗(yàn)證技術(shù)已經(jīng)被廣泛應(yīng)用于數(shù)學(xué)定理的證明驗(yàn)證以及軟件正確性驗(yàn)證。然而定理證明技術(shù)在工程數(shù)學(xué)中的應(yīng)用還十分罕見(jiàn)。安全飛行控制系統(tǒng)在飛行控制中扮演了一個(gè)重要的角色并且被認(rèn)為是飛機(jī)的“大腦”。只有該系統(tǒng)被驗(yàn)證為正確的飛機(jī)才能安全穩(wěn)定的飛行。飛行控制算法是飛行控制系統(tǒng)的核心,它的基礎(chǔ)是大量繁復(fù)的微積分?jǐn)?shù)學(xué)推導(dǎo),這些數(shù)學(xué)推導(dǎo)的正確性對(duì)飛行控制系統(tǒng)的安全性有關(guān)鍵性作用。歐洲曾經(jīng)發(fā)生由于下降過(guò)程控制的失誤導(dǎo)致火星著陸的失敗。在直升機(jī)飛行控制數(shù)學(xué)的形式化驗(yàn)證方面,目前國(guó)際上是空白。本文是基于定理證明器Coq對(duì)直升機(jī)飛行控制系統(tǒng)中的部分?jǐn)?shù)學(xué)公式的推導(dǎo)進(jìn)行的形式化驗(yàn)證初步探索,主要研究?jī)?nèi)容如下:第一,對(duì)以顯模型跟蹤控制系統(tǒng)為基礎(chǔ)的直升機(jī)自動(dòng)過(guò)渡飛行控制過(guò)程進(jìn)行驗(yàn)證。這一過(guò)程分為高度過(guò)渡和速度過(guò)渡兩個(gè)方面,其中高度又分拋物線下降和指數(shù)拉平兩個(gè)階段。這兩個(gè)階段本身受相應(yīng)的物理定律和控制目標(biāo)約束,兩者之間需要平滑的連接。下降曲線所滿(mǎn)足的數(shù)學(xué)公式來(lái)源于在這些約束條件下的推導(dǎo)。我們對(duì)這一推導(dǎo)過(guò)程進(jìn)行了形式化描述和驗(yàn)證。第...

【文章頁(yè)數(shù)】：74 頁(yè)

【學(xué)位級(jí)別】：碩士

【文章目錄】：
摘要
abstract
第一章 緒論
    1.1 研究背景
        1.1.1 定理證明與形式化工程數(shù)學(xué)
        1.1.2 安全飛行控制系統(tǒng)
    1.2 研究現(xiàn)狀
        1.2.1 定理證明的研究
        1.2.2 飛行控制系統(tǒng)的形式化及安全性研究
    1.3 研究目的和意義
    1.4 本文內(nèi)容及安排
第二章 背景知識(shí)
    2.1 交互式定理證明器Coq
        2.1.1 概述
        2.1.2 實(shí)數(shù)理論及微積分
        2.1.3 對(duì)偶與復(fù)數(shù)
        2.1.4 三角函數(shù)與指數(shù)
        2.1.5 搭建基于交互式定理證明器Coq的開(kāi)發(fā)環(huán)境
    2.2 直升機(jī)飛行控制系統(tǒng)
        2.2.1 概述
        2.2.2 顯模型跟蹤控制系統(tǒng)
    2.3 本章小結(jié)
第三章 基于Coq的直升機(jī)典型飛行控制系統(tǒng)數(shù)學(xué)公式驗(yàn)證
    3.1 直升機(jī)自動(dòng)過(guò)渡飛行控制系統(tǒng)驗(yàn)證
        3.1.1 介紹
        3.1.2 高度的自動(dòng)過(guò)渡
        3.1.3 前向速度的自動(dòng)過(guò)渡
        3.1.4 按指數(shù)規(guī)律拉平
    3.2 直升機(jī)艦上起飛過(guò)程及軌跡生成驗(yàn)證
        3.2.1 Z_E軸軌跡生成
        3.2.2 X_E軸軌跡生成
    3.3 直升機(jī)著艦過(guò)程及軌跡生成驗(yàn)證
        3.3.1 返航進(jìn)場(chǎng)階段軌跡生成
        3.3.2 降落段軌跡設(shè)計(jì)
    3.4 本章小結(jié)
第四章 基于Coq的 Z變換形式化
    4.1 Z變換的形式化
        4.1.1 介紹
        4.1.2 預(yù)備措施
        4.1.3 Z變換的定義
    4.2 Z變換的性質(zhì)
        4.2.1 齊次性質(zhì)
        4.2.2 均勻性質(zhì)
        4.2.3 線性性質(zhì)
        4.2.4 復(fù)數(shù)位移性質(zhì)
    4.3 本章小結(jié)
第五章 總結(jié)與展望
    5.1 研究工作總結(jié)
    5.2 未來(lái)工作展望
參考文獻(xiàn)
致謝
在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文



本文編號(hào)：3806204