Trabalho em anais de eventoOpen Access
DSValidator
CHAVES, LENNON; BESSA, IURY; CORDEIRO, LUCAS; KROENING, DANIEL
Resumo
Resumo
We present an automated counterexample reproducibility tool based on MATLAB, called DSValidator, with the goal of reproducing counterexamples that refute specific properties related to digital systems. We exploit counterexamples generated by the Digital System Verifier (DSVerifier), which is a model checking tool based on satisfiability modulo theories for digital systems. DSValidator reproduces the execution of a digital system, relating its input with the counterexample, in order to establish trust in a verification result. We show that DSValidator can validate a set of intricate counterexamples for digital controllers used in a real quadrotor attitude system within seconds and also expose incorrect verification results in DSVerifier. The resulting toolbox leverages the potential of combining different verification tools for validating digital systems via an exchangeable counterexample format.
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
digital system verificationsatisfiability modulo theoriesmodel checkingdigital controllerquadrotor attitude controlMATLAB toolbox
Status
Published
links
Links e arquivos
Trabalho em anais de evento