基于量化微分动态逻辑的CPS自适应性验证

摘要

信息物理融合系统(Cyber-Physical systems，CPS)是一类融合了计算与物理过程，并且通过通信网络高度集成的物理设备系统。形式化验证作为验证系统正确性的重要方法已经成功应用于CPS的正确性验证，然而形式化验证方法理论性很强。难以广泛应用到工业实践中。首先利用工业实践中的标准建模语言UML的扩展-Hybri—dUML对CPS进行建模，然后将HybridUML模型转换为定理证明器KeYmaera的输入-量化混合程序(QuantifiedHybrid Program，QHP)，利用KeYrmera对模型进行形式化验证。