面向服务的信息物理融合系统建模与验证

doi:10.11772/j.issn.1001-9081.2014.06.1770

计算机应用 ›› 2014, Vol. 34 ›› Issue (6): 1770-1773.DOI: 10.11772/j.issn.1001-9081.2014.06.1770

面向服务的信息物理融合系统建模与验证

刘明星,马武彬,邓苏,黄宏斌

国防科学技术大学信息系统工程重点实验室,长沙 410073

收稿日期:2013-11-18 修回日期:2013-12-25 发布日期:2014-07-02 出版日期:2014-06-01
通讯作者: 刘明星
作者简介:刘明星(1986-),男,江西九江人,博士研究生,主要研究方向:信息物理融合系统建模与验证;马武彬(1986-),男,重庆人,博士研究生,主要研究方向:数据挖掘、信息检索;邓苏(1963-),男,湖南长沙人,教授,博士,主要研究方向:信息综合处理与辅助决策;黄宏斌(1975-),男,江苏如皋人,教授,博士,主要研究方向:信息处理、语义覆盖网。

Modeling and verification of services oriented cyber physical systems

LIU Mingxing,MA Wubin,DENG Su,HUANG Hongbin

Science and Technology on Information Systems Engineering Laboratory, National University of Defense Technology, Changsha Hunan 410073, China

Received:2013-11-18 Revised:2013-12-25 Online:2014-07-02 Published:2014-06-01
Contact: LIU Mingxing

摘要/Abstract

摘要：

针对信息物理融合系统(CPS)中建模与验证面临的问题与挑战,基于服务组合的思想,提出一种CPS建模与验证方法。首先,综合分析已有研究成果,提出一种CPS的组成结构,包含物理世界、感知系统、信息处理系统、控制系统及时间约束。基于该结构提出CPS资源的服务分类及组成框架,并利用时间自动机理论,提出CPS物理环境建模方法、CPS原子服务建模方法及服务组合方法。最后,通过案例设计和模型检测工具Uppaal,分别对系统安全性、可达性、活性及时间约束四种类型的性质进行了相关验证。结果表明,系统通过了这些性质的验证,这也证明了面向服务的CPS建模方法的正确性。

Abstract:

Concerning the problems and challenges in Cyber Physical System (CPS), a new modeling and verification method of CPS was proposed based on service composition ideas. Firstly, a composition structure of CPS was proposed, including the physical world, sensor systems, information processing systems, control systems and time constraints. Based on this proposed structure, the service classification and composition framework of CPS resources were proposed. The physical environment modeling, atomic service modeling and service composition of CPS were also given based on the timed automata theory. Finally, through case design and model checking tool Uppaal, the experimental results were given to illustrate the correctness of the CPS service-oriented modeling approach, including system security, accessibility, liveness and time constraints. The results verify the above properties and the correctness of the proposed method.

中图分类号:

TP393

刘明星马武彬邓苏黄宏斌. 面向服务的信息物理融合系统建模与验证[J]. 计算机应用, 2014, 34(6): 1770-1773.

LIU Mingxing MA Wubin DENG Su HUANG Hongbin. Modeling and verification of services oriented cyber physical systems[J]. Journal of Computer Applications, 2014, 34(6): 1770-1773.

参考文献

[1]LEE E A. Cyber-physical systems — are computing foundations adequate? [EB/OL]. [2013-02-15]. http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.84.8011&rep=rep1&type=pdf.
[2]HE J. Cyber physical systems [J]. Communications of the China Computer Federation, 2010,6(1):25-29.(何积丰.Cyber physical systems[J]. 中国计算机学会通讯, 2010,6(1):25-29.)
[3]WANG X, CHEN L, HUANG H, et al. A service-oriented architecture framework of cyber-physical systems [J]. Journal of Computer Research and Development, 2010,47(S2):299-303.(王小乐,陈丽娜,黄宏斌,等.一种面向服务的CPS体系框架[J].计算机研究与发展, 2010,47(S2):299-303.)
[4]TAN P, SHU J, WU Z. An architecture for cyber-physical systems [J]. Journal of Computer Research and Development, 2010, 47(S2):312-316.(谭朋柳,舒坚,吴振华.一种信息—物理融合系统的体系结构[J].计算机研究与发展, 2010, 47(S2):312-316.)
[5]CHEN L, WANG X, DENG S. Cyber physical system architecture design [J]. Computer Science, 2011,38(5):295-300.(陈丽娜,王小乐,邓苏.CPS体系结构设计[J].计算机科学, 2011,38(5):295-300.)
[6]TAN Y, GODDARD S, PREZ L C. A prototype architecture for cyber-physical systems [J]. ACM SIGBED Review, 2008,5(1):51-52.

