On Statistical Model Checking

Model checking offers the possibility to automatically verify the correctness of complex systems or detect bugs. In many practical applications it is also useful to quantify the probability of a property (e.g., system failure), so the concept of model checking has been extended to probabilistic systems. This form is frequently referred to as numerical model checking. To give results with certainty, numerical model checking algorithms effectively perform an exhaustive traversal of the states of the system. In most real applications, however, the state space is intractable, scaling exponentially with the number of independent state variables (the ‘state explosion problem. Abstraction and symmetry reduction may make certain classes of systems tractable, but these techniques are not generally applicable. This limitation has prompted the development of statistical model checking (SMC), which employs an executable model of the system to estimate the probability of a property from simulations. SMC is a Monte Carlo method which takes advantage of robust statistical techniques to bound the error of the estimated result. To quantify a property it is necessary to observe the property, while increasing the number of observations generally increases the confidence of the estimate. Rare properties are often highly relevant to system performance (e.g., bugs and system failure are required to be rare) but pose a problem for statistical model checking because they are difficult to observe. Fortunately, rare event techniques such as importance sampling and importance splitting may be successfully applied to statistical model checking. Importance sampling and importance splitting have been widely applied to specific simulation problems in science and engineering. Importance sampling works by estimating a result using weighted simulations and then compensating for the weights. Importance splitting works by reformulating the rare probability as a product of less rare probabilities conditioned on levels that must be achieved. In this talk, we will introduce Statistical Model Checking and summarize our contributions on importance splitting. Then, we discuss their implementation within the Plasma toolset.