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

摘要

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