Technická zpráva

FIEDOR, J., HRUBÁ, V., KŘENA, B. a VOJNAR, T.. 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.
Jazyk publikace:angličtina
Název publikace:DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking
Název (cs):DA-BMC: Nástroj propojující dynamickou analýzu a bounded model checking
Strany:9
Místo vydání:FIT-TR-2011-06, Brno, CZ
Rok:2011
Vydavatel:Fakulta informačních technologií VUT v Brně
URL:http://www.fit.vutbr.cz/~ihruba/pub/FIT-TR-2011-06.pdf [HTML]
Klíčová slova
dynamic analysis, bounded model checking, verification, record and replay
Anotace
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.
BibTeX:
@TECHREPORT{
   author = {Jan Fiedor and Vendula Hrubá and Bohuslav Křena and Tomáš
	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 = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=9780}
}

Vaše IPv4 adresa: 54.80.120.136
Přepnout na IPv6 spojení

DNSSEC [dnssec]