本发明提出了一种基于HybridUML向微分代数程序转换的CPS建模与验证方法,实现了由HybridUML模型向DAP的转换,并依据微分代数动态逻辑(Differential-AlgebraicDynamicLogic,DAL)推理规则对CPS实例进行验证。该方法使用HybridUML对CPS进行建模,将其转换成DAL的操作模型DAP,并且基于DAL对CPS属性进行验证。