Portal de Periódicos da CAPES

Capítulo de livro Produção Nacional Revisado por pares

BIBTEX RIS

DSVerifier: A Bounded Model Checking Tool for Digital Systems

2015; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-23404-5_9

1611-3349

Hussama Ismail, Iury Bessa, Lucas C. Cordeiro, Eddie B. de Lima Filho, João Edgar Chaves Filho,

Real-time simulation and control systems

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.