On Optimizing Simulation-Based Verification of Cyber-Physical Systems via Statistical Model Checking: a Preliminary Work

Exhaustive simulation-based verification of safety/mission-critical systems often requires unviable overall completion times due to the unmanageable number of operational scenarios to be considered. Statistical Model Checking (SMC), instead, entails randomly evaluating scenarios deemed of interest until statistical guarantees are achieved. In this short paper, we gather on estimating expected value approximations of system-level properties through Adaptive Stopping Algorithms (SAs), a particular class of SMC that learns the number of scenarios to be considered. Our analysis shows that determining upfront the algorithm that will require the fewest samples for the verification task at hand would be greatly beneficial, as it would allow significant reductions in the overall time. However, although qualitative criteria have been proposed to guide the choice of the right algorithm, its actual performance may depend on unknown information (e.g., the actual value to be estimated).