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, 48(10), pages 4002-4013, 2022.

Toni Mancini, Igor Melatti, Enrico Tronci.
Any-horizon Uniform Random Sampling and Enumeration of Constrained Scenarios for Simulation-based Formal Verification.
IEEE Transactions on Software Engineering, 48(10), pages 4002-4013, 2022.
DOI: 10.1109/TSE.2021.3109842

BibTex entry

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 constraints. Such constraints typically stem from requirements (or assumptions) on the SUV inputs and its operational environment as well as from the enforcement of additional conditions aiming at, e.g., prioritising the (often extremely long) verification activity, by, e.g., focusing on scenarios explicitly exercising selected requirements, or avoiding vacuity in their satisfaction.

In this setting, the possibility to efficiently sample at random (with a known distribution, e.g., uniformly) within, or to efficiently 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 fail in extracting scenarios according to a given distribution (e.g., uniformly), and can be 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 the case studies addressed in this article, up to 91% of the scenarios generated using such iterative approaches would need to be neglected.

We showed how, given a set of constraints on the input scenarios succinctly defined by multiple finite memory monitors, a data structure (scenario generator) can be synthesised, from which any-horizon scenarios satisfying the input constraints can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration.

Results

  • Finite State Machines (FSMs) exploited as a succinct, flexible, and practical means to compositionally define (as monitors) requirements about legal scenarios on which the SUV shall be exercised, as well as additional constraints aiming at restricting the focus of the verification process (e.g., for prioritisation needs, or to exercise some requirements avoiding vacuity in their satisfaction)
  • Showed how, by exploiting and combining together results from supervisory control theory and combinatorics, we can synthesise, in a few seconds, a data structure (Scenario Generator) from which any-horizon scenarios entailed by a monitor, or a combination thereof, can be efficiently extracted by (possibly uniform) random sampling or (randomised) enumeration
  • Seamless support provided to virtually all simulation-based approaches to CPS verification, ranging from simple random testing to SMC and formal (i.e., exhaustive) verification, when a suitable bound on the horizon or an iterative/dynamic horizon enlargement strategy is defined, as in the spirit of bounded model checking.