Application Of Assume-guarantee Reasoning In Compositional Stochastic Model Checking

Model checking is an automatic and complete formal verification method.For the finite state system and the temporal logic formula,model checking can determine whether the given system model satisfies the logical description of the property or specification in the formula.It can also provide counterexamples when the system model does not satisfy the property specification.Stochastic model checking is the extension and generalization of classical model checking,which can be used for quantitative verification of stochastic systems based on the model.Stochastic model checking algorithms rely on a combination of model checking techniques for classical model checking and numerical methods for calculating probabilities.So,stochastic model checking faces more severe state explosion problem.In the application of stochastic model checking,how to alleviate the state explosion problem is becoming a key challenge.The main contributions of the research are as below:(1)This paper first applies the symmetric assume-guarantee rule(SYM)into stochastic model checking for two-component systems.At the same time,based on NL* learning algorithm,a SYM-NL framework is proposed for compositional stochastic model checking of Probabilistic automata(PA).(2)We also optimize the existed compositional stochastic model checking process,so that it can get the verification results faster when the system model does not satisfy the probabilistic safety property,and avoid some unnecessary losses caused by errors.(3)The rule SYM is extended to SYM-n that can be used to check multi-component systems,and we also extend the above framework to support the rule SYM-n.In this paper,for assume-guarantee compositional stochastic model checking method(AG-CSMC),the generation of assumption is an iterative learning process.By reducing the number of iterations in the learning process,we improve the operation efficiency of the algorithm.Based on PRISM,we design a prototype tool to verify several large-scale cases,including sensor network model,client-server model,and randomized consensus algorithm model.The purpose of the experiment is divided into three aspects:(1)verify whether the method of this paper is feasible;(2)verify whether our optimization is effective in the learning process;(3)verify whether the rule SYM-n is more advantageous than SYM.Experimental results show that our prototype tool can successfully verify all the cases.Compared with the existing method,our prototype tool requires less time to obtain the verification results when the model does not satisfy the properties.In addition,through the comparative experiment between the rule SYM and SYM-n,we find that the rule SYM-n is obviously superior to SYM for large-scale cases.