欢迎访问一起赢论文辅导网
本站动态
联系我们

手机:15327302358
邮箱:peter.lyz@163.com

Q Q:
910330594  
微信paperwinner
工作时间:9:00-24:00

机械论文
当前位置:首页 > 机械论文
函数极限的高阶逻辑形式化建模与验证
来源:一起赢论文网     日期:2020-12-21     浏览数:61     【 字体:

 第43 第11期计 算机 学 报Vol .43No.1 12020年1 1月CHINESEJOURNALOFCOMPUTERSNov.2〇2〇函数极限的高阶逻辑形式化建模与验证赵春娜赵 刚( 云南大学信息学院 昆明 650500)摘 要 在高阶逻辑定理证明器中研究了函数无穷远处极限的形式化建模和验证, 包括函数无穷远处极限定义的形式化模型, 函数极限相关性质的建模与验证, 有唯一性、 保不等式性、 绝对值函数在无穷远处的极限、 极限等价性、 常函数极限等. 函数无穷远处极限的高阶逻辑定义是利用拓扑极限方式定义的, 并在实数域内利用集合关系等验证定理. 根据集合有序关系定理验证了唯一性. 利用差值和绝对值的高阶逻辑性质验证极限为零的属性. 变S与常数之和与积的极限高阶逻辑定理也通过已验证定理和高阶逻辑策略验证了. 建立了函数极限四则运算的高阶逻辑模型, 并验证了函数极限加法、函数极限减法、 函数极限乘法、函数极限与常数乘法、 函数极限除法的高阶逻辑定理. 也建立了函数积分极限的高阶逻辑形式化模型, 验证了函数积分极限上限绝对值定理、 函数积分极限上限可加定理、函数积分极限上限可乘定理. 在此基础上, 建立了拉普拉斯变换卷积定理的高阶逻辑形式化建模与验证. 最后, 对电阻-电感电路中的电流进行了高阶逻辑形式化建模与验证. 建立了单位阶跃信号和电路中电流的高阶逻辑形式化定义, 并验证了其正确性. 该实例验证表明了函数极限和相关性质的高阶逻辑形式化模型的正确性, 为后续控制系统的形式化分析奠定了良好的基础.关键词 函数极限; 高阶逻辑; 形式化验证; 定理证明; 卷积中图法分类号TP18DOI号10.11897/SP. J.1016. 2020. 02119FormalModelingandVerificationofFunctionLimitinHigher-OrderLogicZHAOChun-NaZHAOGang( School ofInformat ionSci enceandEngineering*YunnanUniversi ty■. Kunming650500)AbstractFuncti onlimi tofi nfi ni tyisstudiedinhigherorderl ogictheoremproveri nthispaper.Formalmodeli ngandverificati onoffuncti onli mitarecreatedi nhigherorderl ogic.Higherorderl ogicmodeloffunctionli mitplaysasigni ficantrolei ntheformal izati onoffractionalordersystems.Firstl y,basedonhigherorderlogicmodel sofsetandnumber,formalmodeloffunctionli mitdefi nitionanditsrelatedproperti esareproposedi nthi spaper.Theseattri butesi ncl udethebasicnatureoffunctionli mit—uniqueness,i nequalitypreservi ngproperty,theabsol uteval uefunctionlimitwhensol vingitsposi ti veinfi nityli mi t ,l i mitequi valence,constantfunctionl imit ,etc.Higherorderl ogicdefi niti onoffunctionli mitisdefi nedbytopol ogicalli mitway.Thenhigherorderlogictheoremisverifiedbasedonsetsandrel ati onsi ntherealdomain.Theuniquenesstheoremisval i datedonaccountofthesetstheorderlyrelationstheorem.Thei nequal i typreservi ngpropertyisverifiedthroughthehigherorderlogicvali dati onstrategy.Thezeroli mittheoremistestedbyhigherorderl ogicpropertiesofdi fferenceandabsol uteval ue.Thel i mi tequi val enceandconstantfunctionlimi ttheoremsareverifiedinhigherorderlogic.Theli mitofthesumofvariabl eandconstantandthel imi toftheproductofvariableandconstantal soareval idatedbasedonthehigherorderlogi cval i dationstrategyandtheverifiedtheorems.Higherorderlogicmodelofarithmeticoffunctionli mitisal soestablishedi nhigherorderlogictheoremprover.Andsomerelated收稿日期:2019-1M6 ; 在线发布日期: 2020-05-1 8. 本课题得到国家自然科学基金( 61862062,61 1 04035 ) 资助. 赵春擲, 博士? 教授, 主要研究领域为高阶逻辑形式化验证、 分数阶系统. E-mai l :chUnnazha〇@1 63. com. 赵 刚, 硕士, 主要研究方向为髙阶逻辑形式化验证.21 20计 算机 学 报2020年theoremsareveri fi ed.Thefuncti onli mitadditi onhigherorderl ogicaxi omi sval i datedonthebasisofhigherorderl ogicmodel offunctionaddition.Thefuncti onlimitsubtracti onhigherorderl ogi cproposi ti oni sveri fi edonthegroundsofhigherorderlogi cmodeloffuncti onsubtraction.Thefuncti onl i mi tmultiplicati onhigherorderl ogictheoremisvalidatedi nthelightofhigherorderlogicmodeloffunctionmul tiplication.Thenhigherorderl ogictheoremsofmul tiplicati onoffunctionl i mitandconstantsandfuncti onli mi tdivi si onareverifi edi nhigherorderlogictheoremproveraccordi ngtotheverifiedtheoremsandsomevalidationstrategies.Thehigherorderl ogicformalmodeli ngandverificationoffuncti oni ntegrallimitisal soproposedinthispaper.Theupperl imi tabsol uteval ueoffunctionintegrall i mittheoremi sveri fi edonthegroundsofsomehigherorderlogicattri butesoffunctionl imitandabsol uteval ue.Theupperl imitadditiontheoremandupperli mitmultiplicati ontheoremoffuncti oni ntegrall i mitisverifiedonthegroundsofsomehigherorderlogi cval i dati onstrategi es.Onthesegrounds,formalmodel i ngandveri fi cati onofLaplacetransformati onconvol uti ontheoremareestablishedinhigherorderl ogictheoremprover.Lastbutnotleast ,formalmodelingandverificati onofthecurrenti nResistor-i nductorcircuithasbeendiscussedasani nstance.Thehigherorderlogi cformalmodelsofuni tstepsignalandcurrenti nthecircuitareproposedbasedontheverifieddefi nitionsi nhigherorderlogictheoremprover.Thecurrentiscorrectandcompl etebytheformalveri fication.Resultsshowthatthecorrectnessofhigherorderl ogi cformalmodel soffuncti onl imi tandtherelatedproperti es.Itl aysagoodfoundationforthefol low-upformalanalysisofcontrolsystems.Keywordsfuncti onl imi t;higherorderlogic;formalveri ficati on;theoremprovi ng;convol utioni 引 言人工智能一直是科技界的一个努力方向, 能够与人类互动的机器人更是人们研究的热点之一.201 5 年7月, 德国大众工厂发生“机器人杀人”事件.提高机器人的可靠性和安全性是机器人应用的至关重要的问题. 机器人系统的可靠性主要依赖于其控制系统. 形式化方法是基于数学方法描述目标系统属性的一种技术, 它提供了更完备的验证结果, 为交互式机器人的安全验证提供了坚实的基础. 髙阶逻辑定理证明方法是形式化方法中一种严谨的验证方法. 在高阶逻辑定理证明方法中, 机器人核心控制系统的验证需要很多定理库的支持, 其中拉普拉斯变换的形式化是一个重要的内容. 拉普拉斯变换的形式化是以函数极限和相关性质的高阶逻辑形式化为基础的.函数极限是数学中的基本概念之一, 也是拉普拉斯变换等的理论基础, 本文在高阶逻辑定理证明器中研究了函数正无穷大时极限及相关性质的形式化建模和验证, 为控制系统的高阶逻辑验证提供基础理论. 第2 节介绍高阶逻辑定理证明器; 第3 节建立函数正无穷大时极限的高阶逻辑模型; 第4 节对函数极限的基本性质、 四则运算和函数积分极限的一些性质进行形式化建模和验证; 第5 节对拉普拉斯变换卷积定理建立高阶逻辑形式化模型; 第6 节应用本文的内容对电阻-电感电路( 简称RL电路)中的电流进行高阶逻辑形式化建模与验证.2高阶逻辑定理证明器定理证明是形式化方法的一种, 它是一种用数学逻辑公式来表达系统及其属性的技术, 通过对现实中的物理模型提取属性性质转换为数学模型, 再由数学模型转换为逻辑模型, 并在相关定理证明器中进行描述, 从而得到一个形式化系统, 找到某属性的一个证明过程. 定理证明是一种交互式分析技术.它的分析原理是为系统的需求规范和设计实现建立逻辑模型, 然后通过形式化定理验证两者的关系. 如果该定理通过证明是正确的, 则说明实现和需求之间是等价的或是蕴含的. 定理证明克服了等价性验证需要建立标准模型和模型检测处理复杂系统会产生空间爆炸的约束的问题. 由于定理证明器可以表达所有可以逻辑化的东西, 它已用于多个领域的可靠性分析, 如应用高阶逻辑来验证操作系统的安全需求[S赵春娜等: 函数极限的高阶逻辑形式化建模与验证 212111 期文献[2]用高阶逻辑表达线性时态逻辑和区间时态逻辑, 并以实例说明它在硬件设计验证中的应用;应用定理证明也可以来验证多机器人路径规划的安全性 文献[4] 在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型等等. 定理证明虽然可以表达所有可逻辑化的系统, 但是证明定理时需要人工引导, 于是要求定理证明器的使用者熟悉逻辑推理并且拥有一定的推理经验, 这是定理证明难以大众化的原因. 目前, 定理证明主要应用于一些系统关键性质的分析, 在特殊领域里定理证明发挥了巨大优势. 定理证明技术逐渐成为形式化验证技术的重点研究方向, 在研究和应用上都拥有巨大的发展潜力?定理证明本质是, 基于系统的公理及推导规则来为定理寻找证明[5].当演绎推理和数学定理的手工推导证明, 变化成为符号演算的过程技术, 并且可以在计算机上自动进行时, 定理证明就成为当今软件工程领域中一种非常重要的形式验证技术[6], 即定理证明系统. 在运用定理证明的方法进行系统设计验证时, 辅助手工推导的计算机程序被称为机械定理证明器, 它和自动定理证明器组成了自动化程度不同的定理证明器. 现在, 具有各种特点的定理证明系统已成为教育、学术及工业界的有力工具. 这些定理证明系统拥有各种不同的特性, 主要系统有ACL2、Coq、 Lego、Isabel le、 HOL和PVS等?ACL2是由早期用于软件验证的定理证明器Boyer-Moore发展来的, ACL2 从设计上支持基于归纳逻辑理论的自动推理, 可应用于软件或硬件系统的验证.ACL2定理证明器的核心是基于项重写系统. Coq支持数学断言的表达式, 机械化地对这些断言执行检查, 辅助寻找正式证明, 并从其形式化描述的构造性证明中提取出可验证的程序. Coq 基于归纳构造演算, 是构造演算的一种衍生理论.HOL( Higher-〇rderLogi c)是定理证明中的高阶逻辑定理证明器, 由Gordon于20世纪80 年代中期在英国剑桥大学创建的高阶逻辑系统[7 8], 其主要特点是通过ML( MetaLanguage 是一个通用的函数式编程语言) 语言实现高度的可编程性. 本文采用的版本是HOL4, 该工具是利用缜密的数学逻辑来实现工业验证的精确性. ML是一种强类型函数程序设计语言, 是比较经典的函数式语言, 其所有对象的类型都必须在编译的时候静态分析决定.ML提供的类型有单元( uni t) 、布尔型( bool) 、整型(i nt)、字符串型( stri ng) 、 实数( real) 、元组(tuple)、记录( record) 和列表( list) .ML还支持模式匹配、 意外处理、类型引用、多态性以及递归数据结构. 它拥有自然的语法和较少的基本概念, 其理论基础是A演算, 语言实现严谨、 高效且易于理解, 用户可以容易写出清晰可靠的程序. 大多数著名的推理系统都是用ML语言编写的. ML语言作为一种函数式编程语言, 减少了指针的使用, 并提供了灵活的表达方式, 有助于管理复杂的对象. ML编译器循环地进行“输入-求值-输出”, 用户标准的操作方式是一条一条地输人ML表达式或者声明, 让ML编译器去处理. ML编译器处理的过程包括类型检査、 编译、 执行. ML家族有好几种语言, 主要的两种语言是Caml 和标准ML, 标准ML语言被简称为SML, 或者直接称为ML.ML语言结合了函数式编程语言和命令式编程语言的特点, 这是它得以广泛应用的重要原因.在定理证明器HOL4中进行形式化证明时, 如要使用定理库里相关的定义和定理, 需要先用load和open语句加载并打开相应的定理库. HOL4 有非常丰富的定理库, 并且由于其庞大的用户基础, 定理库会越来越丰富. 随着HOL4 定理库越来越完善, 其应用也越来越广泛. 加拿大Concordia大学的Si ddique 等人在高阶逻辑定理证明器HOL中验证了分数阶微积分RL定义[9]和Gamma函数[1 "];Liu等人在髙阶逻辑定理证明器HOL中验证了马尔科夫链[1 1], 为系统的状态验证提供基础. Kumar 等人利用HOL分析了DNA中的纳米生物规模的化学信息处理动态D2], 开发利用全息理解分子尺度生物化学计算行为的新形式. Ahmed 等人在HOL中对可靠性框图进行了形式化验证[1 3], 对串并联、 平行、嵌套等建立了形式化模型, 并验证了云计算中心的一个通用的虚拟数据的可靠性. 巴基斯坦的Sardar等人对于分布式动态热管理系统, 应用高阶逻辑方法验证系统的性能和时间属性[M], 包括热性能、 温度范围、 达到热稳定性时间等. 文献[1 5]在HOL4中研究了一个双臂机器人的避碰规划算法的高阶逻辑形式化验证, 并根据验证结果改进了算法.本文的研究动机是在分数阶PID( 比例Proporti on、积分Integral、 微分Derivati ve) 控制系统高阶逻辑形式化验证的目标下产生的. 分数阶PID控制系统的高阶逻辑形式化验证, 需要分数阶拉普拉斯变换的相关理论和方法. 分数阶拉普拉斯变换是在拉普2122 计 算机 学 报2020年拉斯变换基础上的拓展, 因此要对拉普拉斯变换基础内容性质定理进行高阶逻辑形式化验证. Wang等人在Coq中通过复变函数的形式化研究了拉普拉斯变换的形式化ns].Taqdees 等人在HOLLight中通过多重微积分来验证拉普拉斯变换的形式化?3. 将拉普拉斯变换拓展到分数阶拉普拉斯变换, 需要用到函数极限的高阶逻辑形式化. Weber在Isabelle/H()L中给出了函数在固定点处极限的定义[1 8]. 还有学者在Isabel l e/HOL和Coq 中给出了函数极限的形式化研究[1 9 21 1], 但仅是函数趋于固定点的极限定义, 没有相关性质验证. 拉普拉斯变换拓展研究需要函数在正无穷大时极限, 及其相关性质属性等. 由于研究团队之前的分数阶微积分定义和性质等验证工作是建立在HOL上的, 因此本文在HOL中建立了函数在正无穷大时极限的定义和性质等定理, 以便后续工作的持续开展. 在高阶逻辑定理证明器HOL中已包括一些基本定理库, 有实数库[2 1:, 超越函数库、 自然数库[22]、 极限库[23]、链表库[ %等, 目前在HOL中不存在函数在正无穷大时极限的高阶逻辑形式. 本文的验证基于首都师范大学团队研发的复数库[23]、gauge积分库 和函数库中的一部分内容.3 函数极限定义的建模与验证函数无穷远处极限: 设函数/:DCl?—R是一个定义在实数上的函数, 并在某个开区间U>A} 上有定义. L是一个给定的实数. 如果对任意的正实数£, 都存在一个正实数X, 使得对任意的实数X, 只要?r>X, 就有| /(:r)—L| 那么就称L是函数/在i趋于正无穷大时的极限, 或简称L为/在正无穷处的极限, 记为li m/(x)=L或/(_ r)—A( x—. r?f?+〇〇) . 反之则称L不是/在x趋于正无穷大时的极限.在HOL中, 首先对实数域函数趋于正无穷的符号“―”进行形式化描述, 给出如下定义:定义1. 函数无穷远处极限定义valtends_real_real=I-\///〇. /—/〇技(/tends/0)(mtopmrl, ¥〉=)定义中(/:real—real ) 为实数域中要取正无穷极限的函数, ( /〇:real ) 则为该函数在正无穷远处的极限值. 而符号“―”则用来表示中缀操作, 它的前项为要取无穷极限的实数域函数, 而它的后项则为该函数在无穷远处所取得的极限值. 因为HOL中其它极限(包括序列极限以及函数在某点上极限) 的定义都使用等价于拓扑极限的方式, 所以在本文中也采用这种定义方式. 在拓扑学中, 网是序列的广义化, 用来统一极限不同的概念和将其广义至任意的拓扑空间. 根据拓扑中网极限的定义, 定义函数在实数域的极限. 式中tends 是网的定义, 后面则表示满足该网的一种条件. mtop为是将度量转换为拓扑的函数,mrl 为实数直线上的度量定义, ¥>=则表示中缀操作, 是一个rea丨—real—bool 的集合运算符, 而这个集合中的所有元素都满足偏序关系, 这里主要用于确定取极限时的方向, 取负无穷时则会用¥2.根据上述对实数域函数在正无穷处取极限的形式化描述定义, 下面则对上述的定义进行形式化证明如下:定理1. 函数无穷远处极限valFUNC_POS=hV/f0. f-*f0<^ye. 0<e^?X.Vx. o: >&. X=>abs(/x一/OXe该定理等价符号 的左边部分为实数域函数无穷极限的形式化定义, 右边部分为实数域函数在正无穷处极限的文字定义. 在这里, 利用HOL的高阶逻辑对其进行形式化等价性证明.证明. 首先将符号“―”进行重写, 用定义进行替换, 得到(/tends /0) ( mtopmrl, ¥>=) , 然后通过度量拓扑中极限的特征定理MTOP_TENDS对目标进行重写. 可将(/tends/OKmtop¥>=)替换成一个类似等价符号右边的形式, 因为该定理就是将度量拓扑的定义展开, 并证明了集合满足某种关系, 这里即为偏序关系. 接着将实数域中的特殊函数类型及极限值类型用度量拓扑中的任意类型进行替换即可.对于上面的符号¥>=在集合域中满足有向集的关系, 这里将其以定理的形式给出证明, 以方便后面使用. 其高阶逻辑形式化证明如下:定理2. 集合有序关系valDORDER_RNGE=I-dorder¥>=证明. dorder 为HOL系统中有向集合的定义. 在数学中, 有向集合(也叫有向预序或过滤集合)是一个具有序关系 ( 自反及传递之二元关系〇的非空集合A, 而且每一对元素都会有个上界[28],亦即对于A中任意两个元素^ 和6, 存在着A中的一个元素c(不必然不同于a, W, 使得 和赵春娜等: 函数极限的高阶逻辑形式化建模与验证 2123 11 期(有向性). 有向集合是非空全序集合的一般化. 在拓扑中它们用来定义一般化序列的网, 并联合在数学分析中用到的各种极限的概念. 将dorder 定义重写, 并且利用实数在关系¥>=上具有自反性的性质来证明. 会得到目标式子“?&切八7<1£/’, 若要证明《; 既大于:!: 又大于^, 则需要证明W大于I 中较大的一个即可. 因此再增加一个前件用来讨论当x>y时, 以及 时的两种情况. 因此可以证明当工>^时, 取Z为:C 值; 当时, 取Z为^ 值, 两种不同情况下都成立.对于实函数无穷极限取值的高阶逻辑形式化定义有:定义2. 实函数无穷极限值定义valf_lim=I-V/. f_lim该定义的返回值并不是一个定义形式, 而是函数在正无穷远处的极限值, 这个定义将在后续形式化建模函数极限其它性质以及形式化拉普拉斯变换中会使用到. 实际控制系统的验证中还需要实函数在正无穷处取极限时的一些相关性质, 其形式化验证如下.4 函数极限相关性质的建模与验证4.1 基本性质( 1) 唯一性若极限 li m/( x) 存在, 则此极限是唯一的. 其j-*f■-〇形式化定理如下:定理3.唯一性valFUNC_UNIQ=Vxxl—xl八 (xl= x2)证明. 首先根据目标将定义的函数无穷极限的定义进行重写; 其次, 根据HOL中度量拓扑中网的极限唯一性定理MTOP_TENDS_UNIQ进行MATCH证明. 这时, 则需要证明关系集合: ¥>=是一个有向集. 这就是上面已经证明的定理2, 将之前证明的引理DORDER_RNGE进行MATCH接收写入策略.证毕.(2) 保不等式性如果两个函数/, g在正无穷远处有极限, 即l i m/Cr)=L, li mg(x)=M, 并且在给定任意实J—?4-OC+-■〇数e,当:T>e 时,/( 1) >尽(:*: ) , 则有L>M. 其形式化定理如下:定理4. 保不等式性valFUNC_LE=\-\f fglm.f-*-lf\g^-mA( ?X.Vx. j: >X=>/xx)=>Km证明. 首先使用GEN_TAC将目标中的全称量词去掉; 其次需要使用MP_TAC引人一个新的假设条件, 这个假设条件是度量拓扑中网的极限的比较定理NET_LE. 因为这个定理的形式是对任意类型的二元关系集合, 所以还需要使用geq(¥>=:real—real—bool ) 对该定理进行实例化关系类型,则最后使用的策略为:MP_TAC(ISPECgeqNET_LE) . 因为引人的前件是一个已经证明过的定理的实例化, 所以在此不需要进行证明, 可直接引人. 最后先使用tends_real_real 对目标中的函数在正无穷极限的定义进行重写; 然后使用geq和有向集的定理DORDER_RNGE对目标进行重写, 再使用实数的自反性REAL_LE_REFL对目标进行证明, 可得到跟前件的形式相似的目标; 最后使用匹配接收策略MATCH_ACCEPT_TAC可完成证明. 证毕.(3) 极限为零如果函数/在无穷远处存在极限, 并且极限为零, 即 li m/(:〇=0, 则其绝对值函数在无穷远处_r4- c的极限也为零, 即I l i m/(_r)|=0, 反之也成立. 其.r*+形式化定理如下所示:定理5. 极限为零valFUNC_ABS=hV/.(Ax.abs(/j:) )-?0<=>/-?0证明. 首先使用GEN_TAC将目标中的全称量词去掉, 其次使用函数正无穷极限的定理FUNC_POS重写目标, 将会得到函数正无穷极限定义的形式目标. 接着使用BETA_TAC将目标中的A函数去掉, 然后使用任意实数与零之间的差值关系定理REAL_SUB_RZERO及任意实数的绝对值的绝对值与其绝对值相等的定理:ABS_ABS对目标进行重写即可证明完成.证毕.(4) 极限等价性若函数/在正无穷远处存在极限, 则该函数在正无穷远处的极限值为其在正无穷远处的取值.定理6. 极限等价性valLIM_FUNC_EQ=h\/g( f_li mf=l)证明. 该定理即是证明了之前定义的f_li m的正确性, 即当函数/在正无穷远处存在极限, 则2124 计 算机 学 报 2020年可推出f_li m/的值即是该函数的极限值. 首先将目标中的全称量词去掉并将f_li m的定义进行重写, 因为f_lim定义中使用了选择操作符@, 所以在证明的时候需要使用消除选择操作符的策略:SELECT_ELIM_TAC, 将选择操作符@变为存在(?) 和任意( V) 两个形式的目标. 此时可使用策略CONJ_TAC将合取形式的目标分成两个子目标的形式. 两个子目标的前件都为函数/的正无穷处极限为“第一个子目标为证明存在一个实数x使得函数/的正无穷处的极限为该实数, 而第二个子目标则为对任意实数:r 若函数/的极限为I, 则x与Z相等. 第一个子目标很好证明, 只需要将用/ 代替X, 然后使用前件重写目标即可. 在第二个子目标中会发现,函数/有两个正无穷极限值x和“然后需要证明z和/ 相等, 这与之前证明的函数在正无穷处的极限唯一性定理一致, 因此可以直接用自动证明策略PR〇VE_TAC[FUNC_UNIQ](并将极限唯一性定理代入) 可完成证明.证毕.(5) 常函数极限若函数/为常函数, 则其在正无穷远处的极限值为函数本身.定理7. 常函数极限valFUNC_CONST=hV々. (Ax. 々)—是.证明. 首先将目标中的全称量词去除, 然后用函数无穷极限的定理:FUNC_POS对目标进行重写, 再分别使用定理:REAL_SUB_REFL和ABS_0将目标中的“abs U—变为“0”. 此时的目标为:“Ve.0<e=>?X.Vx. x>0<e,,, 发现目标中的前件和结论都为“〇<e”, 那么就需要去除全称量词, 并使用策略DISCH_TAC将目标中的前件放在条件队列中, 最后用自动重写策略ASM_REWRITE_TAC□即可完成证明.证毕.(6) 变量与常数之和的极限若函数/在正无穷远处存在极限, 即li m/( x)=j-*4-xL, 则有任意常数a使得下式成立:l im/( a+x)=L.其形式化描述:定理8. 变量与常数之和的极限valLIM_FUNC_LAM_ADD=I-V//+(7) 变量与常数之积的极限若函数/在正无穷远处存在极限, 8卩lim/Or)=L, 则有任意常数a>0使得下式成立:l im/( a*x)=L.其形式化描述:定理9. 变量与常数之积的极限valLIM_FUNC_LAM_MUL=I-V//a. a ̄>0A(Af./< )-*?/ (Af ./(a*这两个定理通过消去全称量词, 并用函数无穷极限的定理对目标重写即可证明.4. 2 函数极限四则运算的建模与验证极限形式化语言只能证明极限, 不能求极限. 对于简单函数的极限问题, 可以使用比较容易的证明方法证明其极限存在或不存在, 但对于一些形式比较复杂的函数, 就不太容易证明. 因此, 函数正无穷极限的运算法则的形式化十分必要, 它对于证明复杂函数无穷极限的问题至关重要. 在上面正无穷极限的形式化模型的基础上, 这里将对正无穷极限的运算法则进行形式化建模及验证.在对函数在正无穷远处的极限的运算法则进行形式化描述和证明中, 形式化过程包括两种形式化内容.一种是在推出结果的形式中不带有 而是使用“―”的形式化, 这是最基本的形式化证明; 另外一种则是基于上一种证明的进一层, 是在推导结果中使用“=”和Uim的形式, 而这种形式是在后面函数极限的应用形式化建模中所需要的. 如若跳过第一层形式的证明, 直接到第二层, 则会有很多证明代码的冗余. 因此, 为了能够更加有效地组织这些证明逻辑、过程以及代码形式, 最终抽出第一层形成单独的定理形式, 这样在后续的证明过程中可减少不必要的重复证明.(1) 函数极限加法若函数/和g 在正无穷远处都存在极限, 即lim/(x)=L, 则有函数/和g的和在正无穷处存在极限并且:lim(/(x) +^(x) )=L+M.其形式化描述:定理10. 函数加法valFUNC_ADD=I"^fslt+gi l+m').证明. 首先将全称量词去掉, 然后将tendS_real_real 的定义进行重写, 去掉符号 根据目标的形式使用MATCH策略匹配定理NET_ADD,目标会变成“dorder¥>=”, 此时需要使用前面证赵春娜等: 函数极限的高阶逻辑形式化建模与验证 21251 1期明过的定理2:DORDER_RNGE来说明“¥>=”满足有向集关系, 用MATCH接收策略将该定理代人即可.证毕.定理11. 函数极限加法valLIM_FUNC_ADD=I-V/g/Ag ̄>-m^(. i_li m(. Xx. fx+gx)=Z +?i).证明. 由于极限的运算是用f_Hm定义写的,所以首先去除全称量词及重写Ui m的定义, 由于f_li m定义中使用了选择操作运算符@, 因此证明需要使用策略SELECT_ELIM_TAC, 这样就可以将目标转换为两个目标的合取形式,一个是证明存在性,一个证明等价性. 使用CONJ_TAC将目标中的合取形式变为两个子目标. 第一个子目标, 是证明两个函数的和在无穷远处存在极限, 根据前件中的条件函数/和g在无穷远处的极限分别为Z 和 因此只需要证明两个函数的和在正无穷远处的极限值为Z+m即可. 那么就需要MATCH_MP_TAC对上面已经证明完的定理FUNC_ADD进行匹配, 然后重写目标即可. 第二个子目标, 去掉全称量词后发现它的目标形式与之前证明函数极限的唯一性定理FUNC_UNIQ很相似? 此时需要使用MATCH策略匹配该定理, 则目标变成了“?乂xAi—G+m)”的形式. 先证明目标合取式的第一部分, 即证明存在性, 显然存在的V应该为(Ai. /x+gJ: ) ,所以根据前件的条件可以消去目标合取式的第一部分; 而目标的第二部分与上面第一层证明极限和的形式一样, 所以使用MATCH策略匹配定理FUNCLADD即可.证毕.(2) 函数极限减法若函数/和g 在正无穷远处都存在极限, 即l im/(x)=L, l i m尽(_ r)=M, 则有函数/和莒 的X-*+=C+CC差在正无穷处存在极限并且:lim+oc其形式化描述:定理12. 函数减法valFUNC_SUB=Nfglm. f一lt—g该定理的证明方法与定理10是类似的.定理13. 函数极限减法valLIM_FUNC_SUB=l—m) .该定理的证明方法与定理11 是类似的.(3) 函数极限乘法若函数/和g在正无穷远处都存在极限, 即li m/(x)=L, l img(x)=M, 则有函数/和g?的X-*积在正无穷处存在极限并且:l i m(/(x)X^(x) )=LXM.J-*+OO其形式化描述:定理14. 函数乘法valFUNC_MUL=fglm.f—lt* gtl—U*m).定理IS. 函数极限乘法valLIM_FUNC_MUL=卜V/gZm. /—Z Ag—m=>(f_lim(Ax./x*gx)=l*m) .证明. 通过使用策略SELECT_ELIM_TAC,可以将目标转换为两个目标的合取形式,一个是证明存在性,一个证明等价性. 使用CONJ_TAC将目标中的合取形式变为两个子目标. 第一个子目标, 是证明两个函数的乘积在无穷远处存在极限. 根据前件中的条件函数/和g在无穷远处的极限分别为Z和?n, 因此只需要证明两个函数的和在正无穷远处的极限值为mXZ 即可. 那么就需要MATCH_MP_TAC对上面已经证明完的定理FUNC_MUL进行匹配, 然后重写目标即可. 第二个子目标, 需要使用MATCH策略匹配该定理, 则目标变成了“?—x八x'—的形式, 先证明目标合取式的第一部分, 证明存在性, 显然存在的x'应该为(Aor. /i*gx) , 所以根据前件的条件可以消去目标合取式的第一部分; 目标的第二部分使用MATCH策略匹配定理FUNC_MUL即可证明.证毕.( 4) 函数极限与常数乘法若函数/在正无穷远处存在极限, 即lim/U)=L, 则有任意常数a, 使得a与/的乘积在正无穷处存在极限并且:limaX/( x)=aXL.其形式化描述:定理16. 函数极限与常数乘法valLIM_FUNC_CMUL=hV/1a. f^ ̄l=>(f_lim(Ax. a*fx)=a*V):thm.证明.由于该目标的形式与上一个定理: 函数极限的乘法运算很相似, 因此可以借助定理: LIM_2126 计 算机 学 报 2020年FUNC_MUL来进行证明. 那么就需要将目标的形式变成与所用定理一样的形式, 在定理LIM_FUNC_MUL中, 是两个函数乘积的形式, 而在证明目标中则是一个常数与一个函数的乘积形式, 因此需要使用定位策略及添加lambda 函数的方法将常数改写为常函数的形式: CONV_TAC( (LAND_CONV〇EXACT—CONV)[X_BETA_CONV(—‘x:real,--)(-‘a:real’--)]) . 应用到要证明的定理中, 则左侧即可表示为, 对目标中的常数a添加一个自变量为? r的lambda 函数. 此时的目标形式为:f_l im(Ax.(Ax. a)〇: )=?*/? 此时便可以使用MATCH策略匹配定理LIM_FUNC_MUL, 然后使用常函数极限定理FUNC_CONST进行重写, 即可完成证明.证毕.(5) 函数极限除法若函数/和g在正无穷远处都存在极限, 即lif/(x)=L, liijig(_r)=M, 并且M尹0, 则有函k/和g 的商i正无穷处存在极限并且:K(fU)/gU))=L/M.其形式i描述:定理17. 函数极限除法valFUNC_DIV=Nfglhg—miXt.ft/g证明. 首先将全称量词去掉, 然后将tendS_reaLreal 的定义进行重写, 去掉符号“—”, 根据目标的形式使用MATCH策略匹配定理NET_DIV, 目标会变成“dorder¥>=”, 此时需要使用前面证明过的定理2: D0RDER_RNGE来说明“¥>=”满足有向集关系, 即用MATCH接收策略将该定理代人即可.证毕.4. 3 函数积分极限的高阶逻辑形式化建模与验证(1) 正无穷函数积分上限取绝对值的建模与验证若函数/在以任意常数a 为积分下限存在正无穷积分L, 即li mfV(x)=L, 则有该函数在以^j-*+<?Ja为积分下限, 积分上限为取正无穷变量的绝对值的极限为L, 即p1lim/(x)=L.x-^+〇〇Ja该定理表示, 函数积分上限取极限时, 与其上限的绝对值取极限的结果一样. 其形式化描述如下:定理18. 函数积分极限上限绝对值定理valLIM_FUNC_BOUND_ABS=1-V/a/>.(A^ .integral( a, i)(A? .i ntegral(a,absf)证明. 首先用极限定理FUNC_POS重写, 然后使用等价策略( EQ_TAC)将等价性证明变换成两个蕴含式证明. 第一个子目标的蕴含式证明: 由于目标中存在两个蕴含式且它们之间的关系为蕴含关系, 每个蕴含式中都有一个〇所以先将两个e实例化为同一个e, 主要使用SPEC, 即MP_TAC〇SPEC“e: rear. 目标式中有存在量词的证明, 实际上在0<? 时,abs. 所以, 两个蕴含式中的X, 即存在量词, 可以写成一个? 此时, 目标变为“abs(integral(a, absj: )而前件中有三个条件分别为“工X”,“Vx._ r>& X>abs( i ntegral(a, x)/—/>) <,和“OO”. 从条件2 中可以发现, 其成立的条件为“z>对目标来说, 它的成立条件形式应该为“abs&X”. 所以使用目标中的前件匹配结果, 即可得到目标: abs:r>&X, 经过简单的变换, 根据条件即可完成第一个子目标的证明.第二个子目标的证明思路与第一个子目标很相似, 但第二个子目标中的蕴含式与第一个子目标中的蕴含式刚好相反, 条件和结果进行了调换, 所以在证明到目标形式为“abs(i ntegral( a, :c)/_p) <e”的时候, 有所不同. 此时的前件条件中有“x>&X”,MVo:. x>&- X=>abs (integral( a,absx)f ̄p') <ien和“0<,. 此时条件2中的目标中有“abs的形式, 而条件中的前件却为 并没有绝对值abs 的形式. 而目标中也没有绝对值abs 的使用. 为了能使用前件中第二个条件, 需要将目标的形式改写为与前件第二个条件的目标相似的形式. 即用absi代替目标中的X, 将目标变为“abs(i ntegralU,absz)/_/>) <,. 而前件中第一个条件为“x>&X”,: c 为实数, 而X为自然数, 因此会有“&X”的形式, 是将自然数取实数的表示方法.由此可知, 若一个实数大于等于一个自然数, 那么这个实数与其绝对值是相等的.证明步骤如下:首先证明“〇<x”, 需要使用实数小于等于的传递定理REAL_LE_TRANS, 找到一个处于0和x的中间值, 那就是自然数兄于是分别证明“和“02X”, 第一个目标用重写即可( 前件条件中有该目标的形式) . 第二个目标使用定理ZER〇_LESS_EQ(表示自然数不小于零)即可证明.其次证明“x=absI”, 使用定理ABS_REFL(实数绝对值与其本身相等成立的条件, 即该实数不小于零) , 这就需要用到前面证明的目标“〇<x”, 然赵春娜等: 函数极限的高阶逻辑形式化建模与验证 212711期后将条件进行重写即可完成.至此已经构造出了需要的目标形式“abs(integral( a, abst)/—夕) 0”, 然后使用条件匹配策略FIRST_ASSUMHO_MATCH_MP_TAC, 可得到目标为 将前件中一样的条件进行重写即可完成证明.证毕.( 2) 正无穷函数积分上限与常数之和的建模与验证若函数/在以任意常数a 为积分下限存在正无穷积分L, 即丨 i mf/(:r)=L, 则有该函数在以《为积分下限, 积分上限为取正无穷变量与任意常数6的和的极限为L, 即r6+xlim/(x)=L.x-*+〇〇Ja该定理表示, 函数积分上限取极限时, 与其上限与一常数的和取极限的结果一样. 形式化描述如下:定理19. 函数积分极限上限可加定理valLIM_FUNC_B〇UND_ADD=apb.(Xt.i ntegral (a,t)(Ai.i ntegral(a,b+t)f)^ ̄p证明. 首先将极限的定理进行重写, 然后使用等价策略EQ_TAC进行目标重写, 将等价性证明变换成为两个蕴含式的证明. 第一个子目标的蕴含式证明: 由于目标中存在两个蕴含式且它们之间的关系为蕴含关系, 主要使用SPEC. 目标式中有存在量词的证明, 但是目标中的两个X则不相同, 前件中的存在量词用X表示, 则目标中的X应该用clg( &( X:num)—6:real) 表示(clg表上取整) . 此时, 目标变为“Vxj>&dg( &X—abs ( CU.i ntegral (a,6+f)/)再将目标中的前件放下去, 则前件中有三个条件分别为&-clg( &- X—b)",uVx. x>&-X=>abs(integral ( a, x)/一/>) <,和“0<,. 从条件2中可以发现, 其成立的条件为“x>&X”. 对目标来说, 它的成立的条件形式应该为 所以使用目标中的前件匹配结果, 即可得到目标: 6+x>&X, 经过简单的变换, 主要会用到上取整定理: LE_NUM_CEILING( VuS&clgz), 根据条件即可完成第一个子目标的证明. 第二个子目标的证明: 由于第二个子目标的形式跟第一个子目标很相似, 所以证明的思路也基本一致. 但是第二个子目标中的蕴含式与第一个子目标中的蕴含式刚好相反, 条件和结果进行了调换, 所以在证明到目标形式为“abs(i ntegralU, x)/—/0<e”的时候, 有所不同. 此时的前件条件中有abs(i ntegral ( a, absx)/—p) <,和“OO”. 此时条件2 中的目标中有“6+x”的形式, 而条件中的前件却为“_ r>&X”, 并没有和的形式. 而目标中也没有和的使用. 为了能使用前件中第二个条件, 需要将目标的形式改写为与前件第二个条件的目标相似的形式. 即用6+(x—6) 代替目标中的工, 将目标变为“abs(i ntegral(a, 6 +U-W)而前件中第一个条件为“x>&clg( &X+6)”, x为实数, 而X为自然数, 因此会有“& 的形式, 是将自然数取实数的表示方法, 又使用实数上取整clg, 所以又变成自然数了, 然后再用符号“&”即可变为实数的形式. 由于“:c=6 +( z_6)”的证明比较简单, 这里就不赘述了. 目标替换完成后, 使用条件匹配策略HRST_ASSUMH0_MATCH_MP_TAC, 可得到目标为“〇:_6>由于前件的第一个条件中有“&X+6”的形式, 所以将目标转换为 然后使用MATCH匹配实数小于等于的传递定理REAL_LE_TRANS, 则处于目标中间的一个实数为“&dg( &JC+6)”, 使得目#**&-X+6<&-clg( &- X+6)A&-clg(&-X+6) <xw成立. 最后使用上取整定理LE_NUM_CEILING,并将目标进行重写, 即可完成证明.证毕.(3) 正无穷函数积分上限与非负常数之积的建模与验证若函数/在以任意常数a 为积分下限存在正无穷积分L, 即lim|"/(x)=L, 则有该函数在以〇X-*+Ja为积分下限, 积分上限为取正无穷变量与任意非负常数6的积的极限为L, 即nb*xl im/(x)=L..rJa该定理表示, 函数积分上限取极限时, 与其上限与任一非负常数的乘积取极限的结果一样. 形式化描述如下:定理20. 函数积分极限上限可乘定理valLIM_FUNC_B〇UND_CMUL=I-V/a/>6.&-〇<6=>( (Ai.i ntegral(a,t)f) ̄*i ntegral (a, 6*t)该定理的证明思路与定理19 的证明思路很相似, 首先将极限的定理进行重写, 然后使用等价策略EQ_TAC进行目标重写, 将等价性证明变换成为两个蕴21 28 计 算机 学 报 2020年含式的证明. 再分别证明两个蕴含式的子目标即可.L_c〇nv〇luti〇n_def证毕.验证了函数极限的上述性质定理后, 则可以证明拉普拉斯变换的性质定理, 为控制系统的高阶逻辑验证提供基础理论支撑.5 拉普拉斯变换卷积定理的建模与验证卷积是一种积分变换的数学方法, 在许多方面得到了广泛应用. 统计学中, 加权的滑动平均是一种卷积. 概率论中, 两个统计独立变量的和的概率密度函数是两个变量的概率密度函数的卷积. 声学中, 回声可以用源声与一个反映各种反射效应的函数的卷积表示. 电子工程与信号处理中, 任一个线性系统的输出都可以通过将输人信号与系统函数做卷积获得. 物理学中, 任何一个线性系统都存在卷积. 高斯变换就是用高斯函数对图像进行卷积.卷积最重要的一种情况, 就是在信号与线性系统或数字信号处理中的卷积定理. 利用该定理, 可以将时间域或空间域中的卷积运算等价为频率域的相乘运算, 从而利用快速算法, 实现有效的计算, 节省运算代价.拉普拉斯变换卷积定理是指, 函数卷积的拉普拉斯变换是函数拉普拉斯变换的乘积. 即一个域中的卷积相当于另一个域中的乘积, 例如时域中的卷积就对应于频域中的乘积.L(/(x)*g(x) )=U/(;c) ) XL(g(x) ),其中, LCLaplace 的简写) 表示的是拉普拉斯变换.拉普拉斯变换的卷积性质不仅能够用来求出某些函数的拉氏逆变换, 而且在线性系统的研究中起着重要作用. 文献[29]中已验证了拉普拉斯变换定义和存在条件.根据卷积定义, 两个函数 C的卷积可用 表示. 拉普拉斯变换的卷积定义如下:=\/(r)g(f-r)dr=[V(r)^( i-r)dr.J—=〇JO根据拉普拉斯变换定义,《<0 时/(f )=0. 则当r<0 或卜f<0 时, 上述定义中的积分值为零, 因此在i <0时, (/*g) (?)=0.下面为在HOL4中对拉普拉斯变换卷积定义的形式化:定义3. 卷积定义hV/_l/_2t.L_convolutionf_lf_2t=integral(0, abst)(Atau. f_ltau*f_2{t一tau)')这里, 假定函数/和g 是分段光滑, 容易证明拉普拉斯变换卷积存在. 实际上,当固定f>〇 时, 以r为自变量的函数r—/(r)g(i—r)同样也是分段光滑的, 而且这样的函数在区间[〇“]上总是可积. 因此, 在 时, 两个分段光滑的函数/和g 的卷积一定存在. 拉普拉斯变换卷积定理t LC/iU)*/2 ⑴]=L( s) GU). 式中, 函数/和g满足拉普拉斯变换的条件, 且则拉普拉斯变换卷积定理在HOL4 中的验证如下:定理21. 卷积定理valL_TRANS_CONVOLUTION=fff-1f_2 t Mc b vu t .L_exists一condi tion/_16w八L_exists一condi tion/一26ze; 八(i <〇=?(/_lt-〇)A(/_2?=0) )=>( lap_trans (Ax. L_convolution/_1f_2x)btv=lap_transf_lbw^lap_trans/_2bw)其中, 函数lap_trans和L—exists_condition是拉普拉斯变换和存在条件的高阶逻辑形式化表示, 详细解释参见文献[29]. 函数lap_trans 和L_exists_condi tion的高阶逻辑形式如下:vallap_trans_def='ifbtw.lap_transfbw=( f_li m(Ai .i ntegral(&? 0, absi){Xt.ft*exp(—(6*t))*cos(w*i)) )?f_lim(Ai.integral(&-0,abst){Xt,—/i*exp(_(6*t) )*sin{ w*£ ) ) ) )valL_exists_condition_def=V/^w. L_preeonditionfbw^彐Me.W. 八&*0<MA&0〇八abs(/"£XM*exp(e*£) 八/contl之在卷积定理中, 当f<〇时, ,u)=/2 u)=〇, 因此在平面 上有?+?5/?-j-ooL(s)Gis)=fx (t)e ̄stdtfz U')e ̄su6u.JoJo从上式可以看出, 第二个积分与f 无关, 所以可以将上式写成:%-jOO广+OQL(5)G( i)=(/1 (t)/2 ( it) e-5U+< >d?)di.JoVJ07赵春娜等: 函数极限的高阶逻辑形式化建模与验证 2129 1 1 期现在可以使用新变量r代替i +M, 则可得到:L(s)G( s)=J"〇(J〇/“"/“r—Hjck.根据定理中的条件, 将上式积分顺序改变, 可以得到:LG)GW=j。e-sr(j 〇/“"/“r-Ock)*.如上式所示, 其内积分为函数的卷积结果. 因此丄[/, ⑴*/2 ⑴]存在, 并且L[/,W*/2 ⑴]=L(s)GCs).对上述定理的证明, 首先需要将拉普拉斯变换的定义以及卷积的定义重写, 并且将等式中复变函数中的实部和虚部分开证明. 本文就以实部的证明进行简要说明,当证明到如下等式:f_li m(A/.integral(0,abstf)(Xtau. f^lraw*i ntegral (Za??abst/+ tau)—toM)*( exp(—{b*z))*cos(t£;*^) ) ) ) )=f_l i m{Xt ,i ntegral ( 0?abst)t*exp(— (6*尤) )*cos(w*i)))*f_l im(Xt .i ntegral ( 0, abst)t*exp(—(6*i) )*cos (w*z) ) )—f_l im{Xt .integral (0,abst)(A尤.—/_1t*exp(—(6*0)*sin(w*^)) )*f_li m (A^ .i ntegral (0,abst)iXt.—f_2t*exp(_Cb*t ) )*sin(w*i) ) ).可使用换元积分性质INTEGRATION_BY_SUBST对等式左边的内积分进行变换, 可将i ntegral(iaw,abstf ̄\ ̄tau){ Xt .f_2( t_tau)*(exp(_ (6*O*cos( w*i) ) ) 变换为i ntegral( 0,abstf)( At.f_2^*(exp(_i b*( i+tau)))*C〇s(u; *G+m?) ) ) ) ? 使用该性质定理就需要证明目标等式中上下限大小比较的问题, 以及左式和右式中上下限使用换元时相等问题. 最重要的是需要证明积分函数存在原函数, 在抽象形式化中, 并不知道在实际进行验证时是对什么样的模型进行验证,也无法确定该模型提取出的原函数的形式, 所以在这里使用定义(L_COS_DIFF) 将原函数写在前件中. 后面在使用该定理验证实际应用时, 可将前件中原函数的定义用实际中的原函数替换, 这样就保证了实际验证的正确性.根据余弦的二倍角公式( COS_ADD) 将C〇S( ?;*(i +tau) )ft(Wcos*^)*cos(w*tau)一si n(w*£)*si n( w*£aw) _ 同时根据指数函数的性质(EXP_ADD) 可将厂 化简为*厂 . 根据积分性质“两函数分别可积, 则函数之差的积分与函数积分之差相等〇NTEGRAL_SUB)”,将等式左边中的内积分分成两个内积分之差的形式. 再将等式左边外层的积分进行分解, 将函数之差的积分写成函数积分之差的形式. 可得fJi mCA/.integral (0, abstf)(Xtau. f_ltau*(exp(—(b^tau) cos(zvintegral (0,abs,)i. Xt. f_2t*(exp(—(6*i) )*cos( xv*i) ) )—integral (0, abstf)(Xtau.— (/_1tau*( exp(— (6*tau) )*sin( xt> *tau) ) ) )*i ntegral(0, abs/)(A艺?一(/一2£*(exp(—(6*r))*si n(w*,) ) ) ) )=f_l im(Ai .integral (0,abs/)t*exp(— (6*?) )*cosCze; *f) ) )*f_li m(Ai .i ntegral ( 0, abst)(Af. /_2t*exp(— (6*^) )*cos( tv*i) ) )—i ntegral( 0,abs艺)t*exp(—(6*i) )*si n {w*^) ))*f_li m(Ai .i ntegral( 0?abst){Xt.—f_2t*exp(—(6*£) )*si n(w*O) ) ?此时, 即可将等式左边的极限写成单个积分极限的形式, 用来对应等式的右边形式. 这里主要会用到引理FUNC_SUB极限减法运算以及引理FUNC_MUL极限乘法运算.6RL电路电流的高阶逻辑形式化建模与验证RL电路, 全称电阻-电感电路, 或称RL滤波器、RL网络, 是最简单的无限脉冲响应电子滤波器. 它由一个电阻器、一个电感元件串联或并联组成, 并由电压源驱动. 本文验证的是RL串联电路.日光灯电路实际上就相当于一个RL电路, 它是由电阻元件和电感元件组成, 这类电路是很多复杂系统中的组成部分.RL电路作为最基本的电子原件的一种组合,在各种电路中使用的非常多. 这里将对RL电路中的电流进行高阶逻辑形式化验证. 验证过程中会用到函数极限和拉普拉斯变换的高阶逻辑模型和性质. 这里将从模型、 需要验证的性质、 形式化验证过程这三方面来描述.2130 计 算机 学 报2020年( 1) 模型本文讨论的RL电路如图1 所示.图1 时域RL电路图中, 激励信号为单位阶跃 根据拉普拉斯变换的卷积定理以及相关性质, 对该电路电流£(?)=去(1—A)进行高阶逻辑验证.验证/'(0的拉普拉斯变换的结果为J?+sL.引理1. 阶跃函数频域表示valL_TRANS_INSTANCE_UF_LEMMA=卜VAfc6w.0<M/\ 0〇Ac<6=>( lap_transikt. u_ft')bw ̄(6/(b*6+w*w)*_(6/( 6*6+zw*te;) ) )) .上面的引理为证明阶跃函数的拉普拉斯变换的上述时域电路图可等效频域电路图, 如图2所示.sL\ R图2 频域RL电路根据图2 所示, 可知图中电流在频域的表达式1应为:I(s)i?+sLE(5) .R+sL为频域电路中的导纳(阻抗的倒数), 可以写成7s ̄( ̄z)电压的拉普拉斯变换(频域表示) : £Xs)=L[m( £)]=丄.s( 2) 需要验证的性质根据拉普拉斯变换的位移性质[29], 若L[/U)]=L( s), 则有L| >'/( f)]=L(s—a), 则可以得到导纳(频域) 的拉氏逆变换为 这个结果可以根据11 0,t<0结果, 即为jL〇(f)]=—, 当《(〇=、时,s11,t>0■L[M(f )]=—.导纳的表示证明:下面是根据上面阶跃函数的引理证明, 可以推理出, 某函数/(即为上述RL电路在时域中的导1纳) 的拉普拉斯变换若为+RL?, 那么该结果可以写成L( s—a) 的形式, 即a为一f, 再根据拉普拉斯变换的位移性质I?[产/(f)]=L( s_a) , 可将其变为 ⑴].证明过程如下所示.引理2. 导纳等价性表示证明1valL_TRANS_INSTANCE_LEMMA=|-VMcbwR_c.Q<MA〇<cAc<b /\ 〇<La拉普拉斯变换进行验证. 则将电流在频域中的表达式进行拉氏逆变换, 及根据卷积定理, 得到结果为t( f)=-7-eL,*u(,t')=[w( r)?-^-e ̄^u ̄T)drLJoL=—ef<,_c)=—(i—gf1)R。_RU八下面将通过高阶逻辑形式化验证这个性质, 由此验证电流结果的正确性.(3) 形式化验证首先在HOL4中建立输人信号单位阶跃响应的高阶逻辑模型.定义4. 单位阶跃信号的形式化定义:valu_f=I-Vf. w_/i=i ft<i0then0elsel :thm(lap_trans{Xt.1/L*exp(—(J?_tr/L)*f))biv=lap_trans(At.1/L) (6(J?_c/L) )zv) .上述的证明为说明导纳(频域)在使用拉普拉斯变换表示时存在两种等价的表示方法, 即使用拉普拉斯变换的位移性质.引理3. 导纳等价性表示证明2valL_TRANS_INSTANCE_ADMIN=I-VMcbivR_ctL.0<MA0<c 八t: <6 八0<L八0<i?_£:=>(lap_trans(Af.l/L)Cb(J?_c/L) )w)=l/L*l/( 6-(-(l?_c /L) ) ) .上述引理证明了, 导纳的另一种表示方法(根据位移性质) , 证明了导纳在上述推导的正确性.引理4. 电流在时域中表达式赵春娜等: 函数极限的高阶逻辑形式化建模与验征 213111 期下面则为证明电流在时域的表达式, 是根据上面导纳拉氏逆变换的结果进行证明的.valL-TRANS一INSTANCE_LEMMA2 =|-VMcbvuR_cL.0<M八0<c八c<6 八0<X八0<CR_c八( abs( (A^.1/L*exp(—(J?_c/L)*t) )M*exp(c*i) )A1/L*exp(—CR_c/L)*r) ) r=0) ) 八( V^.abs( (A^.u_ft)t)<M*exp(c*之) ) 八( V艺? (Az .m_/尤 ) contl£)=>( Iap_transiXt. u_ft )b-w^lap_transikt .l/L)(b(.R_c/L) )vu=lap一trans(An1AR一c*(1—exp(—{R_c/L)*£) ) )buu) .下面是对电流在时域中的表达式结果进行证明, 使用的是积分的方法, 证明的结果与上面使用拉普拉斯变换的卷积定理证明的结果一样, 这同时也说明了拉普拉斯变换卷积定理的形式化证明的正确性和本例中在推理电流在时域中的表达式是正确的.valL_TRANS_INSTANCE_LEMMA3=hVxR_cL.0<x^0<R_c ^0<L^(i ntegral ( 0, 〇■)(Aiaw.1/L*exp(—(R_c/L)*{x ̄tau) ))—l/R_c*(1—exp(—(i^_c/D^x) ) ).7 结 论形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统, 是改善和确保计算系统质量的重要方法, 已广泛应用于软硬件验证中.高阶逻辑形式化验证需要验证者具有专业知识, 并采用必要的策略和手段, 交互式引导系统完成验证.对于分数阶控制系统的高阶逻辑形式化验证, 首先要完善一些必要的数学理论和性质等, 再通过反复推敲各种需要的定义, 最终在一系列定理和性质的基础上验证控制系统的精准性、 时效性.函数正无穷大时极限是拉普拉斯变换形式化的基础, 拉普拉斯变换形式化验证是控制系统形式化验证的重要部分. 本文验证的函数正无穷大时极限及其性质将是控制系统验证平台的重要理论基础.后续将研究分数阶拉普拉斯变换的高阶逻辑形式化验证, 最后验证分数阶控制系统的优越性能. 在本文的基础上, 进一步验证机器人分数阶控制系统的安全稳定性能, 为机器人产业的发展提供有力保障.参 考 文 献[1]QianZhen-Jiang,HuangHao,SongFang-Min. Researchonconsi stencyverifi cat ionofformaldesignandsecurityrequi rementsforoperatingsyst em.ChineseJournalofComputers,2014,37( 5) :l〇82-l〇99( inChinese)( 钱振江, 黄皓, 宋方敏. 操作系统形式化设计与安全需求的一致性验证研究? 计算机学报, 201 4,37( 5) :1082-1 099)[2]HanJun-Gang.Expressingtemporallogici nhigher-orderlogi canditsapplications. ChineseJournalofComput ers,1993,16( 12) :925-930( inChinese)( 韩俊刚.用高阶逻辑表达时态逻辑及其应用. 计算机学报,1993,16( 1 2) :925-930)[3]LiuTao?WangShu-Ling,ZhanNai-Jun.Safetyverificationoftrajectoryplanni ngfor multiplerobots. JournalofSoftware,201 7,28( 5) :1 11 8-1 127( i nChinese)( 刘涛, 王淑灵, 詹乃军. 多机器人路径规划的安全性验证.软件学报, 2017 ,28( 5) :1 1 1 8-1127)[4]MaSha,ShiZhi-Pi ng,LiLi-Ming,etal.Formalizationofgeometricalgebrat heori esinhigherorderlogic.JournalofSoft ware,2016,27( 3) :49 7-516(inChinese)(马莎, 施智平, 李黎明等. 几何代数的高阶逻辑形式化. 软件学报,2016,27 ( 3) :4 97-516)[5]AbbasiN. FormalReliabilityAnalysisusingHighei^OrderLogicTheoremProving[Ph.D.di ssert ati on].DepartmentofEl ect rical andComputerEngi neeri ng, Concordi aUni versity,Montreal ^Quebec*Canada?201 2[6]SchumannJM. AutomatedTheoremProvinginSoft wareEngineering. NewYork,USA:Springer,2001[7]GordonMJC, MelhamTF.Introduct iont oHOL:ATheoremProvingEnvironment forHigherOrderLogic.NewYork,USA:CambridgeUniversityPress,1993[8]Harri sonJ.HandbookofPracticalLogicandAutomat edReasoning. Cambridge, UK: CambridgeUniversityPress,2009[9]SiddiqueU*HasanO. Formalanalysi soffract ionalordersyst emsi nHOL. FormalMethodsi nComputer-Ai dedDesign,201 1: 163-170[10]SiddiqueU,HasanO.Ontheformalizationoft hegammafunct ioninHOL.Journalof Automat edReasoni ng,201 4,53 : 407-429[11]LiuL, Hasan0, TaharS. Formalreasoningaboutfi nit e-stat ediscrete-timeMarkovchainsinHOL.JournalofComputerScienceandTechnology,2013,28(2) :2 17-231[12]KumarN,daCruzNC,RangelE C.DNA for nano-bioscal ecomputationofchemicalformalismsusingHigherOrderLogic( HOL)andanalysisusinganint erdisciplinaryapproach.MaterialsResearch, 2014, 17( 6) : 1391-13962132 计 算 2020年[13]AhmedW.HasanO,TaharS.Formali zationof rel i abilityblockdi agramsinhigher-orderlogi c. Journal ofAppliedLogic ,2016,18:19-41[14]SardarMU.HasanO,ShafiqueM,HenkelJ. Theoremprovingbasedformal verificationof distributeddynami cthermalmanagementschemes.JournalofParal lelandDi st ri butedComput ing,2017,100:1 57-1 71[ 1 5]Li L.Shi Z, GuanY, et al .Formalveri fi cat i on ofacoll ision-f reealgori thmfor adual-ar mrobot i nHOL4//Proceedi ngs oft heRoboti csandAutomation(I CRA). HongKong,Chi na?2014 :1 380-1 385[1 6]WangYF, Chen(;? Formali zat ionofLaplacetransf ormi nCoq//Proceedi ngsof the2017Fourt hInternat ional ConferenceonDependableSystemsandTheirApplications( Dsa2017).Beiji ng,China,2017: 13-21[ 17]TaqdeesSH,HasanO.Formal izati onof Laplacetransformusingt hemul t ivariablecal cul ust heoryofHOL-light//McMi llanK,Mi ddeldorpA,VoronkovAeds. LogicforProgrammi ng,ArtificialIntelligence,andReasoni ng. LNCS,vol. 831 2.Berli nHeidelberg:Springer-Verlag?2013:744-758[18]WeberT. Boundedmodelgenerati onfori sabelle/HOL.El ectronicNotesinTheoreticalComput erSci ence,2005 ,125 :1 03-116[19]PuitgF, DufourdJF. Formali zingmat hemat i csinhi gher-orderlogi c:Acasestudyi n geometric modelli ng.TheoreticalComputerScience , 2000, 234:1-57[20]RashidA, HasanO.Formalanalysisofcont i nuous-t imesyst emsusingFouri ert ransform.Journalof Symboli cComputation,201 9,90:65-88[21]Cardel l-OliverR. Thefor malveri fi cati onofhardreal-ti me机 学 报systems[Ph. D. di ssertation]. UniversityofCambri dge,Cambri dge , UK,1992[22]HarrisonJ. Formalizedmat hemat ics. TurkuCent reforComput erScience: TechnicalReport36,1 996[23]Sl i ndK,NorrishM.Abriefoverviewof HOL4//Proceedi ngsofthe21stI nternati onalConferenceonTheoremProvi ngi nHigherOrderLogi cs.Berlin, Germany: Springer Verlag,2008 :28-32[24]Harri sonJ. AHOLt heoryofEucl i deanspace//HurdJ.Mel hamTF, eds.TheoremProvi ngi nHigherOrderLogi cs(TPHOLs2005).Lect ureNot esi nComputerSci ence3603.Berli nHei del berg: Spri nger-Verl ag.2005:1 14-1 29[25]Shi Zhi-Pi ng,Li Li-Mi ng,GuanYong,et al.Formal izat ionoft hecompl exnumber t heoryi nHOLl . Applicat i onsofMat hemat ics,201 3?7( 1) :279-286[26]GuWei-Qi ng, ShiZhi-Ping, GuanYong,etal . Formali zationofGaugei ntegrati ont heoryinHOL4. ComputerScience?2013,40(2) :191-194(inChinese)( 谷伟卿. 施智平, 关永等. Gauge 积分在HOL4 中的形式化? 计算机科学, 2013 ,2 :1 91-194)[27]SchroderBSW. OrderedSets: AnIntroduction.Bost on,USA:Bi rkhauser,2002[28]DaveyBA, Pri estleyHA. I ntroductiontoLatti cesandOrder. NewYork:CambridgeUniversityPress,2002[29]ZhaoGang.ZhaoChun-Na , GuanYong, etal.Formalizat ionofLaplacetransformcalculusinHOL4.JournalofChineseComput erSyst ems,201 4 , 35( 9) :2177-2 1 81 ( i nChinese)(赵刚. 赵春娜? 关永等. 拉普拉斯变换微积分性质在HOL4中的形式化. 小型微型计算机系统,2014,35 ( 9 ) : 2177-2 181 )ZHAOChun-Na.Ph.D.,professor.Hermainresearchinterest si ncludehigherorderlogicverifi cationandfractionalordersystems.ZHAOGang.M. S.Hismai nresearchinterestishigherorderlogicverification.BackgroundThispapersurveysthefieldofhigherorderlogicformalverifi cat i on. Higherorderl ogi cformalverifi cationi si nthestageofdevel opment.Theresearchersf romallovertheworldworkonhighe rorderlogict heoremlibrary,andthenverificat ionofrel atedpract i calproblemsonthegroundofthel i brary.Thisworkisthepartialcont entofhigherorderlogicformalmodel ingandveri ficat ionoffractionalordersyst ems.Formalmodelingandverificationoffunct ionlimit arecreat edi nhigherorderlogi c.Basedonhigherorderlogicmodelsofsetandnumber,formalmodeloffunct i onlimi tdefinitionandit srelat edpropert ies—uniqueness,i nequalitypreservingproperty,theabsolut eval uefunctionlimitwhensolvingit spositiveinfinityl imi t,limi tequivalence?const antfunctionlimit,et c—areproposedi nthispaper. Higherorderlogicmodelofari thmet icoffunctionli mitisal soest abli shedin赵春娜等: 函数极限的高阶逻辑形式化建模与验证 21331 1 期higherorderlogictheoremprover.Andsomerelatedtheoremsareverified.Thehigherorderlogicformalmodel ingandverificationoffunctionintegrallimitisalsoproposedi nthispaper.Formalmodeli ngandverificationofLaplacetransfor?mationconvolutiontheoremisestablishedinhigherorderlogi ctheoremprover.Formalmodel ingandverificationofthecurrentinResi stor-i nductorcircui thasbeendiscussedasaninstance.Thehigherorderlogicformalmodelsofunitstepsignalandc urrentintheci rcuitareproposedbasedontheverifieddefini tionsinhigherorderlogictheoremprover.Theworkattributestotheproject“FormalAnalysi sandVerificati onofFractionalOrderPIDControl lerBasedonHigherOrderLogic”, whichissupportedbytheNationalNatural ScienceFoundationofChina(No.61862062).Fractionalordercontrolsystemisami lestonei nthehistoryoffractionalordercontroltheory.Itisabletoimprovethecontrolpreci sionandaccuracyofthesystemandgetmorerobustcontrolresults.Theoremprovingformalverificationmethodcanbeusedforanysystemthatcanbeexpressedbymathematicalmodel.Iti stheidealverifi cationmethodbecausei tisnotsubjecttolimitsonstatenumbers.Thisprojectresearchesformalverificationandmodel ingoffractionalordercont rolsystem. Theresearchresul tswi llenhancetoimprovethecontrolperformanceofcontrolsystem,toachievethecompleteverificationoffractionalordercontrolsystems?toensurethereliabilityandsecurityofrobotcontrolsystems.Ourresearchgrouphasbeenworkingonhigherorderlogicformalverificationoffractionalordersystems.Fractionalordercal cul ushasbeenverifiedinhigherorderlogictheoremprover.Relatedworkswerepubl ishedi ngood-reputationjournalsandconferences,suchasTheoreticalComputerScience, ISATransactions,ICRA.Thispaperprovidesthebasicmathematicalfoundationlibraryforcontrolsyst em.Itlaysagoodfoundationforthefol low-upformalanalysisoffractionalordercontrolsystems.

[返回]
上一篇: 基于声波感知的移动设备实时防窃方法研究
下一篇:利用网格卷积特征的三维形变目标分类