Towards Verifying Robotic Systems Using Statistical Model Checking in STORM

Robust autonomy and interaction of robots with their environment, even in rare or new situations, is an ultimate goal of robotics research. We settle on Statistical Model Checking (SMC) for the benefit of robustness of robot deliberation and base our implementation on STORM, one of the most performant and comprehensive open-source model checkers, so far lacking an SMC extension. The SMC extension introduced in this paper offers various statistical methods, from which the user can choose to find the best trade-off between accuracy of the result and runtime. We demonstrate the efficiency of our SMC implementation by comparing it to other state-of-the-art SMC tools on well-established benchmarks and on a robotics-related example. The results indicate that our implementation, which will be continuously extended in the future to improve support for robotics use cases, is performant enough to bridge the gap between robotic systems and model checking in industry.