D 2017

From Model Checking to Runtime Verification and Back

KEJSTOVÁ, Katarína, Petr ROČKAI a Jiří BARNAT

Základní údaje

Originální název

From Model Checking to Runtime Verification and Back

Autoři

KEJSTOVÁ, Katarína (703 Slovensko, domácí), Petr ROČKAI (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, garant, domácí)

Vydání

neuvedeno, Runtime Verification - 17th International Conference, RV 2017, od s. 225-240, 16 s. 2017

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/17:00095134

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-67530-5

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-67531-2_14

UT WoS

000463267200014

Klíčová slova anglicky

model checking; runtime verification

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 13. 5. 2020 19:25, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We describe a novel approach for adapting an existing software model checker to perform precise runtime verification. The software under test is allowed to communicate with the wider environment (including the file system and network). The modifications to the model checker are small and self-contained, making this a viable strategy for re-using existing model checking tools in a new context. Additionally, from the data that is gathered during a single execution in the runtime verification mode, we automatically re-construct a description of the execution environment which can then be used in the standard, full-blown model checker. This additional verification step can further improve coverage, especially in the case of parallel programs, without introducing substantial overhead into the process of runtime verification.

Návaznosti

GA15-08772S, projekt VaV
Název: Analýza korektnosti vícevláknových programů v C a C++
Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads
MUNI/A/0897/2016, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty
Zobrazeno: 5. 11. 2024 09:07