Verifying fragility in digital systems with uncertainties using DSVerifier v2.0

•SMT-based BMC tool to verify systems with uncertainties using fixed-point arithmetics.•Verification of limit-cycle oscillations, stability, and quantization error.•Support for two model checkers as back-end, CBMC and ESBMC.•Support for the SAT/SMT solvers Boolector, CVC4, MathSAT, MiniSAT, Yices, a...

Full description

Saved in:
Bibliographic Details
Published in:The Journal of systems and software 2019-07, Vol.153, p.22-43
Main Authors: Chaves, Lennon C., Ismail, Hussama I., Bessa, Iury V., Cordeiro, Lucas C., de Lima Filho, Eddie B.
Format: Article
Language:English
Subjects:
Bounded model checking
Fixed-point digital controllers
Formal methods
System reliability
Uncertainty
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:•SMT-based BMC tool to verify systems with uncertainties using fixed-point arithmetics.•Verification of limit-cycle oscillations, stability, and quantization error.•Support for two model checkers as back-end, CBMC and ESBMC.•Support for the SAT/SMT solvers Boolector, CVC4, MathSAT, MiniSAT, Yices, and Z3. 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 DSVerifier 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 closed-loop associations of digital control systems (i.e., series and feedback). DSVerifier 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.
ISSN:0164-1212
1873-1228
DOI:10.1016/j.jss.2019.03.015