TY - GEN
T1 - Spatio-temporal properties analysis for cyber-physical systems
AU - Shao, Zhucheng
AU - Liu, Jing
AU - Ding, Zuohua
AU - Chen, Mingsong
AU - Jiang, Ningkang
PY - 2013
Y1 - 2013
N2 - Cyber-Physical Systems (CPSs) integrate computing, communication and control processes. Close interactions between the cyber and physical worlds occur in time and space frequently. Therefore, both temporal and spatial information should be taken into consideration when specifying properties of CPS systems for verification. However, how to formulate properties specifying spatial together with temporal features is still an unsolved problem in the CPS. In this paper, we propose an approach to analyze the spatio-temproal properties of CPS. A spatio-temporal logic is developed, including the syntax and semantics of the logic. With that logic, properties of both states, transitions and global systems could be specified, paving the way for further verification. To show the efficiency of the approach, a Train Control System is introduced as a case study. Meanwhile, more details about how to specifying properties of CPS systems with our method are elaborated.
AB - Cyber-Physical Systems (CPSs) integrate computing, communication and control processes. Close interactions between the cyber and physical worlds occur in time and space frequently. Therefore, both temporal and spatial information should be taken into consideration when specifying properties of CPS systems for verification. However, how to formulate properties specifying spatial together with temporal features is still an unsolved problem in the CPS. In this paper, we propose an approach to analyze the spatio-temproal properties of CPS. A spatio-temporal logic is developed, including the syntax and semantics of the logic. With that logic, properties of both states, transitions and global systems could be specified, paving the way for further verification. To show the efficiency of the approach, a Train Control System is introduced as a case study. Meanwhile, more details about how to specifying properties of CPS systems with our method are elaborated.
KW - CPS
KW - property
KW - spatio-temporal logic
KW - specification
UR - https://www.scopus.com/pages/publications/84885201621
U2 - 10.1109/ICECCS.2013.23
DO - 10.1109/ICECCS.2013.23
M3 - 会议稿件
AN - SCOPUS:84885201621
SN - 9780769550077
T3 - Proceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
SP - 101
EP - 110
BT - Proceedings - 2013 International Conference on Engineering of Complex Computer Systems, ICECCS 2013
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 18th International Conference on Engineering of Complex Computer Systems, ICECCS 2013
Y2 - 17 July 2013 through 19 July 2013
ER -