Detail publikace

DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking

DUDKA, V.; FIEDOR, J.; KŘENA, B.; VOJNAR, T. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. FIT-TR-2011-06, Brno: Faculty of Information Technology BUT, 2011.
Název česky
DA-BMC: Nástroj propojující dynamickou analýzu a bounded model checking
Typ
zpráva odborná
Jazyk
anglicky
Autoři
Dudka Vendula, Ing.
Fiedor Jan, Ing., Ph.D. (UITS)
Křena Bohuslav, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

dynamic analysis, bounded model checking, verification, record and replay

Abstrakt

Tento článek prezentuje nástroj DA-BMC, který propojuje dynamickou analýzu s omezeným model checkingem (bounded model checking). Nástroj slouží k vyhledávání chyb v Java programech s paralelismem. Hlavní myšlenkou je použití dynamické analýzy na detekci podezřelého chování ověřovaných programů. Vybrané události v rámci takových chování jsou přitom zaznamenávány. Posloupnost zaznamenaných událostí posléze slouží k navigaci stavovým prostorem při rekonstrukci podezřelého chování v model checkeru, resp. při nalézání chování, které obsahuje stejnou posloupnost monitorovaných událostí jako podezřelé chování detekované dynamickou analýzou. Pro navigování mezi jednotlivými zaznamenanými událostmi je využito možností model checkingu procházet stavovými prostory. Omezedný model checking je pak následně také proveden v okolí konce vygenerovaného chování s cílem potvrdit výskyt reálné chyby.

Rok
2011
Strany
9
Vydavatel
Faculty of Information Technology BUT
Místo
FIT-TR-2011-06, Brno
BibTeX 
@techreport{BUT192772,
  author="Vendula {Dudka} and Jan {Fiedor} and Bohuslav {Křena} and Tomáš {Vojnar}",
  title="DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking",
  year="2011",
  publisher="Faculty of Information Technology BUT",
  address="FIT-TR-2011-06, Brno",
  pages="9",
  url="http://www.fit.vutbr.cz/~ihruba/pub/FIT-TR-2011-06.pdf"
}
Nahoru