Abstract: Because the cyber-physical system(CPS) hardware integration and software involvement in degree rise ceaselessly,many software and hardware have heterogeneous connectivity and mutual control．The analysis design,modeling of CPS have become more and more difficult．In this paper,a safety verification method based on 1abeled hybrid Petri net and differential-algebraic dynamic logic was proposed．The method firstly transforms LHPN model to differential-algebraic program,then realizas the specification of system safety using differential-algebraic program,and finally the cyber physical systems safety is verified according to differential-algebraic program reasoning rules．It is effectiveness for the method through an instance of the prototype application.

Key words: Labeled hybrid Petri net,Cyber physical system,Modeling,Verification