@Article{Mancini_etal2021,
author="Mancini, T.
and Melatti, I.
and Tronci, E.",
title="Any-horizon uniform random sampling and enumeration of constrained scenarios for simulation-based formal verification",
journal="IEEE Transactions on Software Engineering",
year="2021",
pages="1",
abstract="Model-based approaches to the verification of non-terminating Cyber-Physical Systems (CPSs) usually rely on numerical simulation of the System Under Verification (SUV) model under input scenarios of possibly varying duration, chosen among those satisfying given {\textit{}constraints{}}. Such constraints typically stem from {\textit{}requirements{}} (or {\textit{}assumptions{}}) on the SUV inputs and its {\textit{}operational environment{}} as well as from the enforcement of {\textit{}additional conditions{}} aiming at, e.g., {\textit{}prioritising{}} the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising {\textit{}selected{}} requirements, or avoiding </i>vacuity</i> in their satisfaction. In this setting, the possibility to {\textit{}efficiently sample at random{}} (with a known distribution, e.g., uniformly) within, or to efficiently {\textit{}enumerate{}} (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 general {\textit{}fail{}} in extracting scenarios according to a given distribution (e.g., uniformly), and can be {\textit{}very inefficient{}} to 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 multiple {\textit{}finite memory monitors{}}, a data structure ({\textit{}scenario generator{}}) can be synthesised, from which {\textit{}any-horizon scenarios{}} satisfying the input constraints can be {\textit{}efficiently{}} extracted by (possibly uniform) random sampling or (randomised) enumeration. Our approach enables {\textit{}seamless 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.",
optnote="To appear",
optnote="exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=191), last updated on Mon, 06 Sep 2021 19:27:54 +0200",
issn="1939-3520",
doi="10.1109/TSE.2021.3109842",
opturl="https://doi.org/10.1109/TSE.2021.3109842",
file=":http://mclab.di.uniroma1.it/publications/papers/mancini/2021/191_Mancini_etal2021.pdf:PDF"
}