DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems (Tool Demonstration)
For developers of digital systems, DSValidator increases trust in verification results by automatically reproducing counterexamples, but the contribution is incremental as it builds on existing tools.
DSValidator is a MATLAB-based tool that reproduces counterexamples from DSVerifier to validate verification results for digital systems. It validated counterexamples for a real quadrotor attitude system in seconds and exposed incorrect verification results.
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.