电子学报

• 学术论文 • 上一篇    下一篇

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

朱敏, 李必信, 陈乔乔, 吉顺慧, 李加凯   

  1. 东南大学计算机科学与工程学院,江苏南京 211189
  • 收稿日期:2011-09-22 修回日期:2012-03-14 出版日期:2012-06-25
    • 通讯作者:
    • 李必信 男,1969年出生于安徽省庐江县,博士/博士后,现任东南大学计算机科学与工程学院教授、博士生导师,CCF高级会员,主要研究领域为软件分析、测试、验证,实证软件工程. E-mail:bx.li@seu.edu.cn
    • 作者简介:
    • 朱 敏 男,1988年出生于安徽省庐江县,现为东南大学计算机科学与工程学院在读硕士研究生,主要研究方向为CPS验证. E-mail:kong@seu.edu.cn
      陈乔乔 男,1987年出生湖北省荆门市,现为东南大学计算机科学与工程学院在读硕士研究生,主要研究方向为CPS验证. E-mail:joe_0701@126.com
      吉顺慧 女,1987年出生江苏省海安市,现为东南大学计算机科学与工程学院在读博士研究生,主要研究方向为Web服务验证. E-mail:shunhuiji@seu.edu.cn
      李加凯 男,1987年出生山东省潍坊市,现为东南大学计算机科学与工程学院在读硕士研究生,主要研究方向为CPS验证. E-mail:jiakai_li@seu.edu.cn
    • 基金资助:
    • 国家自然科学基金 (No.60973149); 博士点基金 (No.20100092110022); 中科院计算机科学国家重点实验室开放基金基金 (No.SYSKF1110)

Transforming HybridUML to Hybrid Program for CPS Property Verification

ZHU Min, LI Bi-xin, CHEN Qiao-qiao, JI Shun-hui, LI Jia-kai   

  1. School of Computer Science and Engineering,Southeast University,Nanjing,Jiangsu 211189,China
  • Received:2011-09-22 Revised:2012-03-14 Online:2012-06-25 Published:2012-06-25
    • Supported by:
    • National Natural Science Foundation of China (No.60973149); Doctoral Foundation (No.20100092110022); Open Project of the State Key Laboratory of Computer Science (No.SYSKF1110)

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

关键词: 信息物理融合系统, 微分动态逻辑, HybridUML, 模型转换, 验证

Abstract: With the wide application of cyber-physical systems(CPS),it is of vital importance to ensure that the design and implementation of CPS meet critical performance requirements (e.g.,security,reliability).This paper presents a framework for CPS modeling and verification.In the framework,CPS are modelled by HybridUML and then the generic model is transformed to a formal model that is suitable for reasoning with the help of formal methods.The formal method adopted is differential dynamic logic(dL) whose operational model is hybrid program(HP).When transforming a HybridUML model to its corresponding HP presentation,transformation rules are defined according to semantic consistency.After transformation,CPS properties are specified on the basis of the resulting HP,and finally,the properties are automatically verified through the theorem prover KeYmaera.

Key words: CPS, differential dynamic logic, HybridUML, model transformation, verification

中图分类号: