基于HybridUML和定理证明的CPS自适应性验证方法

本发明提出一种基于HybridUML和定理证明的CPS自适应性验证方法，主要用于解决形式化验证方法理论性过强所带来的难以普遍应用的难题。本发明步骤包括：首先利用HybridUML视图对CPS建模；然后将HybridUML规约转换为定理证明器KeYmaera的输入-量化混合程序QHP；结合生成的QHP，以量化微分动态逻辑QdL公式的形式对待验证的属性进行规约，然后利用KeYmaera进行自动验证；进行模型转换之前，需要定义HybridUML和QHP的元模型，转换时首先消除顶层Mode具有的层次性，转换后"