Any-Horizon Uniform Random Sampling and Enumeration of Constrained Scenarios for Simulation-Based Formal Verification
Toni Mancini, Igor Melatti, Enrico Tronci · IEEE Transactions on Software Engineering · 2021
Model-basedapproaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely onnumerical simulationof the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying givenconstraints. Such constraints typically stem fromrequirements(orassumptions) on the SUV inputs and itsoperational environmentas well as from the enforcement ofadditional conditionsaiming at, e.g.,prioritisingthe (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercisingselectedrequirements, or avoidingvacuityin their satisfaction. In this setting, the possibility toefficiently sample at random(with a known distribution, e.g., uniformly) within, or to efficientlyenumerate(possibly in a uniformly random order) scenarios among those satisfying all the given constraints is a key enabler for the practical viability of the verification process, e.g., via simulation-based statistical model checking. Unfortunately, in case of non-trivial combinations of constraints, iterative approaches like Markovian random walks in the space of sequences of inputs in generalfailin extracting scenarios according to a given distribution (e.g., uniformly), and can bevery inefficientto produce at all scenarios that are both legal (with respect to SUV assumptions) and of interest (with respect to the additional constraints). For example, in our case studies, up to 91% of the scenarios generated using such iterative approaches would need to be neglected. In this article, we show how, given a set of constraints on the input scenarios succinctly defined by multiplefinite memory monitors, a data structure (scenario generator) can be synthesised, from whichany-horizon scenariossatisfying the input constraints can beefficientlyextracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enablesseamless support to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to statistical model checking and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative horizon enlargement strategy is defined, as in the spirit of bounded model checking.