Informační systém MU
KEJSTOVÁ, Katarína, Petr ROČKAI a Jiří BARNAT. From Model Checking to Runtime Verification and Back. In Shuvendu Lahiri, Giles Reger. Runtime Verification - 17th International Conference, RV 2017. neuvedeno: Springer, 2017, s. 225-240. ISBN 978-3-319-67530-5. Dostupné z: https://dx.doi.org/10.1007/978-3-319-67531-2_14.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 0302-9743
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ěnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 13. 5. 2020 19:25.
Anotace
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 VaVNá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 MUNá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: 30. 4. 2024 21:25