一种基于微分代数时序动态逻辑的CPS属性验证方法

项目简介

       本发明提出了一种基于微分代数时序动态逻辑的CPS属性验证方法,用于对CPS进行系统建模、属性规约和属性验证。本发明涉及到的关键操作包括:(1)在对CPS详细分析的基础上,使用微分代数程序对CPS进行系统建模,得到系统的操作模型;(2)使用DATL对要验证的CPS属性进行规约,得到DATL公式,此规约过程考虑了CPS的时序行为;(3)使用DATL中的相继式演算对前面得到的DATL公式进行验证,整个演算过程是通过不断地使用DATL规则来进行推理,最后得出DATL公式成立,也就是CPS属性满足。


过程模型

所属领域

电子信息


合作方式

技术咨询、技术服务