CPS Modeling And Analysis Based On Uncertain Spatiotemporal Logic

Due to the rapid development of embedded technology,computer technology and the performance of hardware products,as well as the continuous improvement of the performance and the data processing ability,some technologies have been developed by leaps and bounds,such as the Internet of things technology.Under the background,Cyber-Physical Systems(CPS)came into people's vision,and has been paid attention to by governments and people from all walks of life and has become a new kind of embedded network system.CPS is a comprehensive system that combines physics,biology and engineering with local control and regional control,CPS is the physical,biological and engineering fusion in integrated system with local control and the control of the network,this new system has aroused great interest in the research community,also is a kind of important development direction of the future communication network.CPS is often used in a number of areas of high security requirements,such as infrastructure monitoring and control,national defense and weapons systems,medical and intelligent transportation and so on.CPS has been able to get the favor of academia,on the one hand is its application in modeling.In the CPS system modeling should not only consider the time information,also should consider the spatial information,and the traditional embedded methods are only concerned with one aspect of these information,this obviously does not meet the complex communication requirements in the CPS system.Therefore,we need to consider how to describe the time and space information in the Cyber-Physical Systems and its modeling.Although the automaton can effectively model the discrete and continuous behavior of the CPS system in the aspect of system modeling,it can't effectively represent the location related information,especially the spatial constraints is described.In this way,the scholars consider to extend the existing hybrid systems in terms of spatial variables and spatial expressions in order to improve the ability of modeling.In this paper,we devotes to the research of uncertain CPS modeling and attribute verification and takes into account the uncertainty of the environment,and then considers the impact of environmental uncertainty on CPS software operation and dynamic verification.On the basis of intensive studying possibility measure and spatio-temporal logic,the possibility spatio-temporal hybrid automaton model is proposed,the possibility spatio-temporal CPS software architecture model is given and the CPS architecture model is built.In view of the influence of the uncertain environment on the CPS control dynamic behavior,a formal description language of the CPS software model which is named possibility spatio-temporal LTL(PoStLTL)is presented,meanwhile,possibility possibility spatio-temporal responsiveness and the possibility spatio-temporal ?-regular security are given for verifying system attributes.As a result,the feasibility of the verification methods is verified by inspecting a representative application and analyzing the responsiveness and ?-regular security attributes of the CPS control system under the uncertain environment.