DSValidator: an automated counterexample reproducibility tool for digital systems

Conference item

An automated counterexample reproducibility tool based on MATLAB is presented, 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.

Authors: Chaves, L; Bessa, I; Cordeiro, L; Kroening, D

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: Association for Computing Machinery
• Host title: HSCC 2018: 21st ACM International Conference on Hybrid Systems: Computation and Control
• Journal: HSCC 2018
• Pages: 253-258
• Publication date: 2018-04-11
• Acceptance date: 2017-12-19
• DOI: 10.1145/3178126.3178151
• Keywords: digital systems; model checking; MATLAB