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

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

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

【文章目錄】：
摘要
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)容及安排
第二章 背景知識
    2.1 交互式定理證明器Coq
        2.1.1 概述
        2.1.2 實數(shù)理論及微積分
        2.1.3 對偶與復(fù)數(shù)
        2.1.4 三角函數(shù)與指數(shù)
        2.1.5 搭建基于交互式定理證明器Coq的開發(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é)公式驗證
    3.1 直升機(jī)自動過渡飛行控制系統(tǒng)驗證
        3.1.1 介紹
        3.1.2 高度的自動過渡
        3.1.3 前向速度的自動過渡
        3.1.4 按指數(shù)規(guī)律拉平
    3.2 直升機(jī)艦上起飛過程及軌跡生成驗證
        3.2.1 Z_E軸軌跡生成
        3.2.2 X_E軸軌跡生成
    3.3 直升機(jī)著艦過程及軌跡生成驗證
        3.3.1 返航進(jìn)場階段軌跡生成
        3.3.2 降落段軌跡設(shè)計
    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 未來工作展望
參考文獻(xiàn)
致謝
在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文



本文編號：3806204