Skip to main content
SpringerLink
Log in
Book cover

International SPIN Workshop on Model Checking of Software

SPIN 2015: Model Checking Software pp 126–131Cite as

DSVerifier: A Bounded Model Checking Tool for Digital Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9232))

Abstract

This work presents the Digital-Systems Verifier (DSVerifier), which is a verification tool developed for digital systems. In particular, DSVerifier employs the bounded model checking technique based on satisfiability modulo theories (SMT) solvers, which allows engineers to verify the occurrence of design errors, due to the finite word-length approach employed in fixed-point digital filters and controllers. This tool consists in an additional module for the efficient SMT-based context-bounded model checker and presents command-line and graphical user interface (GUI) versions. Indeed, the GUI version is essential for reporting property violations, together with associated counterexamples. DSVerifier is implemented in C/C\(++\) and uses JavaFX for providing GUI support.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Available at http://www.dsverifier.org.

  2. 2.

    http://www.dsverifier.org/benchmarks.

  3. 3.

    http://www.oracle.com/technetwork/java/javase/8u40-relnotes-2389089.html.

References

  1. Jackson, M.: The world and the machine. In: ICSE, pp. 283–292 (1995)

    Google Scholar 

  2. Alur, R., et al.: Model-checking for real-time systems. In: LICS, pp. 414–425 (1990)

    Google Scholar 

  3. Alur, R., et al.: Model-checking in dense real-time. IC 104(1), 2–34 (1993)

    MATH  MathSciNet  Google Scholar 

  4. Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Tripakis, S., et al.: Checking timed Buechi automata emptiness efficiently. FMSD 26, 267–292 (2005)

    MATH  Google Scholar 

  6. Magellan, Hybrid RTL formal verification. http://www.synopsys.com/tools/verification/functionalverification/pages/magellan.aspx. Accessed 12 September 2014

  7. Davis, T.A., Sigmon, K.: MATLAB Primer, 7th edn. CRC Press, Boca Raton (2005)

    Google Scholar 

  8. Abreu, F.N., et al.: Verifying fixed-point digital filters using SMT-based bounded model checking. SBrT (2013). doi:10.14209/sbrt.2013.57

  9. Bessa, I., et al.: SMT-based bounded model checking of fixed-point digital controllers. In: IECON, pp. 295–301 (2014)

    Google Scholar 

  10. Bessa, I., et al.: Verification of delta form realization in fixed-point digital controllers using bounded model checking. In: SBESC, pp. 49–54 (2014)

    Google Scholar 

  11. Cordeiro, L., et al.: SMT-based bounded model checking for embedded ANSI-C software. TSE 38(4), 957–974 (2012)

    Google Scholar 

  12. Beyer, D.: Software verification and verifiable witnesses. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 401–416. Springer, Heidelberg (2015)

    Google Scholar 

  13. Ogata, K.: Discrete-Time Control Systems. Prentice Hall International editions, Prentice-Hall International, Upper Saddle River (1995)

    Google Scholar 

  14. Platzer, A.: Logic and compositional verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 28–43. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Electronic and Information Research Center, Federal University of Amazonas, Manaus, Brazil

    Hussama I. Ismail, Iury V. Bessa, Lucas C. Cordeiro, Eddie B. de Lima Filho & João E. Chaves Filho

Authors
  1. Hussama I. Ismail
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Iury V. Bessa
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Lucas C. Cordeiro
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Eddie B. de Lima Filho
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. João E. Chaves Filho
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Iury V. Bessa .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Matieland, South Africa

    Bernd Fischer

  2. Stellenbosch University, Matieland, South Africa

    Jaco Geldenhuys

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Ismail, H.I., Bessa, I.V., Cordeiro, L.C., de Lima Filho, E.B., Chaves Filho, J.E. (2015). DSVerifier: A Bounded Model Checking Tool for Digital Systems. In: Fischer, B., Geldenhuys, J. (eds) Model Checking Software. SPIN 2015. Lecture Notes in Computer Science(), vol 9232. Springer, Cham. https://doi.org/10.1007/978-3-319-23404-5_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23404-5_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23403-8

  • Online ISBN: 978-3-319-23404-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation