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