[7]DERLER P, LEE E A. Modeling cyber-physical systems [J]. Proceedings of the IEEE, 2012,100(1):13-28.

[8]LIN J, SEDDIGH S, MILLER A. Modeling cyber-physical systems with semantic Agents [C]// Proceedings of the 2010 34th Annual Computer Software and Applications Conference Workshops. Piscataway: IEEE Press, 2010:13-18.

[9]TAN Y, VURAN M C, GODDARD S. Spatio-temporal event model for cyber-physical systems [C]// Proceedings of the 2009 29th IEEE International Conference on Distributed Computing Systems Workshops. Washington, DC: IEEE Computer Society, 2009:44-50.

[10]LI L, JIN Z, LI G. Modeling and verifying services of Internet of things based on timed automata [J]. Chinese Journal of Computers, 2011,34(8):1355-1377.(李力行,金芝,李戈.基于时间自动机的物联网服务建模和验证[J].计算机学报,2011,34(8):1355-1377.)

[11]CHEN Z. Modeling and verification of cyber-physical systems based on timed automata [J]. Computer and Modernization, 2012(10):125-130.(陈志辉.基于时间自动机的信息物理融合系统建模与验证[J].计算机与现代化,2012(10):125-130.)

[12]ALUR R, DILL D L. A theory of timed automata [J]. Theoretical Computer Science, 1994,126(2):183-235.

[1]	宗学军韩冰王国刚宁博伟何戡连莲. TDRFuzzer:基于自适应动态区间策略的工业控制协议模糊测试方法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[2]	张明, 付乐, 王海峰. 面向边缘计算的并发数据流接转控制模型[J]. 《计算机应用》唯一官方网站, 2024, 44(12): 3876-3883.
[3]	郑智强王锐棋范子静何发镁姚叶鹏汪秋云姜政伟. DNS隧道检测技术研究综述[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[4]	张立孝马垚杨玉丽于丹陈永乐. 基于命名实体识别的大规模物联网二进制组件识别[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[5]	刘羿希, 何俊, 吴波, 刘丙童, 李子玉. DevSecOps中软件安全性测试技术综述[J]. 《计算机应用》唯一官方网站, 2024, 44(11): 3470-3478.
[6]	庞川林, 唐睿, 张睿智, 刘川, 刘佳, 岳士博. D2D通信系统中基于图卷积网络的分布式功率控制算法[J]. 《计算机应用》唯一官方网站, 2024, 44(9): 2855-2862.
[7]	方介泼, 陶重犇. 应对零日攻击的混合车联网入侵检测系统[J]. 《计算机应用》唯一官方网站, 2024, 44(9): 2763-2769.
[8]	张一鸣曹腾飞. 基于本地漂移和多样性算力的联邦学习优化算法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[9]	徐航, 杨智, 陈性元, 韩冰, 杜学绘. 基于自适应敏感区域变异的覆盖引导模糊测试[J]. 《计算机应用》唯一官方网站, 2024, 44(8): 2528-2535.
[10]	陈虹, 齐兵, 金海波, 武聪, 张立昂. 融合1D-CNN与BiGRU的类不平衡流量异常检测[J]. 《计算机应用》唯一官方网站, 2024, 44(8): 2493-2499.
[11]	耿海军董赟胡治国池浩田杨静尹霞. 基于Attention-1DCNN-CE的加密流量分类方法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[12]	邓淼磊阚雨培孙川川徐海航樊少珺周鑫. 基于深度学习的网络入侵检测系统综述[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[13]	陈瑞龙胡涛卜佑军伊鹏胡先君乔伟. 面向加密恶意流量检测模型的堆叠集成对抗防御方法[J]. 《计算机应用》唯一官方网站, 0, (): 0-0.
[14]	吴中岱, 韩德志, 蒋海豹, 冯程, 韩冰, 陈重庆. 海洋船舶通信网络安全综述[J]. 《计算机应用》唯一官方网站, 2024, 44(7): 2123-2136.
[15]	姚梓豪, 栗远明, 马自强, 李扬, 魏良根. 基于机器学习的多目标缓存侧信道攻击检测模型[J]. 《计算机应用》唯一官方网站, 2024, 44(6): 1862-1871.

面向服务的信息物理融合系统建模与验证

Modeling and verification of services oriented cyber physical systems

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics