Formal Modeling And Dynamic Verification For Human Cyber Physical Systems Under Uncertain Environment

With the advancement of technology,new complex systems such as Human Cy-ber Physical Systems(HCPS)have become more and more inseparable from human social life.The information space where the software system is located and the phys-ical space where people's daily lives are gradually merging.Uncertain factors such as the complex and changeable environment in the physical space,the explosive growth of spatio-temporal data and unpredictable human behavior threaten the security of the system.Following this,issues such as the surge in security requirements for software systems,the extended scope of responsibility,the expanded scale,and complexity are urgently to be resolved.Therefore,in an uncertain environment,modeling and verifica-tion methods for constructing intelligent and safe human-machine fusion systems and tool chain platform development have become inevitable challenges for the software industry.Uncertainty of the environment makes the software of the human cyber physical system unable to accurately perceive its operating environment.Perceived uncertainty will lead to misjudgment of the system,thus affecting the security of the system.Un-certainty in the environment prevents system designers from providing accurate formal specifications for the operating environment of the ergonomic system software.For systems with high security requirements,accurate formal specifications are the primary condition for ensuring system security.In order to cope with the uncertainty of the protocol,this thesis proposes a combination of spatio-temporal data-driven and model-driven modeling,that is,the use of machine learning algorithms to model the envi-ronment based on spatio-temporal data in the environment rather than based on formal protocols.According to the typical characteristics of security software,a parametric modeling language with hierarchical characteristics is designed,and the security of the system is guaranteed by dynamic verification,so as to build a unified security theoreti-cal framework.This thesis takes the theoretical framework and application of building a safe and intelligent human-machine fusion system as the main research goal.· Aiming at the uncertainty of the physical environment in which the system is located,applying machine learning technology and driven by the spatio-temporal data in the environment,a perception model under uncertain environment is pro-posed.Including human behavior classification model based on decision tree and environmental risk prediction model based on LSTM recurrent neural network.· The parameterized modeling language stohChart(p)with hierarchical features is defined,and the formal definitions of corresponding syntax and semantics are given.A mapping algorithm that converts the model into a random hybrid automa-ton(SHA)is proposed.· A dynamic verification method for uncertain models is proposed,and the dy-namic verification of the model is realized by the verification tool UPPAAL-SMC,so as to quantitatively evaluate the impact of the uncertain environment and human behavior on the system security.