The Research Of Model Checking Methods For Complex Stochastic System

With the rapid development of information technology,a variety of software and hardware systems occupy an increasingly important position in social life,so system safety and reliability become more important.The functional correctness and performance satisfiability of the system are increasingly becoming the hot topics to which the academic communities pay close attention.Using effective means to verify whether the functional and performing features of the system meet the requirements has become a very important research topic.Formal method is considered as one of the feasible and effective methods in credibility assessment of system performance.In which,model checking technology is widely used because of its advantages such as high degree of automation and rigorous mathematical foundation.The research hot spots of model checking include hardware verification,protocol analysis and some other fields and are gradually shifted to software verification.Model checking is initially focused on qualitative analysis of system behavior but now it is turning to the verification of complex parameter properties,which combines the qualitative analysis and the quantitative analysis.For the complex stochastic system containing many kinds of parameter features,the most important issue of model checking is how to accurately model the system and effectively characterize the features of system.Besides,the state space explosion problem occurring in the traditional modeling checking techniques,efficient properties verification algorithm of complex stochastic system and valid representation and comprehension of counterexample information become new obstacles to further application and development of complex stochastic system model checking techniques.Therefore,further study on the model checking theory and its application on complex stochastic system verification have high theoretical and practical value.The following work has been carried out in this thesis aiming to the main problems of the model checking faced in the aspect of complex stochastic system verification.(1)An improved new continuous stochastic logic named aCSRL was proposed to describe properties of the complex stochastic system and the corresponding model representation,named CTMRDP,was given after comprehensive comparative analysis of all kinds of existing temporal logics and model representation methods in model checking techniques.Then how to strictly express the dynamic behavior of the complex stochastic system model by aCSRL was described in detail.At last,it is proved that the expression ability of aCSRL strictly stronger then the relevant other continuous stochastic logics through the comparative analysis of aCSRL and existing relevant temporal logics for describing complex stochastic systems properties.(2)The aCSRL properties verification methods for complex stochastic system CTMRDP model were proposed.Among them,the solution process of aCSRL steady state probability formula and concrete instance analysis were all given by using the method similar to CSL model checking through characteristic elimination,strongly connected sub graph structure and other steps.For aCSRL transient probability state formula,first the automata representation of aCSRL path formula was given based on automata theory after analyzing the structure of the path formula in aCSRL transient probability state formula,then the definition of the synchronous automata model of path formula automata and system model was described based on the methods in traditional LTL model checking and the quantitative validation methods of properties with the time and reward characteristic constraints based on synchronous automata model,and the corresponding algorithm was described.At last,we proved the feasibility and effectiveness of the aCSRL temporal logic property verification method on complex stochastic system model through case analysis.(3)For discrete probability reward model,the logic semantics of multi until constrain path formula and the corresponding conditional probability state formula were proposed first,then we proposed the corresponding formula property verification methods and gave the case studies.At last compressed representation of regular expression of discrete probability reward model counterexample and counterexample automaton model representation methods were given.On the one hand,we gave formula automata construction method and property verification method based on synchronous automata model.On the other hand,discrete probability reward model was transformed into weighted directed graph,then quantitative validation algorithm of multi until constrain path formula and the corresponding conditional probability state formula were given using the iterative solution method and the effectiveness of the algorithm was proved by case study.(4)For the state space explosion problem in the complex stochastic system model property validation process,one state space reduction method applied in Markov reward model was proposed.First we gave the matrix representation of the model by symbols encoding.Then combining symmetric reduction technology and bissimulation theory,the model reduction algorithm was given based on state transition matrix by analyzing the equivalence relationship of original model and unique representation function of equivalence class.At last we proved effectiveness of the method through case study.The method can be easily applied to other complex stochastic system models after appropriate improvements and can effectively alleviate the state space explosion problem in model checking process.