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

doi:10.3969/j.issn.0372-2112.2012.06.010

电子学报

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

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

东南大学计算机科学与工程学院,江苏南京 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

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)

摘要/Abstract

摘要： 随着信息物理融合系统(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

中图分类号:

TP301

朱敏, 李必信, 陈乔乔, 等. 基于微分动态逻辑的CPS建模与属性验证[J]. 电子学报, DOI: 10.3969/j.issn.0372-2112.2012.06.010.

ZHU Min, LI Bi-xin, CHEN Qiao-qiao, et al. Transforming HybridUML to Hybrid Program for CPS Property Verification[J]. Acta Electronica Sinica, DOI: 10.3969/j.issn.0372-2112.2012.06.010.

参考文献

[1] Lee EA.Cyber physical systems:Design challenges .Proceedings of 11th IEEE Symposium on Object Oriented Real-time Distributed Computing(ISORC) .Washington:IEEE Computer Society,2008.363-369.

[2] Chutinan A,Krogh,BH.Computational techniques for hybrid system verification[J].IEEE Transactions on Automatic Control,2003,48(1):64-75.

[3] Tiwari A.Approximate reachability for linear systems .Proceedings of Hybrid Systems:Computation and Control .Verlag:Springer,2003.514-525.

[4] Platzer A,Clarke,EM.The image computation problem in hybrid systems model checking .10workshop on Hybrid System:Computation and control .Heidelberg:Springer,2007.473-486.

[5] Collins P,Lygeros J.Computability of finite-time reachable sets for hybrid systems .Proceedings of the 44th IEEE Conference on Decision and Control,and the European Control Conference .New Jersey:Piscataway,2005.4688-4693.

[6] Zhou CC,Hansen MR.Duration Calculus:A Formal Approach to Real-Time Systems[M].Heidelberg:Springer,2004.41-62.

[7] Platzer A.Differential dynamic logic for hybrid systems[J].Journal of Automated Reasoning,2008,41(2):143-189.

[8] 刘亚萍,黄志球,祝义.基于元建模的实时系统模型转换方法研究[J].小型微型计算机系统,2010,31(11):2146-2153. Liu Yaping,Huang Zhiqiu,Zhu Yi.Research on model transformation method of real-time system based on metamodeling[J].Journal of Chinese Computer Systems,2010,31(11):2146-2153.(in Chinese)

[9] Stefan Bisanz.Executable HybridUML Semantics:A Transformation Definition .Bremen:University of Bremen,2005.

[10] Kirsten Berkenkøtter,Stefan Bisanz,Ulrich Hannemann,Jan Peleska.The HybridUML profile for UML 2.0[J].International Journal on Software Tools for Technology Transfer(STTT),2006,8(2):167-176.

[11] 周颖,郑国梁,等.面向模型检验的UML状态机语义[J].电子学报,2004,51(12):2091-2095. ZHOU Ying,ZHENG Guo-liang,et al.An operational semantics for UML State Machines in model checking context[J].Acta Electronica Sinica,2004,51(12):2091-2095.(in Chinese)

[12] Platzer A,Quesel JD.KeYmaera:A hybrid theorem prover for hybrid systems .International Joint Conference on Automated Reasoning(IJCAR) .Heidelberg:Springer,2008.171-178.

[13] Platzer,A.Logical Analysis of Hybrid Systems:Proving Theorems for Complex Dynamics[M].Heidelberg:Springer,2010.

[14] Caplat G,Sourrouille J-L.Model mapping using formalism extensions[J].IEEE Software,2005,22(2):44-51.

[15] Czarnecki K,Helsen S.Classification of model transformation approaches .OOPSLA’03 Workshop on Generative Techniques in the Context of Model-driven Architecture .New York:ACM Press,2003.

[16] 战德臣,冯锦丹,等.ICEMDA:一种可互操作可配置可执行的模型驱动体系结构[J].电子学报,2008,36(12A):120-127. ZHAN De-chen,FENG Jin-dan,et al.ICEMDA:An interoperable configurable executable model driven architecture[J].Acta Electronica Sinica,2008,36(12A):120-127.(in Chinese)

[17] 赖明志,尤晋元.从UML状态图到PVS规范的自动转换、验证[J].电子学报,2002,30(12A):2122-2125. LAI Ming-zhi,YOU Jin-yuan.Automatic transform UML statechart into PVS[J].Acta Electronica Sinica,2002,30(12A):2122-2125.(in Chinese)

[18] Platzer A,Quesel,J.D.European Train Control System:A case study in formal verification .Formal Methods and Software Engineering:11th International Conference on For- mal Engineering Methods .Heidelberg:Springer,2009.246-265.

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

Transforming HybridUML to Hybrid Program for CPS Property Verification

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

[1]	陈书仪, 刘亚丽, 林昌露, 李涛, 董永权. 面向物联网的轻量级可验证群组认证方案[J]. 电子学报, 2022, 50(4): 990-1001.
[2]	杨坤伟, 杨波, 周彦伟. 群智网络中基于区块链的有序聚合签名认证方案[J]. 电子学报, 2022, 50(2): 358-365.
[3]	蔡莹, 朱翔, 王舰, 李昊远, 韩建伟. 基于激光注入的FPGA加密防护设计验证研究[J]. 电子学报, 2022, 50(10): 2381-2386.
[4]	朱健, 胡凯, 张伯钧. 智能合约的形式化验证方法研究综述[J]. 电子学报, 2021, 49(4): 792-804.
[5]	杨启良, 周彦伟, 杨坤伟, 王涛. 标准模型下可公开验证的匿名IBE方案的安全性分析[J]. 电子学报, 2020, 48(2): 291-295.
[6]	孙朋朋, 董云卫. 二维全向无线充电信息物理融合系统建模与优化方法[J]. 电子学报, 2019, 47(3): 568-575.
[7]	房丙午, 黄志球, 王勇, 李勇. 状态不可观测的信息物理融合系统运行时验证[J]. 电子学报, 2018, 46(12): 2824-2831.
[8]	杜思军, 徐尚书, 刘俊南, 张俊伟, 马建峰. 云计算中抗共谋攻击的数据位置验证协议[J]. 电子学报, 2017, 45(6): 1321-1326.
[9]	任正伟, 孙小雁, 王丽娜, 王骞, 徐明迪, 张茂胜. 基于简单随机抽样的大数据可信性验证方法[J]. 电子学报, 2017, 45(10): 2484-2490.
[10]	彭巧, 田有亮. 基于多线性Diffie-Hellman问题的秘密共享方案[J]. 电子学报, 2017, 45(1): 200-205.
[11]	钱振江, 刘永俊, 姚宇峰, 汤力, 黄皓, 宋方敏. 微内核架构内存管理的形式化设计和验证方法研究[J]. 电子学报, 2017, 45(1): 251-256.
[12]	江南, 何炎祥, 张晓瞳. _mJava到Micro-Dalvik虚拟机的编译验证[J]. 电子学报, 2016, 44(7): 1619-1629.
[13]	李顺东, 杨坤伟, 巩林明, 毛庆, 刘新. 标准模型下可公开验证的匿名IBE方案[J]. 电子学报, 2016, 44(3): 673-678.
[14]	雷红轩, 彭家寅, 刘熠. 几类非确定型量子程序的终止验证[J]. 电子学报, 2016, 44(12): 2932-2938.
[15]	周洪丞, 杨超, 马建峰, 张俊伟. 云端数据异地容灾验证方案研究[J]. 电子学报, 2016, 44(10): 2485-2494.