A Modeling and Verification Method of CPS Based on Differential-Algebraic Dynamic Logic

With the wide use of cyber physical systems in industrial control, intelligent transportation system, intelligent medical and other areas, safety has been the core problem of the recent cyber physical systems theory and application research. In this paper, a safety verification method based on differential-algebraic dynamic logic is proposed. The method firstly transforms HybridUML model to differential-algebraic program, then realizes 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. Through the case study of airplane collision avoidance system, it is shown that the method can verify the validity of the collision avoidance manoeuver effectively and guarantee the safety of airplane collision avoidance system.