A Method for Cyber-Physical System Behavior Modeling and Safety Verification Based on Extended Hybrid System Description Language

Ming Fu Tuo; Xing She Zhou; Zheng Xin Guo; Li Jun Shan

doi:10.1051/matecconf/20164402092

A Method for Cyber-Physical System Behavior Modeling and Safety Verification Based on Extended Hybrid System Description Language

Ming Fu Tuo
, Xing She Zhou
, Zheng Xin Guo
, Li Jun Shan

School of Computer Science

Northwestern Polytechnical University Xian
Air Force Engineering University Xian
Hunan University

Research output: Contribution to journal › Conference article › peer-review

1 Scopus citations

Abstract

The safety of Cyber-physical system(CPS) is up to its behavior, and it is a key property for CPS to be applied in critical application fields. A method for CPS behavior modeling and safety verification is put forward in this paper. The behavior model of CPS is described by extended hybrid system description language(EHYSDEL). The formal definition of hybrid program(HP) is given, and the behavior model is transformed to HP based on the definition. The safety of CPS is verified by inputting the HP to KeYmarea. The advantage of the approach is that it models CPS intuitively and verify it's safety strictly avoiding the state space explosion.

Original language	English
Article number	02092
Journal	MATEC Web of Conferences
Volume	44
DOIs	https://doi.org/10.1051/matecconf/20164402092
State	Published - 8 Mar 2016
Event	2016 International Conference on Electronic, Information and Computer Engineering, ICEICE 2016 - Hong Kong, Hong Kong Duration: 26 Apr 2016 → 27 Apr 2016

Access to Document

10.1051/matecconf/20164402092

Cite this

@article{4c86c46f37c54e5298f6af83cf4b7832,

title = "A Method for Cyber-Physical System Behavior Modeling and Safety Verification Based on Extended Hybrid System Description Language",

abstract = "The safety of Cyber-physical system(CPS) is up to its behavior, and it is a key property for CPS to be applied in critical application fields. A method for CPS behavior modeling and safety verification is put forward in this paper. The behavior model of CPS is described by extended hybrid system description language(EHYSDEL). The formal definition of hybrid program(HP) is given, and the behavior model is transformed to HP based on the definition. The safety of CPS is verified by inputting the HP to KeYmarea. The advantage of the approach is that it models CPS intuitively and verify it's safety strictly avoiding the state space explosion.",

author = "Tuo, \{Ming Fu\} and Zhou, \{Xing She\} and Guo, \{Zheng Xin\} and Shan, \{Li Jun\}",

note = "Publisher Copyright: {\textcopyright} Owned by the authors, published by EDP Sciences, 2016.; 2016 International Conference on Electronic, Information and Computer Engineering, ICEICE 2016 ; Conference date: 26-04-2016 Through 27-04-2016",

year = "2016",

month = mar,

day = "8",

doi = "10.1051/matecconf/20164402092",

language = "英语",

volume = "44",

journal = "MATEC Web of Conferences",

issn = "2261-236X",

publisher = "EDP Sciences",

}

TY - JOUR

T1 - A Method for Cyber-Physical System Behavior Modeling and Safety Verification Based on Extended Hybrid System Description Language

AU - Tuo, Ming Fu

AU - Zhou, Xing She

AU - Guo, Zheng Xin

AU - Shan, Li Jun

N1 - Publisher Copyright: © Owned by the authors, published by EDP Sciences, 2016.

PY - 2016/3/8

Y1 - 2016/3/8

N2 - The safety of Cyber-physical system(CPS) is up to its behavior, and it is a key property for CPS to be applied in critical application fields. A method for CPS behavior modeling and safety verification is put forward in this paper. The behavior model of CPS is described by extended hybrid system description language(EHYSDEL). The formal definition of hybrid program(HP) is given, and the behavior model is transformed to HP based on the definition. The safety of CPS is verified by inputting the HP to KeYmarea. The advantage of the approach is that it models CPS intuitively and verify it's safety strictly avoiding the state space explosion.

AB - The safety of Cyber-physical system(CPS) is up to its behavior, and it is a key property for CPS to be applied in critical application fields. A method for CPS behavior modeling and safety verification is put forward in this paper. The behavior model of CPS is described by extended hybrid system description language(EHYSDEL). The formal definition of hybrid program(HP) is given, and the behavior model is transformed to HP based on the definition. The safety of CPS is verified by inputting the HP to KeYmarea. The advantage of the approach is that it models CPS intuitively and verify it's safety strictly avoiding the state space explosion.

UR - https://www.scopus.com/pages/publications/84963616548

U2 - 10.1051/matecconf/20164402092

DO - 10.1051/matecconf/20164402092

M3 - 会议文章

AN - SCOPUS:84963616548

SN - 2261-236X

VL - 44

JO - MATEC Web of Conferences

JF - MATEC Web of Conferences

M1 - 02092

T2 - 2016 International Conference on Electronic, Information and Computer Engineering, ICEICE 2016

Y2 - 26 April 2016 through 27 April 2016

ER -

A Method for Cyber-Physical System Behavior Modeling and Safety Verification Based on Extended Hybrid System Description Language

Abstract

Access to Document

Other files and links

Fingerprint

Cite this