基于微分动态逻辑的液压运动系统的分析与验证

液压运动系统既包含连续过程也包含离散过程,可以认为是一个混成系统,在以往研究中缺乏对此类系统安全性的建模与证明。为了解决这个问题,以经典液压运动系统为例,结合专业知识,用微分方程对整个系统运动过程进行详细描述。结合微分动态逻辑和混成程序建立模型,通过工具KeYmaera来验证所建模型的正确性及液压运动系统运动的安全性。结果表明,所建模型正确,安全性良好。该方法适合应用于此类系统的建模与验证过程。

Analysis and Verification of Hydraulic Kinetic System Based=on Differential Dynamic Logic

Hydraulic motion system includes both continuous and discrete processes and can be considered a hybrid system.In previous studies,modeling and verification of security for such systems is lacking.In order to solve this problem,taking the classic hydraulic motion system as an example,combined with the professional knowledge,the differential equation of the whole system motion process was described in detail.Combined with differential dynamic logic and hybrid procedure,the model was built.Correctness of the model and safety of the hydraulic motion system were verified by the tool KeYmaera.The running results of KeYmaera showed that the model was correct and the safety of which was good,and the method was suitable for modeling and verification of such systems.