Hybrid Statistical Model Checking Technique for Reliable Safety Critical Systems

Reliability of safety critical systems such as nuclear power plants and automobiles has become a significant issue to our society. As more computing systems are utilized in these safety critical systems, there are high demands for verification and validation (V&V) techniques to assure the reliability of such complex computing systems. However, as the complexity of computing systems increases, conventional V&V techniques such as testing and model checking have limitations, since such systems often control highly complex continuous dynamics. To improve the reliability of such systems, statistical model checking (SMC) techniques have been proposed. SMC techniques can check if a target system satisfies given requirements through statistical methods. In this paper, we propose a new hybrid SMC technique that integrates sequential probability ratio test (SPRT) technique and Bayesian interval estimation testing (BIET) technique to achieve precise verification results quickly. In our experiment, the new hybrid SMC was up to 20% faster than BIET. In addition, we demonstrate the effectiveness and efficiency of this hybrid SMC technique by applying the hybrid SMC technique to three safety critical systems in the automobile domain.