Research On The Probabilistic Model Checking Problem On Real Time Systems

With the increasing use of real-time systems,the reliability requirements of realtime systems are becoming higher and higher.The evaluation of the function,performance and reliability of real-time systems has become an important research topic.As an important approach to improve the credibility of software,probabilistic model checking can conduct formal verification of software and hardware systems automatically and give the attribute analysis results from a quantitative aspect of view.The main work of this dissertation is to study the theoretical framework of probabilistic model checking for real-time systems and suggest a solution for probabilistic model checking for real-time systems,so as to explore the further application of probabilistic model checking technology.Because of the particularity of the real-time systems,it is very difficult to perform probabilistic model checking for real-time systems.In summary,real-time systems have three major characteristics: real-time,self-stability and interactivity.Firstly,because of the real-time systems' real-time response characteristics,the behaviors of real-time system models often change continuously with time.The fundamental characteristic of this kind of models is that their state space is infinite.However,probabilistic model checking technology is only applicable to finite state space models,so it is almost impossible to implement probabilistic model checking for real-time systems.Secondly,real-time systems have the characteristics of selfstabilization,that is,without external interference,real-time systems can automatically migrate from an unstable state to a stable state.The performance of the self-stabilization algorithms,which govern the self-stabilization process of real-time systems,becomes a key factor of restricting the performance of real-time systems.Thirdly,the real-time systems will always interact with the working environment or users.To evaluate the performance and reliability of real-time systems,people should not consider real-time systems themselves unilaterally;instead,we should restore its real usage environment as far as possible and put real-time system models under the background of interacting with the working environment or potential users.The main contents and innovative achievements of this dissertation can be summarized as follows:Firstly,due to the fact that real-time system models present infinite state space,the semantic rule of discretizing the probabilistic models of real-time systems is proposed.This rule can discretize probabilistic time automaton models of real-time systems which have infinite state space and transform them into Markov decision process models of finite state space on the basis of maintaining real-time attributes.The upper and lower boundaries of attribute probabilities can be calculated based on Markov decision process model.However,the current researches only focuse on the probabilistic time automaton model itself.The quantitative calculation of attributes starts from the initial state(or target state)of the model and reaches the target state(or initial state)forward(or backward).Such methods can only present a single boundary of the probability value(i.e.,maximum or minimum).Secondly,aiming at the state space explosion problem that Markov decision process model may face,this dissertation proposes a series of abstract-refinement algorithms with the background of probability for the first time.The purpose is to mitigate or eliminate the impact of state space explosion on probabilistic model checking.The state space of the model is partitioned adaptively.The criterion of state cluster is the probability of reaching the target states,not the similarity based on the transition relations.This is an improvement and innovation in abstraction-refinement technique under the background of qualitative analysis,which takes the similarity of migration relations as the abstract standards.When the abstract model is refined,the criterion is whether the difference of upper and lower bounds of the probabilities of reaching the target state exceeds a given accuracy.Different from other abstract refinement technologies,abstract refinement process does not concencrate on abstract models entirely,but takes concrete models into account.Thirdly,aiming at the self-stabilization characteristics of real-time systems,the performance analysis of self-stabilization algorithms governing the self-stabilization process of real-time systems is carried out in a prescriptive manner by using probabilistic model checking technology.Compared with the existing performance evaluation methods of self-stabilization algorithms,the proposed method strictly restricts the self-stabilization state set to be a true subset of all configuration sets,rather than a subset of all configuration sets.This restriction is closer to the actual working scenarios of self-stabilization algorithms.After the analysis,this dissertation finds out the main factors affecting the performance of the self-stabilization algorithm,they are : the probability of token transfer,token distribution,the number of tokens per host and the number of hosts.Fourthly,in view of the inadequacy of Markov decision process model in describing real-time systems' concurrency and interactions with the working environment,this dissertation proposes a scheme that further abstracts Markov decision process model into a stochastic player game model,and proposes an abstractrefinement framework for the stochastic player game model.Because the Markov decision process model has limited ability to model concurrency,and it can not describe the interaction between real-time system and its working environment,it can only describe the interaction behavior unilaterally as the uncertain choices of the model,which makes the model can not describe the actual behavior of real-time system completely and accurately.The proposed modeling rules support the modeling of the behaviors on both sides of the interaction.This can ensure that the formal verification conditions are closer to the actual working environment of real-time systems further and more accurate verification results can be obtained.In addition,an abstract refinement framework for stochastic player game model is proposed by this dissertation for probabilistic model checking of models with larger state space.