作者其他论文
文献详情
一种基于CPS-ADL模型向混合程序转换的CPS建模与验证方法
文献类型:专利
发明人:周兴社[1]  拓明福[2]  张凡[3]  杨刚[4]  单黎君[5]  杨亚磊[6]  张军[7]  
机构:[1]西北工业大学
[2]西北工业大学
[3]西北工业大学
[4]西北工业大学
[5]西北工业大学
[6]西北工业大学
[7]空军工程大学
申请人:西北工业大学
专利类型:发明专利
年度:2014
专利公开号:CN103699743A
专利申请号:CN201310723208.1
人气指数:115
浏览次数:115
摘要:本发明公开了一种基于CPS-ADL模型向混合程序转换的CPS建模与验证方法,主要用于处理CPS建模与属性验证问题,其特征在于:在CPS-ADL平台上采用扩展的混成系统描述语言E-HYSDEL对CPS进行建模;给出HP模型的形式化定义HPM,并在满足模型转换一致性的前提下建立CPS-ADL模型元素与HP模型元素之间的转换规则;基于这些转换规则,将具体CPS的模型描述代码自动转换为混合程序;按照定理证明器KeYmaera的输入格式,由混合程序和以动态微分逻辑描述的系统属性公式生成KeYmaera的输入文件;在KeYmaera中打开输入文件,进行推理验证。本发明细化了基于CPS-ADL模型向HP转换...
0
评论(0 条评论)
登录