Verifying Fragility in Digital Systems with Uncertainties using DSVerier v2:0

Control-system robustness verification with respect to implementation aspects
lacks automated verification approaches for checking stability and performance
of uncertain control systems, when considering finite word-length (FWL) effects.
Here we describe and evaluate novel verification procedures for digital systems
with uncertainties, based on software model checking and satisfiability modulo
theories, named as DSVerier v2:0, which is able to check robust stability of
closed-loop control systems with respect to FWL effects. In particular, we
describe our verification algorithms to check for limit-cycle oscillations (LCOs),
output quantization error, and robust non-fragile stability on common closedloop associations of digital control systems (i.e., series and feedback). DSVerier v2:0 model checks new properties of closed-loop systems (e.g., LCO), including stability and output quantization error for uncertain plant models, and considers unknown parameters and FWL effects. Experimental results over a large set of benchmarks show that 35%, 34%, and 41% of success can be reached for stability, LCO, and output quantization error verification procedures, respectively, for a set of 396 closed-loop control system implementations and realizations.