From Model Checking to Runtime Verification and Back

D 2017

From Model Checking to Runtime Verification and Back

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

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Confidentiality degree

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

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

DOI

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

UT WoS

000463267200014

Keywords in English

model checking; runtime verification

Abstract

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.

Links

GA15-08772S, research and development project

Name: Analýza korektnosti vícevláknových programů v C a C++

Investor: Czech Science Foundation

MUNI/A/0897/2016, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masaryk University, Category A

Citovat

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.

@inproceedings{1394289,
   author = {Kejstová, Katarína and Ročkai, Petr and Barnat, Jiří},
   address = {neuvedeno},
   booktitle = {Runtime Verification - 17th International Conference, RV 2017},
   doi = {http://dx.doi.org/10.1007/978-3-319-67531-2_14},
   editor = {Shuvendu Lahiri, Giles Reger},
   keywords = {model checking; runtime verification},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {neuvedeno},
   isbn = {978-3-319-67530-5},
   pages = {225-240},
   publisher = {Springer},
   title = {From Model Checking to Runtime Verification and Back},
   year = {2017}
}

TY  - JOUR
ID  - 1394289
AU  - Kejstová, Katarína - Ročkai, Petr - Barnat, Jiří
PY  - 2017
TI  - From Model Checking to Runtime Verification and Back
PB  - Springer
CY  - neuvedeno
SN  - 9783319675305
KW  - model checking
KW  - runtime verification
N2  - 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.
ER  -

KEJSTOVÁ, Katarína, Petr ROČKAI and Jiří BARNAT. From Model Checking to Runtime Verification and Back. In Shuvendu Lahiri, Giles Reger. \textit{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.

Detailed Information on Publication Record