Detail výsledku

Verifying Parametrised Hardware Designs Via Counter Automata

SMRČKA, A.; VOJNAR, T. Verifying Parametrised Hardware Designs Via Counter Automata. Hardware and Software, Verification and Testing. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2008. p. 51-68. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Smrčka Aleš, Ing., Ph.D., FIT (FIT), UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Abstrakt

The paper presents a new approach to formal verification of generic(i.e. parametrised) hardware designs specified in VHDL. The proposedapproach is based on a translation of such designs to counter automataand on exploiting the recent advances achieved in the area of theirautomated formal verification. We have implemented the proposedtranslation. Using one of the state-of-the-art tools for verificationof counter automata, we were then able to verify several non-trivialproperties of parametrised VHDL components, including a real-life one.

Klíčová slova

formal verification, hardware design, counter automaton, VHDL

URL
Rok
2008
Strany
51–68
Časopis
Lecture Notes in Computer Science, roč. 4899, ISSN 0302-9743
Sborník
Hardware and Software, Verification and Testing
Řada
Lecture Notes in Computer Science
Konference
Haifa Verification Conference 2007
Vydavatel
Springer Verlag
Místo
Heidelberg
BibTeX 
@inproceedings{BUT30897,
  author="Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Verifying Parametrised Hardware Designs Via Counter Automata",
  booktitle="Hardware and Software, Verification and Testing",
  year="2008",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="4899",
  pages="51--68",
  publisher="Springer Verlag",
  address="Heidelberg",
  issn="0302-9743",
  url="http://www.fit.vutbr.cz/~smrcka/pub/hvc07.pdf"
}
Projekty
Optická síť národního výzkumu a její nové aplikace, MŠMT, Výzkumná centra (2000-2004), MSM6383917201, zahájení: 2004-01-01, ukončení: 2010-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru