Artigo em periódicoOpen Access
Verifying fragility in digital systems with uncertainties using DSVerifier v2.0
CHAVES, LENNON C.2019CHAVES, LENNON C.; ISMAIL, HUSSAMA I.; BESSA, IURY V.; CORDEIRO, LUCAS C.; DE LIMA FILHO, EDDIE B
Resumo
Resumo
Abstract 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.
Autoria
Autores do grupo (2)
A lista completa de autores está no topo da página. Abaixo, apenas os pesquisadores do e-Controls vinculados a esta publicação.
palavras-chave
Palavras-chave
finite word length effectsdigital control systemssoftware model checkingsatisfiability modulo theorieslimit cycle oscillationsclosed-loop feedback system
Volume
153
Páginas
22-43
Editora
Elsevier BV
Status
Published
links
Links e arquivos
Artigo em periódico