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

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