一种基于LHPN的信息物理融合系统模型验证方法

计算机科学 ›› 2014, Vol. 41 ›› Issue (Z6): 64-66.

一种基于LHPN的信息物理融合系统模型验证方法

丘威

嘉应学院计算机学院梅州514015

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受广东省自然科学基金(S2013010013307),广东省高等学校学科专业建设专项资金(2013KJCX0171)资助

Method for Verification of LHPN-based Cyber Physical System

QIU Wei

Online:2018-11-14 Published:2018-11-14

摘要/Abstract

摘要： 由于信息物理融合系统(CPS)的硬件集成度和软件参与度不断提高,大量软件与硬件间异构连通并相互控制,使得CPS的分析设计、建模与验证也愈加困难,由此引起模型的状态空间膨胀问题。提出利用带标记混合Petri网方法对CPS进行建模和验证研究,在CPS中采用模型检测和定理证明相结合的形式化方法,对试图解决系统验证时状态空间膨胀问题供理论依据。提出一种自动抽取及其简化模型的方法,在容错温度传感器系统中的初步实验结果表明该方法是可行的,通过一个实例原型的应用说明了该方法的有效性。

关键词: 带标记混合Petri网,信息物理融合系统,建模,验证中图法分类号TP391.4文献标识码A

Abstract: Because the cyber-physical system(CPS) hardware integration and software involvement in degree rise ceaselessly,many software and hardware have heterogeneous connectivity and mutual control．The analysis design,modeling of CPS have become more and more difficult．In this paper,a safety verification method based on 1abeled hybrid Petri net and differential-algebraic dynamic logic was proposed．The method firstly transforms LHPN model to differential-algebraic program,then realizas the specification of system safety using differential-algebraic program,and finally the cyber physical systems safety is verified according to differential-algebraic program reasoning rules．It is effectiveness for the method through an instance of the prototype application.

Key words: Labeled hybrid Petri net,Cyber physical system,Modeling,Verification

丘威. 一种基于LHPN的信息物理融合系统模型验证方法[J]. 计算机科学, 2014, 41(Z6): 64-66. https://doi.org/

QIU Wei. Method for Verification of LHPN-based Cyber Physical System[J]. Computer Science, 2014, 41(Z6): 64-66. https://doi.org/

参考文献

[1] Zhang Li-chen．Formal Methods for Aspect-Oriented Specification of Cyber Physical Systems[C]∥Communications in Computer and Information Science．Springer,2011,5:316-322
[2] Zhang Li-chen．QoS Specification for Cyber-physical Systems[C]∥CCIS．Springer,2011,5:329-334
[3] Thacker R A,Jones K R,Myers C J,et al．Automatic Abstraction for Verification of Cyber-Physical Systems[C]∥Procee-dings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems.2010:12-21
[4] Zhang Li-chen．MDA Approach for Non-functional Characteristics of Cyber Physical Systems Based on Aspect-Oriented Method[C]∥Communications in Computer and Information Science．Springer,2011,5:323-328
[5] 黎作鹏,张天驰,张菁．信息物理融合系统(CPS)研究综述[J]．计算机科学,2011(9):25-31
[6] Yun H,Liang Wu-po,Rahmaniheris M,et al．A Reduced Complexity Design Pattern for Distributed Hierarchical Command and Control System[C]∥Proceedings of the 1st ACM/IEEE International Conference on Cyber-Physical Systems.2010:42-49
[7] Parolini L,Tolia N,Sinopoli B,et al.A Cyber-Physical Systems Approach to Energy Management in Data Centers[C]∥ICCPS’10．Stockholm,Sweden,2010:168-177
[8] Tan Ying,Vuran M C,Goddard S,et al.A Concept Lattice-based Event Model for Cyber-Physical Systems[C]∥Procee-dings of the 1st ACM/IEEE International Conference of Cyber Physical Systems.2010:50-60
[9] Chun I,Park J,Kim W,et al．Autonomic Computing Technologies for Cyber-Physical Systems[C]∥Proceedings of the International Conference on Advanced Communication Technology.2010:1009-1014
[10] Woo H,Yi Jiang-liang,Browne J C．Design and DevelopmentMethodology for Resilient Cyber-Physical Systems[C]∥Proceedings of the 28th International Conference on Distributed Computing Systems Workshops.2008:525-528
[11] Vicaire P A,Hoque E,Xie Zhi-heng,et al.Bundle:A GroupBased Programming Abstraction for Cyber Physical[C]∥Proceedings of the 1st ACM/IEEE International Conference of Cyber-Physical Systems.2010:32-41
[12] Ahmadi H,Abdelzaher T F,Gupta I．Congestion control for spatiotemporal data in cyber-physical systems[C]∥Proceedings of the 1st International Conference on Cyber-physical Systeam(ICCPS’10)．New York,NY,USA:ACM,2010:89-98
[13] Tan Ying,Vuran M C,Goddard S,et al．A Concept Lattice-based Event Model for Cyber-Physical Systems[C]∥Procee-dings of the 1st ACM/IEEE International Conference on Cyber Physical Systems．2010:50-60

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed