An Approach Of Incremental Probabilistic Model Checking For Runtime System

With the rapid development of computer technology,computer systems are becoming larger and more complex.Many practical systems are endowed with stochastic behavior characteristics.We need to use model checking to automatically verify the stochastic system and quantitatively analyze its properties,this is the probabilistic model checking.Probabilistic model checking is the generalization of classical model checking theory and is widely used to verify the qualitative and quantitative properties of computer systems with stochastic behavior.Computer systems analyzed in the probabilistic model checking include adaptive software systems,these systems change dynamically during their life cycle.In order to verify such systems at runtime,a runtime probabilistic model checking is proposed.An important challenge in many aspects of run-time probabilistic model checking is its performance.It should respond to run-time requirements fast enough to continuously verify whether the current system meets the system requirements when the run-time system changes dynamically.In this paper,we propose an incremental probabilistic model checking method for the runtime system,which is used in the calculation of the reachability probability for stochastic model at runtime.The main feature of the incremental probabilistic model checking method for runtime system proposed in this paper is the combination of two heuristic methods to improve its performance during the verification process of the runtime probabilistic model checking.These two heuristic methods reduce the number of numerical iterations during the verification process by reusing the reachability probabilistic values from the previous model and reordering the state after the model changes,thereby accelerating the process of calculating and improving the efficiency of the runtime probabilistic model checking.Note that the work in this paper is focused on improving the efficiency of stochastic system verification where the model has some changes during runtime.Our research focus is on the improvement of probabilistic model checking method for the runtime system,regardless of the choice of the runtime verification method.We added our heuristic methods to the model verification tool PRISM,and used three types of benchmark case models in PRISM for experiment.In the experiment,we used discrete time Markov chain(DTMC)to represent the system model,and used probabilistic time tree logic(PCTL)to describe the reachability property that need to be verified.The results of experiment showed that,under the default experimental parameter settings,our incremental probabilistic model checking method for runtime can shorten the verification time of standard runtime probabilistic model checking to more than 40%.The main work and contributions of this paper are as follows:1 Analyzed the principle of the existing runtime probabilistic model checking,and in order to deal with the situation where the stochastic system changes at runtime,we combined two heuristic methods during the runtime probabilistic model checking process,and proposed an incremental probabilistic model checking method for runtime.2 The first heuristic method was incremental value iteration.The heuristic method was based on Gauss-Seidel iteration,and calculation results of the initial DTMC model probabilistic values were used as the initial values for calculation of the changed DTMC model.3 The second heuristic method was to reorder the states after model changes.Find a better state order according to the changes of model in the process of numerical iteration to reduce the number of iterations in the model checking.