KEJSTOVÁ, Katarína, Petr ROČKAI and 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, p. 225-240. ISBN 978-3-319-67530-5. Available from: https://dx.doi.org/10.1007/978-3-319-67531-2_14.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name From Model Checking to Runtime Verification and Back
Authors KEJSTOVÁ, Katarína (703 Slovakia, belonging to the institution), Petr ROČKAI (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution).
Edition neuvedeno, Runtime Verification - 17th International Conference, RV 2017, p. 225-240, 16 pp. 2017.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/17:00095134
Organization unit Faculty of Informatics
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
Keywords in English model checking; runtime verification
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 13/5/2020 19:25.
Abstract
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.
Links
GA15-08772S, research and development projectName: Analýza korektnosti vícevláknových programů v C a C++
Investor: Czech Science Foundation
MUNI/A/0897/2016, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masaryk University, Category A
PrintDisplayed: 30/4/2024 22:25