Technické zprávy
| Fiedor, J., Hrubá, V., Křena, B., Vojnar, T.: DA-BMC: A Tool Chain Combining Dynamic Analysis and Bounded Model Checking, FIT-TR-2011-06, Brno, CZ, FIT VUT, 2011, s. 9 | | 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?id=9780}
} |
|
Fakulta informačních technologií
![[dnssec]](/common/img/dnssec.png)