[1]周颖,段鹏飞,翟小祥,等.基于DATL的信息物理融合系统安全性建模与验证[J].东南大学学报(自然科学版),2017,47(1):12-17.[doi:10.3969/j.issn.1001-0505.2017.01.003]
 Zhou Ying,Duan Pengfei,Zhai Xiaoxiang,et al.Model and verification of safety of cyber-physical systems based on DATL[J].Journal of Southeast University (Natural Science Edition),2017,47(1):12-17.[doi:10.3969/j.issn.1001-0505.2017.01.003]
点击复制

基于DATL的信息物理融合系统安全性建模与验证()
分享到:

《东南大学学报(自然科学版)》[ISSN:1001-0505/CN:32-1178/N]

卷:
47
期数:
2017年第1期
页码:
12-17
栏目:
计算机科学与工程
出版日期:
2017-01-18

文章信息/Info

Title:
Model and verification of safety of cyber-physical systems based on DATL
作者:
周颖段鹏飞翟小祥李必信
东南大学计算机科学与工程学院, 南京 211189
Author(s):
Zhou Ying Duan Pengfei Zhai Xiaoxiang Li Bixin
School of Computer Science and Engineering, Southeast University, Nanjing 211189, China
关键词:
信息物理融合系统 属性验证 微分时序动态逻辑 微分代数动态逻辑 微分代数时序动态逻辑
Keywords:
cyber-physical systems property verification differential temporal dynamic logic differential-algebraic dynamic logic differential-algebraic temporal dynamic logic
分类号:
TP301
DOI:
10.3969/j.issn.1001-0505.2017.01.003
摘要:
为解决微分时态动态逻辑(dTL)表达能力弱以及微分代数动态逻辑(DAL)缺少时序表达能力的问题,提出了一种结合dTL和DAL的微分代数动态时态逻辑(DATL).采用微分代数程序(DAP)作为操作模型,使DAL具有dTL的时序处理能力.定义了DATL操作模型的DAP和DATL语法,给出了DAP的迹语义和DATL语义,在继承dTL和DAL规则的基础上新增了6个规则.通过对飞机避撞系统安全性的规约和验证,检验了DATL的有效性.
Abstract:
To solve the problem that the expression of the differential temporal dynamic logic(dTL)is weak and the temporality expression of the differential-algebraic dynamic logic(DAL)is lack, a differential-algebraic temporal dynamic logic(DATL)based on the dTL and the DAL was proposed. The differential-algebraic program(DAP)was used as the operating model and the ability of handling temporality of the dTL was introduced into the DAL. The syntax of both the DAP and the DATL formulas were defined. Both the trace semantics of DAP and the semantics of the DATL formulas were presented. The six new rules were added based on the existing rules of dTL and DAL. Finally, the safety of the aircraft collision avoidance system were modeled and verified, proving the effectiveness of the DATL.

参考文献/References:

[1] Lee E A. Cyber physical systems: Design challenges[C]//2008 11th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing(ISORC). Los Angeles,CA,USA, 2008: 363-369. DOI:10.1109/isorc.2008.25.
[2] Beckert B, Schlager S. A sequent calculus for first-order dynamic logic with trace modalities[J]. Automated Reasoning, 2001, 2083: 626-641. DOI:10.1007/3-540-45744-5_51.
[3] Platzer A, Clarke E M. The image computation problem in hybrid systems model checking[C]//International Conference on Hybrid Systems: Computation and Control. Pisa,Italy, 2007: 473-486.
[4] 王中杰,谢璐璐.信息物理融合系统研究综述[J].自动化学报.2011,37(10):1157-1166.
  Wang Zhongjie, Xie Lulu. Cyber-physical systems: A survey[J]. Acta Automatica Sinica, 2011, 37(10): 1157-1166.(in Chinese)
[5] Clarke E M, Emerson E A, Sifakis J. Model checking[J]. Lecture Notes in Computer Science, 1997, 164(2): 305-349.
[6] Henzinger T A. The theory of hybrid automata[C]//1996 IEEE Symposium on Logic in Computer Science. Los Angeles, CA, USA, 1996: 278-292.
[7] Henzinger T A, Nicollin X, Sifakis J, et al. Symbolic model checking for real-time systems[C]//1992 IEEE Symposium on Logic in Computer Science. California, USA, 1992: 394-406. DOI:10.1109/lics.1992.185551.
[8] Alur R. Principles of cyber-physical systems[M]. Cambridge, Massachusetts,USA: MIT Press, 2015: 76-89.
[9] Platzer A. Logical analysis of hybrid systems: Proving theorems for complex dynamics[M]. Berlin, Germany: Springer-Verlag, 2010: 35-86.
[10] Zhai X, Chen Q, Ji S, et al. A unified modeling and verifying framework for cyber physical systems[C]//2012 12th International Conference on Quality Software. Xi’an,China, 2012:23-29.DOI:10.1109/qsic.2012.11.
[11] Xiong G, Zhu F, Liu X, et al, Cyber-physical-social system in intelligent transportation[J]. IEEE/CAA Journal of Automatica Sinica, 2015, 2(3): 221-228.
[12] Lü C, Zhang J, Nuzzo P, et al. Design optimization of the control system for the powertrain of an electric vehicle: A cyber-physical system approach [C]//2015 IEEE International Conference on Mechatronics and Automation. Beijing,China, 2015: 32-40. DOI:10.1109/icma.2015.7237590.
[13] Quaglia D. Cyber-physical systems: Modeling, simulation, design and validation[C]//2013 2nd Mediterranean Conference on Embedded Computing. Budva,Montenegro, 2013: 102-109. DOI:10.1109/meco.2013.6601389.
[14] Kesten Y, Manna Z, Pnueli A. Verification of clocked and hybrid systems[J]. Acta Informatica, 2000, 36(11): 837-912. DOI:10.1007/s002360050177.

备注/Memo

备注/Memo:
收稿日期: 2016-06-12.
作者简介: 周颖(1974—),女,博士,讲师;李必信(1969—),男, 博士,教授,博士生导师,bx.li@seu.edu.cn.
基金项目: 国家自然科学基金资助项目(61572008).
引用本文: 周颖,段鹏飞,翟小祥,等.基于DATL的信息物理融合系统安全性建模与验证[J].东南大学学报(自然科学版),2017,47(1):12-17. DOI:10.3969/j.issn.1001-0505.2017.01.003.
更新日期/Last Update: 2017-01-20