Research On Safety Verification Of Cyber-Physical Systems

Safety issues begin with system modeling and continue throughout the entire life cycle of cyber-physical systems consisting of system analysis, design, development and maintenance. The safety problem widely exists in cyber-physical system and is rich in content as well as diverse in form. This paper is based on the perspective of system dynamics, through modeling the dynamical process of cyber-physical system as hybrid dynamical system, safety problem of cyber-physical system is formally interpreted as determination of whether trajectories of hybrid system intersect with specified unsafe states set.There are many stages in the life cycle of cyber-physical system, each of which includes several distinguished scenarios. Safety problems have various forms in real ap-plications, though, they are unified in essence in the context of cyber-physical system. The premise of the research of safety verification of cyber-physical system is to grasp the key factors in system's safety and abstract a reasonable verification scenario. Generally speaking, behavior, control and structure of the system are important factors the affect the safety of cyber-physical system. In view of this, safety verification of cyber-physical system could be attributed to safety verification of the corresponding hybrid system under certain behavioral, control or structural mechanisms.It is in line with that understanding, this dissertation will study cyber-physical sys-tem as the background and then be committed to the theory as well as methods of formal safety verification of the corresponding hybrid system under specific behavioral, control or structural assumptions. Continuous evolution, impulsive jumps and mode switchings are three basic forms of behavior of hybrid systems, furthermore, interaction between them constitutes the behavioral mechanism. Towards safety verification of behavioral mechanism of hybrid systems, we introduce barrier certificates theorem and the construc-tion theorem on barrier certificates as the core of corresponding formal methods. Two ba-sic forms of hybrid control are closed-loop feedback control and open loop control, which are subordinating to either states or time constraints correspondingly. Towards safety ver-ification of mode-dependent dwell time driven switching mechanism as well as interval dwell time driven switching mechanism, two theorems on barrier certificates along with their corresponding constructions are proposed to develop relevant formal theories and methods. Interconnected switching system and interconnected impulsive system are two basic forms of interconnected hybrid systems. Towards safety verification of those two cases, corresponding barrier certificates as well as their constructions are proposed, which provide a complete solution from theoretic principles to feasible algorithms.This research takes safety verification of mode-dependent dwell time driven switch-ing policy, interval dwell time driven switching policy, interconnected switching system as well as interconnected impulsive system as the core, and further advance the research on safety verification of cyber-physical systems from following four aspects:Firstly, toward safety verification of hybrid systems under some specific behavioral mechanism, formal definition on behaviors is presented, and then theorem on barrier cer-tificates is given which proves the sufficiency of the existence of a barrier function to safety of the corresponding hybrid system. Furthermore, relevant theories, issues on numerical computations as well as support softwares are introduced for the purpose of constructing such barrier functions.Secondly, toward safety verification of hybrid systems under some specific control mechanism, this dissertation focuses on the time-driven case. Through giving sufficient conditions for safety of both mode-dependent dwell time driven hybrid system and inter-val dwell time driven hybrid system, corresponding theorems on barrier certificates are proposed. Furthermore, theorems about constructing barrier certificates are also proposed with emphasis on time driven control mechanism to reduce their computational complex-ity.Thirdly, toward safety verification of hybrid systems under some specific intercon-nection structure, this dissertation focuses on interconnected switching system and inter-connected impulsive system cases. Through introducing constraints satisfying dissipation-like-inequality and small-gain characteristics, sufficient conditions for safety of those two cases are presented in the forms of theorems on corresponding barrier certificates. Fur-thermore, theorems for the construction of such barrier certificates are also proposed to promote the implementation of automated verification.In the end, a kind of following control mechanism using front and back information based on vector Lyapunov function is verified to be safe following the idea of barrier certificates.