DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems (Tool Demonstration)

TL;DR

DSValidator is an automated MATLAB tool that reproduces counterexamples from digital system verifications, enhancing trust and exposing errors in verification results for digital controllers, demonstrated on a quadrotor system.

Contribution

Introduces DSValidator, a MATLAB-based tool that automates counterexample reproduction for digital systems, improving verification reliability and interoperability.

Findings

Validates complex counterexamples in seconds

Exposes incorrect verification results in DSVerifier

Enhances trust in digital system verification

Abstract

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.