Bayesian Statistical Model Checking For Complex Stochastic Systems

As Internet technologies step into maturity, they accelerate the development of Internet infrastructures, applications and services, such as mobile Internet, cloud computing and so on. They permeate into every corner of people’s daily life. More and more infrastructures and applications will be built on networks. Investigating how to ensure their correctness and stableness is valuable. Different from other software or hardware systems, network systems contain stochastic behaviors. Testing is applied widely in industry to accomplish this object, but it still contains some deficiencies, such as not being able to find out all of the bugs and being closely related to testers’ experience.To ensure correctness and stableness of complex stochastic systems, we propose a prediction-based Bayesian statistical model checking approach-PBMC. If we randomly sample a finite path from the initial state in a model, and repeat this procedure, then we get independent paths. If we regard them as samples, then we are able to infer the probability of the model satisfying for a property.Furthermore, utilizing conjugate relation between prior distribution and posterior distribution in Bayesian Statistics, we can predict the size of samples needed. And requirements on confidence and precision of result are sure to be satisfied when the number of samples reaches this size. Secondly, according to prediction, we can utilize conjugate relation again to predict all of the possible results after statistics have been updated. If all the predicting results consent to current result, it will be returned as final result directly.To enhance the efficiency of verifying one type of systems (long-term running stochastic systems), we proposed another heuristic sampling and verifying algorithm. It separates sampling and verification into two steps:In verification, we use an algorithm to find out a "decidable" path prefix. And this prefix is able to determine whether the path satisfies the property. Then, in the following sampling steps, we may be able to directly determine whether the path satisfies the property. Moreover, this approach can be integrated with PBMC.SPAC (Statistical Probabilistic Approximate model Checker) is a statistical model checker which implements several approaches above. We verify scheduling algorithm and distributed algorithms with SPAC. It shows that PBMC is more efficient than APMC and SPRT in some cases. Especially, for long-run term stochastic systems, heuristic algorithms can further enhance the efficiency of verification.