Runtime Verification In Uncertain Environments

With the continuous development of human society,the scale of software is becoming more and more complex,and the form is also colorful.But the software crisis is like a shadow devil,often inadvertently causing human losses.Especially in the field of national economy and people’s livelihood,we attach more importance to security.Software deployed in the fields of finance,national defense,aerospace and so on is even more critical to security.How to resist ”devil”? On the one hand,software engineering puts forward a whole set of theories to help people produce according to the standard process in the process of software development;on the other hand,people study various software quality assurance technologies to check whether the produced software is reliable,such as testing,model checking,symbolic execution and other technologies emerge as the times require.Runtime verification technology is also a kind of software quality assurance technology,which is mainly used to monitor whether the running track of the target system conforms to the expected specifications.It can be applied to the software deployment,so it can detect the monitoring requirements related to the running environment.In addition,the runtime verification technology is a lightweight mathematical formal verification method,which is different from the problem that the test technology is difficult to fully cover the complex system path and the possible state guarantee by using the model checking technology.The runtime verification technology only focuses on the monitoring target when The runtime monitor is generated by mathematical formalization of the monitoring specifications,so its judgment result is reliable,and is generally deployed to the monitoring system in the form of automata.In the previous research,some scholars proposed the technology of software proactive monitoring: analyzing the model or code of the target system through the static phase,extracting useful information,so that the running state monitor can actively predict the future system and the satisfaction of the monitoring specifications.This technology enables runtime verification from only finding the alarm after the problem,to realizing the prediction in advance,so as to reserve time for the intervention,so as to avoid the possibility of software failure.Software proactive monitoring technology greatly expands the application space of runtime verification technology.It is because of these four advantages of runtime verification technology: it can be applied to software deployment,lightweight,mathematical formal methods,predictable technology,so it is widely used in all various industriesThis article mainly studies how to improve the quantitative prediction ability of monitoring of temporal properties when the runtime verification method is used in uncertain environments and systems.The specific work and innovations include:(1)In order to improve the ability of runtime verification to predict the violations of properties,model-based methods,program-based analysis methods,etc.have been proposed.But for black-box systems without models and code,and with uncertain behavior,these methods are difficult to apply.In this regard,this paper proposes a method to learn a system’s probabilistic model for determining behavior through machine learning and deploy a runtime probability monitor.First,according to the events in the monitoring specification,a corresponding historical trajectory set is extracted from the log library of the target to be monitored,and then a Markov model conforming to the observation log is constructed from this trajectory library by machine learning.The transition system is generated based on the probability model and specification,and is further integrated into a runtime probability monitor to predict the probability that the target system in the uncertain environment will violate the specification.The advantage of the probability monitor is that it can analyze the possibility of the current system status meeting or violating the monitoring specification in a quantitative manner,so as to predict the tendency of the system to run against the specification.(2)When the runtime verification technology is applied to a distributed system,it is difficult to guarantee the monitoring efficiency because of the event loss due to communication and other issues.When faced with a monitoring specification with timing requirements,the common method is to timestamp the event that occurs at each node,and the monitor makes a centralized decision based on the timestamp of the event.However,for distributed systems,especially dynamic distributed systems where the environment and the spatial location of their nodes are constantly changing,problems such as delay and even packet loss often occur,which is difficult to solve fundamentally.This paper proposes a method for generating a probability monitor for a distributed system based on historical data in the absence of partial event information.This method first generates a probabilistic model based on the monitoring event learning.When the monitor cannot be judged because of missing information,the probabilistic model can help the runtime monitor calculate the possibility of missing information in various positions,so as to obtain the current system state and the satisfaction degree of specifications.Experiments show that this method can effectively improve the monitoring effect for the runtime monitoring of distributed systems,and has strong practicability.(3)The application of runtime verification technology will inevitably increase the overhead of the monitored system.How to effectively reduce the impact of monitoring on the target system is an important research content.This paper proposes a templatebased runtime verification method for some properties with isomorphic characteristics.This method can effectively reduce the redundancy brought by the monitor itself,and can also reduce the impact on the target system when the monitor is inserted into the target system in the form of a plug-in.In addition,a backtracking mechanism is also proposed to optimize the runtime verification process.The backtracking mechanism can reduce the insertion points to the target system for a special type of properties,thereby improving the efficiency of runtime verification.(4)When constructing a probability monitor using the model learning method proposed above,in order to improve the efficiency of model learning,this paper studies an incremental runtime verification method.When constructing a probabilistic model of the target system and uncertain environment,a runtime verification technique based on incremental hidden Markov model construction is proposed,which can be efficiently performed through different models such as single-point data trigger,data-set trigger,and time trigger.The learned model is updated so that the runtime verification can reflect the latest model learning results,and the advantages of the incremental model construction method over the non-incremental method are demonstrated through experiments.