基于定理证明器HOL4的模糊控制器形式化研究

作     者：张展豪 

作者单位：北京化工大学 

学位级别：硕士

导师姓名：张杰

授予年度：2022年

学科分类：08[工学] 0802[工学-机械工程] 080201[工学-机械制造及其自动化] 

主      题：模糊数学 模糊控制 形式化方法 定理证明 HOL4 

摘      要：相较于传统控制方法,模糊控制能够有效处理复杂系统中存在的不精确性问题,从而得到了广泛应用。随着其应用范围的不断扩大,基于模糊控制的被控系统安全性就显得尤为重要;而传统的测试方法由于无法覆盖所有输入空间,因此不能确保结论的完备性;为了将形式化验证方法引入基于模糊控制的应用验证中,保证其结论对于任意输入均成立,建立一个可复用的模糊控制器形式化模型是必不可少的工作。为此,本课题采用了形式化方法中的定理证明方法,基于HOL4(Higher-Order Logic4)对模糊控制器进行形式化研究。论文首先介绍了模糊数学中基础理论的形式化建模,其中包含了基本定义的形式化模型及其性质的验证,并将其表示为定理的形式;之后在此基础上设计了模糊控制器的形式化架构,主要包括四个模块的形式化建模及其整合;在建模过程中,模糊化方法函数、模糊子集、控制规则均作为参数输入,使模型具有更强的复用性;同时对模型中矩阵扩展为向量、规则库合成运算的功能函数在设计上进行了优化,降低了模型整体的复杂度;最后通过一个具体应用给出基于该设计的形式化验证过程;在验证中引入前向证明思想,规划关键的验证步骤,为目标中因嵌套递归而难以化简的问题提供了一种解决思路。本课题使用定理证明法,对模糊数学以及模糊控制进行了形式化研究,给出了模糊控制器的一种可复用形式化模型架构,扩展了定理证明法的应用范围,对未来使用定理证明法,验证以模糊数学及模糊控制为基础的算法具备一定的参考和借鉴价值。