Detail publikace

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

DUDKA Vendula, FIEDOR Jan, KŘENA Bohuslav a VOJNAR Tomáš. DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking. FIT-TR-2011-06, Brno: Fakulta informačních technologií VUT v Brně, 2011.
Název česky
DA-BMC: Nástroj propojující dynamickou analýzu a bounded model checking
Typ
technická zpráva
Jazyk
angličtina
Autoři
Dudka Vendula, Ing. (UITS FIT VUT)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
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
Fakulta informačních technologií VUT v Brně
Místo
FIT-TR-2011-06, Brno, CZ
BibTeX 
@TECHREPORT{FITPUB9780,
   author = "Vendula Dudka and Jan Fiedor and Bohuslav K\v{r}ena and Tom\'{a}\v{s} Vojnar",
   title = "DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking",
   pages = 9,
   year = 2011,
   location = "FIT-TR-2011-06, Brno, CZ",
   publisher = "Faculty of Information Technology BUT",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9780"
}
Nahoru