一种基于CPS‑ADL模型向混合程序转换的CPS建模与验证方法

摘要

本发明公开了一种基于CPS‑ADL模型向混合程序转换的CPS建模与验证方法，主要用于处理CPS建模与属性验证问题，其特征在于：在CPS‑ADL平台上采用扩展的混成系统描述语言E‑HYSDEL对CPS进行建模；给出HP模型的形式化定义HPM，并在满足模型转换一致性的前提下建立CPS‑ADL模型元素与HP模型元素之间的转换规则；基于这些转换规则，将具体CPS的模型描述代码自动转换为混合程序；按照定理证明器KeYmaera的输入格式，由混合程序和以动态微分逻辑描述的系统属性公式生成KeYmaera的输入文件；在KeYmaera中打开输入文件，进行推理验证。本发明细化了基于CPS‑ADL模型向HP转换的方法和机制，实现了CPS‑ADL模型元素向HP模型元素转换的规则。