Replay Tracer & BMC
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F10%3APR25240" target="_blank" >RIV/00216305:26230/10:PR25240 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Replay Tracer & BMC
Popis výsledku v původním jazyce
This tool is about the using of bounded model checking for verification of the bugs in concurrent programs. There is the search strategy for navigation through a state space to a suspicious state (or to its surroundings) and a subsequent bounded model checking initialled from this state. In the first step is record the trace of running program. The second step is replay this trace in some model checker and verify a chosen place in state space only. One of the advantage of these strategy is that the model checking can be started from any of recorded states which precede the suspicious state. We are concentrate to program written in Java. The model checker for Java program has been chosen Java PathFinder JPF. There is record trace of the running of the program by the IBM ConTest
Název v anglickém jazyce
Replay Tracer & BMC
Popis výsledku anglicky
This tool is about the using of bounded model checking for verification of the bugs in concurrent programs. There is the search strategy for navigation through a state space to a suspicious state (or to its surroundings) and a subsequent bounded model checking initialled from this state. In the first step is record the trace of running program. The second step is replay this trace in some model checker and verify a chosen place in state space only. One of the advantage of these strategy is that the model checking can be started from any of recorded states which precede the suspicious state. We are concentrate to program written in Java. The model checker for Java program has been chosen Java PathFinder JPF. There is record trace of the running of the program by the IBM ConTest
Klasifikace
Druh
R - Software
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2010
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Interní identifikační kód produktu
RecRev
Technické parametry
Poskytováno pod Freeware licencí VUT v Brně (https://wis.fit.vutbr.cz/FIT/db/dir.php/dr/VZ2007/externiInformace/softwareNaWebu/Priloha2_rozh23.pdf). - Implementovaný v programovacím jazyce Java. - Modul model checkeru JPF, kte
Ekonomické parametry
—
IČO vlastníka výsledku
00216305
Název vlastníka
Vysoké učení technické v Brně