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

计算机学院

科研成果: 期刊稿件 › 会议文章 › 同行评审

1 引用（Scopus）

摘要

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.

源语言	英语
文章编号	02092
期刊	MATEC Web of Conferences
卷	44
DOI	https://doi.org/10.1051/matecconf/20164402092
出版状态	已出版 - 8 3月 2016
活动	2016 International Conference on Electronic, Information and Computer Engineering, ICEICE 2016 - Hong Kong, 香港期限: 26 4月 2016 → 27 4月 2016

访问文件

10.1051/matecconf/20164402092

其它文件与链接

链接到 Scopus 的出版物

引用此

@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

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 - http://www.scopus.com/inward/record.url?scp=84963616548&partnerID=8YFLogxK

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

摘要

访问文件

其它文件与链接

指纹

引用此