Automated Verification of Noisy Nonlinear Cyber-Physical Systems with Ariadne

This paper discusses the ongoing work aimed at extending the dynamical model used in Ariadne to differential inclusions, in order to perform reachability analysis in the presence of noisy inputs. While the most straightforward application of differential inclusions is for modeling system uncertainty, it is worth remarking that they can be used also to support contract-based design: given a complex system, we can replace the actual input of a component with an input having partially defined behaviour. The resulting decoupling of components ultimately allows to analyse subsystems in isolation, thus trading-off system complexity for precision. Unfortunately, the introduction of differential inclusions into a nonlinear system represents a challenge in terms of controlling the quality of the computed reachable sets. Such control can be exercised using a number of precision parameters, which should be tuned dynamically for maximum effectiveness. In other words, the successful verification of a noisy system cannot disregard a thorough analysis of such precision parameters and the identification of a proper set of policies for their automated control.