公开(公告)号：CN102436375B

公开(公告)日：2014-05-07

申请号：CN201110332336.4

申请日：2011-10-28

Applicant: 东南大学

Inventor： 李必信 ,  朱敏 ,  李加凯 ,  陈乔乔 ,  翟小祥

IPC: G06F9/44

Abstract: 本发明提出了一种基于模型转换的CPS建模与验证方法，主要用于处理CPS建模与属性验证问题，本发明涉及到的关键操作包括：(1)采用HybridUML对CPS进行建模，并将所建HybridUML模型转换为微分动态逻辑方法的操作模型混合程序Hybrid？Programs。首先按照HybridUML和Hybrid？Programs元模型元素之间的关系定义模型转换的规则，并生成规则应用的模板，再在模型层次应用规则进行模型转换自动生成Hybrid？Programs；(2)将得到的Hybrid？Programs根据定理证明器KeYmaera的输入格式，生成输入代码，在KeYmaera中进行推理验证。

公开(公告)号：CN102722593B

公开(公告)日：2014-08-06

申请号：CN201110332307.8

申请日：2011-10-28

Applicant: 东南大学

Inventor： 李必信 ,  翟小祥 ,  李加凯 ,  朱敏 ,  陈乔乔

IPC: G06F17/50

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

公开(公告)号：CN102436375A

公开(公告)日：2012-05-02

申请号：CN201110332336.4

申请日：2011-10-28

Applicant: 东南大学

Inventor： 李必信 ,  朱敏 ,  李加凯 ,  陈乔乔 ,  翟小祥

IPC: G06F9/44

Abstract: 本发明提出了一种基于模型转换的CPS建模与验证方法，主要用于处理CPS建模与属性验证问题，本发明涉及到的关键操作包括：(1)采用HybridUML对CPS进行建模，并将所建HybridUML模型转换为微分动态逻辑方法的操作模型混合程序Hybrid Programs。首先按照HybridUML和Hybrid Programs元模型元素之间的关系定义模型转换的规则，并生成规则应用的模板，再在模型层次应用规则进行模型转换自动生成Hybrid Programs；(2)将得到的Hybrid Programs根据定理证明器KeYmaera的输入格式，生成输入代码，在KeYmaera中进行推理验证。

公开(公告)号：CN102426522B

公开(公告)日：2014-12-10

申请号：CN201110338092.0

申请日：2011-10-28

Applicant: 东南大学

Inventor： 李必信 ,  陈乔乔 ,  翟小祥 ,  宋锐 ,  张前东

IPC: G06F9/44

Abstract: 本发明提出了一种基于HybridUML向微分代数程序转换的CPS建模与验证方法，实现了由HybridUML模型向DAP的转换，并依据微分代数动态逻辑(Differential-Algebraic Dynamic Logic，DAL)推理规则对CPS实例进行验证。该方法使用HybridUML对CPS进行建模，将其转换成DAL的操作模型DAP，并且基于DAL对CPS属性进行验证。

公开(公告)号：CN102722593A

公开(公告)日：2012-10-10

申请号：CN201110332307.8

申请日：2011-10-28

Applicant: 东南大学

Inventor： 李必信 ,  翟小祥 ,  李加凯 ,  朱敏 ,  陈乔乔

IPC: G06F17/50

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

公开(公告)号：CN102426522A

公开(公告)日：2012-04-25

申请号：CN201110338092.0

申请日：2011-10-28

Applicant: 东南大学

Inventor： 李必信 ,  陈乔乔 ,  翟小祥 ,  宋锐 ,  张前东

IPC: G06F9/44

Abstract: 本发明提出了一种基于HybridUML向微分代数程序转换的CPS建模与验证方法，实现了由HybridUML模型向DAP的转换，并依据微分代数动态逻辑(Differential-Algebraic Dynamic Logic，DAL)推理规则对CPS实例进行验证。该方法使用HybridUML对CPS进行建模，将其转换成DAL的操作模型DAP，并且基于DAL对CPS属性进行验证。