research-article

Open access

DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems

Authors:

Lucas Cordeiro,

Daniel KroeningAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 253 - 258

https://doi.org/10.1145/3178126.3178151

Published: 11 April 2018 Publication History

Abstract

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.

References

[1]

R. B. Abreu, M. Y. R. Gadelha, L. C. Cordeiro, E. B. de Lima Filho, and W. S. da Silva. Bounded model checking for fixed-point digital filters. Journal of the Brazilian Computer Society, 22(1):20, 2016.

[2]

P. Bauer and L.-J. Leclerc. A computer-aided test for the absence of limit cycles in fixed-point digital filters. IEEE Trans. Signal Processing, 39(11):2400--2410, Nov 1991.

Digital Library

[3]

I. Bessa, H. Ismail, L. Cordeiro, and J. Filho. Verification of fixed-point digital controllers using direct and delta forms realizations. Design Autom. for Emb. Sys., 20(2):95--126, 2016.

Digital Library

[4]

I. Bessa, H. Ismail, R. Palhares, L. Cordeiro, and J. E. C. Filho. Formal non-fragile stability verification of digital control systems with uncertainty. IEEE Transactions on Computers, 66(3), 2017.

Digital Library

[5]

D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, and A. Stahlbauer. Witness validation and stepwise testification across software verifiers. In ESEC/FSE, pages 721--733, 2015.

Digital Library

[6]

D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In CAV, volume 6806 of LNCS, pages 184--190, 2011.

Digital Library

[7]

S. Bouabdallah, P. Murrieri, and R. Siegwart. Design and control of an indoor micro quadrotor. In ICRA, volume 5, pages 4393--4398 Vol.5, April 2004.

[8]

J. Carletta, R. Veillette, F. Krach, and Z. Fang. Determining appropriate precisions for signals in fixed-point IIR filters. In DAC, pages 656--661, 2003.

Digital Library

[9]

L. Chaves, I. Bessa, L. C. Cordeiro, D. Kroening, and E. B. de Lima Filho. Verifying digital systems with MATLAB. In ISSTA, pages 388--391, 2017.

Digital Library

[10]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In TACAS, volume 2988 of LNCS, pages 168--176, 2004.

[11]

L. Cordeiro, B. Fischer, and J. Marques-Silva. SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Transaction on Software Engineering, 38(4):957--974, 2012.

Digital Library

[12]

P. Diniz, S. Netto, and E. D. Silva. Digital Signal Processing: System Analysis and Design. Cambridge University Press, New York, NY, USA, 2002.

Digital Library

[13]

S. Fadali and A. Visioli. Digital Control Engineering:Analysis and Design, volume 303 of Electronics & Electrical. Elsevier/Academic Press, 2009.

[14]

M. Heizmann, J. Christ, D. Dietsch, E. Ermis, J. Hoenicke, M. Lindenmann, A. Nutz, C. Schilling, and A. Podelski. Ultimate Automizer with SMTInterpol - (competition contribution). In TACAS, volume 7795 of LNCS, pages 641--643, 2013.

Digital Library

[15]

H. Ismail, I. Bessa, L. C. Cordeiro, E. B. de Lima Filho, and J. E. C. Filho. DSVerifier: A bounded model checking tool for digital systems. In SPIN, volume 9232 of LNCS, pages 126--131, 2015.

Digital Library

[16]

R. Istepanian and J. Whidborne. Digital Controller Implementation and Fragility: A Modern Perspective. Advances in Industrial Control. Springer, 2001.

Digital Library

[17]

MathWorks. Matlab toolbox, 2017.

[18]

F. R. Monteiro. Bounded model checking of state-space digital systems: The impact of finite word-length effects on the implementation of fixed-point digital controllers based on state-space modeling. In FSE, pages 1151--1153, 2016.

Digital Library

[19]

K. Premaratne, E. Kulasekere, P. Bauer, and L.-J. Leclerc. An exhaustive search algorithm for checking limit cycle behavior of digital filters. IEEE Trans. Signal Processing, 44(10):2405--2412, Oct 1996.

Digital Library

[20]

H. Rocha, R. S. Barreto, L. C. Cordeiro, and A. D. Neto. Understanding programming bugs in ANSI-C software using bounded model checking counter-examples. In IFM, volume 7321 of LNCS, pages 128--142, 2012.

Digital Library

Cited By

Chaves LIsmail HBessa ICordeiro Lde Lima Filho E(2019)Verifying fragility in digital systems with uncertainties using DSVerifier v2.0Journal of Systems and Software10.1016/j.jss.2019.03.015153:C(22-43)Online publication date: 1-Jul-2019
https://dl.acm.org/doi/10.1016/j.jss.2019.03.015
Chaves LBessa IIsmail Hdos Santos Frutuoso ACordeiro Lde Lima Filho E(2018)DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial VehiclesIEEE Transactions on Reliability10.1109/TR.2018.287326067:4(1420-1441)Online publication date: Dec-2018
https://doi.org/10.1109/TR.2018.2873260

Recommendations

Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...
Modeling and Verification of Reactive Systems using Rebeca

Actor-based modeling has been successfully applied to the representation of concurrent and distributed systems. Besides having an appropriate and efficient way for modeling these systems, one needs a formal verification approach for ensuring their ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Copyright © 2018 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
255
Total Downloads

Downloads (Last 12 months)52
Downloads (Last 6 weeks)7

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Chaves LIsmail HBessa ICordeiro Lde Lima Filho E(2019)Verifying fragility in digital systems with uncertainties using DSVerifier v2.0Journal of Systems and Software10.1016/j.jss.2019.03.015153:C(22-43)Online publication date: 1-Jul-2019
https://dl.acm.org/doi/10.1016/j.jss.2019.03.015
Chaves LBessa IIsmail Hdos Santos Frutuoso ACordeiro Lde Lima Filho E(2018)DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial VehiclesIEEE Transactions on Reliability10.1109/TR.2018.287326067:4(1420-1441)Online publication date: Dec-2018
https://doi.org/10.1109/TR.2018.2873260

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Figures

Tables

Media

View Table of Conten