基于高阶逻辑的分数阶PID控制器形式化分析与验证

Fractional order PID controller is a milestone in the history of fractional order control theory. It is able to improve the control precision 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 is the ideal verification method because it is not subject to limits on state numbers. This project researches formal verification and modelling of fractional order PID controller, including the following aspects: research on parameter setting method and analytical model of fractional order PID controller; research on logical model of fractional order PID controller; research on higher order logic formalization of fractional Laplace transform; research on the theorem proving formal description of fractional order PID control system and development of its theorem library in HOL; research on formal analysis and verification of fractional order PID control system performance. The superior performance of fractional order PID control systems will be verified based on established library files in robot systems. A breakthrough achievement on theories and methods of formal analysis and verification for fractional order PID control systems will be achieved in this project. The research results will enhance to improve the control performance of control system, to achieve the complete verification of fractional order PID control systems, to ensure the reliability and security of robot control systems.

分数阶PID控制器是分数阶控制理论历史上的一个里程碑，她能够提高系统的控制精度和准确性，得到更鲁棒的控制结果。定理证明形式化验证方法可用于任何能被数学模型表示的系统，不受状态数限制，是非常理想的验证方法。本项目研究分数阶PID控制器模型设计和分数阶PID控制系统的形式化分析与验证，包括研究分数阶PID控制器参数整定方法，建立分数阶PID控制器的解析模型；研究分数阶PID控制器逻辑模型建立；研究分数阶拉普拉斯变换的高阶逻辑形式化；研究分数阶PID控制系统高阶逻辑形式化模型并开发定理库；研究分数阶PID控制系统性能的形式化分析与验证方法；应用建立的库文件验证机器人系统中分数阶PID控制系统的优越性能。本项目将在分数阶PID控制系统形式化证明理论和方法方面取得突破。研究成果将提高控制系统的控制性能，实现分数阶PID控制系统的完备验证，保障机器人控制系统的可靠性和安全性。

分数阶PID控制器是分数阶控制理论历史上的一个里程碑，她能够提高系统的控制精度和准确性，得到更鲁棒的控制结果。定理证明形式化验证方法可用于任何能被数学模型表示的系统，不受状态数限制，是非常理想的验证方法。本项目研究了分数阶PID控制器模型设计和分数阶PID控制系统的形式化分析与验证，包括研究了分数阶PID控制器参数整定方法，建立了分数阶PID控制器的解析模型；研究了分数阶PID控制器逻辑模型建立；研究了分数阶拉普拉斯变换的高阶逻辑形式化；研究了分数阶PID控制系统高阶逻辑形式化模型并开发定理库；研究了分数阶PID控制系统性能的形式化分析与验证方法；应用建立的库文件验证机器人系统中分数阶PID控制系统的优越性能。本项目研究成果可以提高控制系统的控制性能，实现分数阶PID控制系统的完备验证，保障机器人控制系统的可靠性和安全性。