Survivability Analysis And Verification Method Based On Probability Model Checking

Model checking,which is an important formal verification technology, has achieved great success in the hardware circuit design,protocol verification, and gained wide attention for it’s availability,reliability and automatable.BDDs, symbolic model checking, and the other optimization technologies have largely alleviated the state explosion problem, and make it possible for model checking’s industrialization. Survivability is the description of the hardware/software systems’ ability to withstand disasters and self-recover, and the relative research has become a hot topic of the network filed. The exact definition of survivability is not yet definite, and its definition and analysis method are the main direction of this study field.The paper implements the survivability analysis with model checking techniques,which is a formal analysis of the survivability.1、This paper describes the framework of model checking, and elicits the contents of probabilistic model checking.First we described the three different types of probabilistic model checking in detail, which based on the DTMC, CTMC and PTA models respectively. Then the paper discussed the characteristics of the probabilistic model checking,the ability of expression and the difficulty of implement.2、On that basis, the model checking method for survival is presented.First the definition of survivability apply to model checking is given, and the method to verify the survivability with model checking.Then with the PRISM, the paper built model for telephone access network and verified the survivability. The result’s comparison with the numerical calculation method can prove the correctness of formal methods to analyze the survivability.3、Considering the delay and energy consumption constraints of stochastic system verification, the probabilistic model checking with compensation constraints was proposed here.First the DTMC with reward constraints was proposed, and translated into the equivalent weight graph. Taken the path, which fulfills the rewards, should also have the maximal probability as the principle, and the counterexample’ generation can be converted into the CSP problem on the weight graph. Second state formula and path reward formula should be contained in the extended LTL-x logic, and the probability model checking here own the ability of description and verification for reward. The conversion process keeps the states, which satisfies the constraints, and the corresponding paths invariable.So the solvability of the CSP problem on the weight graph is the proof the feasibility of Probability model checking with reward restrictions.Finally, there is a summary of the paper’s work, which points out the shortage of the paper, and the further work.