基于微分动态逻辑的CPS建模与属性验证

• 作者: 吉顺慧 朱敏 李加凯 李必信 陈乔乔
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 信息物理融合系统 微分动态逻辑 HybridUML 模型转换 验证
• 年，卷（期）: 2012,（6）
• 所属期刊栏目: 学术论文
• 页码范围: 1126-1132
• 分类号: TP301
• 字数: 5901字
• 语种: 中文
• DOI: 10.3969/j.issn.0372-2112.2012.06.010

摘要

随着信息物理融合系统(Cyber-Physical Systems,CPS)应用的越来越普及,CPS的设计和实现能否满足实际需求显得至关重要.本文提出了一种CPS建模与属性验证框架.在框架中,首先使用HybridUML对CPS进行建模,然后将该通用模型转换为形式化模型,进而进行形式化验证.本文采用的形式化验证方法为dL(Differential Dynamic Logic),其操作模型为hybrid program.将HyhridUML模型转换为hybrid program时,基于语义一致性的原则定义转换规则.转换完成后,结合得到的hybrid program对验证的CPS属性进行规约,最后使用定理证明器KeYmaera对属性进行自动化验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	吉顺慧	东南大学计算机科学与工程学院	4	44	4.0	4.0
2	李必信	东南大学计算机科学与工程学院	39	305	9.0	15.0
3	朱敏	东南大学计算机科学与工程学院	16	76	5.0	8.0
4	陈乔乔	东南大学计算机科学与工程学院	2	33	2.0	2.0
5	李加凯	东南大学计算机科学与工程学院	1	29	1.0	1.0