Laplace变换在Coq中的形式化及其在飞控系统验证中的应用

发布时间：2020-08-01 16:58

【摘要】：形式化数学是一个借助定理证明器进行数学定理机械验证的研究方向。形式化工程数学是形式化数学技术在工程数学领域中的应用。在控制系统设计中的一个关键性数学工具是Laplace变换,它被广泛地应用于求解线性微分方程和分析安全关键系统,它也是包括飞行控制系统在内的许多控制算法设计和软件设计的基础工具。定理证明是利用计算机辅助人们进行数学定理证明,它克服了纯人工证明容易出错等缺点,已经广泛应用于数学定理证明、集成电路和软件验证中,然而在飞行控制方面的形式化验证工作十分罕见。一个典型的例子是采用SCADE系统进行建模、开发和验证飞行控制软件,虽然基于模型的方法提高了软件生产力并且减少了软件缺陷,但是并不能解决数学推导和飞控数学算法的可靠性验证问题。飞行控制系统的设计和分析依赖于大量复杂的数学推导,为了解决这样的问题,我们研究基于Coq定理证明器的形式化工程数学验证技术。这一工作的大方向是在Coq中建立完善的形式化工程数学理论库,以便支持飞行控制数学以及其他工程数学的推导验证。本文在高阶逻辑定理证明器Coq中采用极限、连续、微分、积分、复数等理论实现了Laplace变换定义的形式化,并且验证了Laplace变换的主要性质:存在性、线性性质、复频域位移性质、微分性质、二阶微分性质、积分性质等。为了能验证更复杂的控制系统,本文给出了二维向量Laplace变换的形式化定义,并且验证了向量Laplace变换基本性质。目前尚未在文献中发现将Laplace变换形式化理论推广到二维向量的类似工作,这一工作已经能够有效支持实际应用中大部分控制系统的形式化验证。二维Laplace变换依赖于矩阵理论,我们采用基于元组的表示方法对小规模的矩阵(2-4维)进行形式化定义并且对矩阵的运算、向量的运算以及矩阵和向量之间的运算进行形式化定义。在此基础上,我们对这些矩阵运算的正确性以及运算性质进行形式化证明。最后我们对飞行控制系统、机器人控制系统中的一些传递函数的推导过程进行了形式化的描述和验证。
【学位授予单位】：南京航空航天大学
【学位级别】：硕士
【学位授予年份】：2019
【分类号】：V249.1;TB11
【图文】：

原理图,定理证明,原理

公式来描述系统及其性质，并且通过定义公理和推导规则来证传统需要人工纸笔证明的数学定理和日常生活中的推理变成了它与传统的数学证明是不一样的，传统证明大多数都是依靠不言一步都需要有完整的证明过程，所以整个定理证明过程中每一个步骤准确无误。但是这也是它的缺点，有时候非常简单的证但是计算机是能够处理这些复杂的证明过程的。定理证明分为。定理证明的发展是从自动定理证明开始，由于其自动化的特。但是很多复杂数据类型的定理是不能够通过自动化的方式完能处理非常有限的情况[8]。在实际应用中，大规模的控制系统此出现了逻辑表述能力更强的交互式定理证明[9]。交互式定理证技术，虽然不能自动推理，但是对于复杂程度不高的问题，策略[10]，比如等式自动证明策略、导数自动证明策略等。它的数学逻辑对待验证系统和系统性质进行形式化描述（建模），然理进行一步一步证明，在证明的过程中往往会出现大量新的子我们可能会需要证明大量的中间引理对这些子目标单独证明。

交互模式,命令行,终端

Laplace 变换在 Coq 中的形式化及其在飞控系统验证中的应用oq 交互式集成开发环境 Coq 系统一般有两种方法，标准的方法是在操作系统的命令行终端中启动 Coq 系统的 linux 系统的终端中，或者在 cygwin 终端中，可以使用 coqto之后可以输入 Coq 命令，如图 2.1，命令“Require Import Reals”将会装载用“.”结束，回车提交给系统执行。在操作全部执行完毕之后用命令“Qu

环境,子目标

图 2.2 CoqIde 环境明方法，定理证明的过程是反向的，就是从目标出发，寻找到达目标的择某一个命令作用于它。Coq 系统会检查使用该命令之后所需那么该命令应用成功并且将待证目标分解为一个或多个子目标的信息。对于分解出来的每一个子目标采用相同的方式进行证。CoqIde 右边子窗口中显示 No more subgoals，表示引理已经还得再加一条命令 Qed，它的作用是正式结束一个证明，并且便在后续的证明中调用。在证明的过程中，我们会发现并不是所以这对用户的要求很高[5]。明过程中经常使用到的命令：. 把全称量词中的变量和蕴含式的左端都转变成子目标的条件。qIde 环境的右边窗口中，横线上方是子目标中的条件部分，下方ption. 当待证目标已经出现在假设条件当中，直接使用假设条件

【相似文献】