Behavior Modeling and Attribute Validation of Cyber Physical System (CPS)Based on Hybrid Automata
TUO Mingfu
ZHOU Xingshe
LI Jialin
LI Hui
Abstract：Non?function attribute such as real?time,security,and reliability,etc.is a key factor in cyber?physical systems applied to many areas.On the basis of analyzing CPS modeling and verification,a CPS behavior modeling and attribute verification is proposed in this paper.In this method,three steps are as follows:(1)to model the behavior of CPS based on hybrid automata;(2)to convert this model to HP model;(3)to verify the HP model in KeYmarera.The structure of behavior model language is introduced. Rules of converting hybrid automata model to hybrid program (HP)model are established.The consisten-cy of the conversion is analyzed.The result shows that this method can depict the behavior of CPS simply and intuitively,and can also verify the properties of CPS strictly.By doing so,this avoids state space ex-plosion in formal verification effectively.
Keywords：cyber?physical system (CPS)model verificationhybrid automatahybrid program (HP)model conversion
Publication Date：2016-01-01
Online Publishing Date：2025-08-15(First online date of this platform, not the publication date of the document)
Pages：5( 40-44 )