拉普拉斯变换微积分性质在HOL4中的形式化  

Formalization of Laplace Transform Calculus in HOL4

作　　者：赵刚[1] 赵春娜[1] 关永[1] 吕兴利 李晓娟[1] 施智平[1] 王瑞[1] 叶世伟[2] 

机构地区：[1]首都师范大学信息工程学院高可靠嵌入式系统技术北京市工程研究中心,北京100048 [2]中国科学院研究生院信息科学与工程学院,北京100049

出　　处：《小型微型计算机系统》2014年第9期2177-2181,共5页Journal of Chinese Computer Systems

基　　金：国际科技合作计划项目(2010DFB10930;2011DFG13000)资助;国家自然科学基金项目(60873006;61070049;61170304;61104035;61174145;61201378)资助;北京市自然科学基金项目;北京市优秀人才项目(4122017;KZ201210028036;KM201010028021;2012D005016000011)资助

摘　　要：拉普拉斯变换是系统时域频域分析转换的基本工具,基于拉普拉斯变换的数值计算广泛用于信号传输的评估和重要安全系统的分析等,但是其存在计算不精确等问题.高阶逻辑定理证明是验证系统的一种严密的形式化方法.本文在高阶逻辑证明工具HOL4中使用积分、微分、超越函数、复数等定理建立了拉普拉斯变换形式化模型,并且对拉普拉斯变换的线性性质、微分性质、积分性质、频移性质进行了逻辑推理证明.最后通过对电机传递函数的形式化验证说明拉普拉斯变换形式化的有效性和正确性.Laplace transform is a basic tool for the system analysis in time domain and frequency domain conversion, is widely used for evaluating transfer of signalsand analyzing safety-critical systems, but these techniques cannot guarantee accurate analysis. The higherorder-logic theorem proving is one of the rigorous formal methods. This paper established a formal model of the Laplace transform in the higher-order logic proof tool HOL4 use integral, differential, Transcendental functions and complex theories. In addition, the correctness of some properties of Laplace transformare proved, for instance, linearity, differentiation, integration, and frequency shifting in time domain. In order to demonstrate the practical effectiveness and correctnessof this formalization,we use it to formally verify the transfer function of the motor.

关 键 词：拉普拉斯变换 形式化验证 定理证明 HOL4 微积分性质 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]