Modeling and Verification of Cyber-Physical Systems under uncertainty

Cyber Physical System (CPS) is a hotspot issue which is researched in the current control field for modeling and validation analysis of the complex system. Due to the influence of the uncertain environment on the CPS control dynamic behavior. In this paper, we proposed a possibility spatio-temporal hybrid automata model (PST-hybrid automata) and a formal description language of the CPS software model which is named PoStLTL. Morewhile, the system verification method of the possibility spatio-temporal CPS model is given. Fnally, an example analysis shows this method is valid and describe the verification of CPS on the uncertain environment factors.