From Model Checking to Runtime Verification and Back

Investor logo

Warning

This publication doesn't include Faculty of Education. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

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

Year of publication 2017
Type Article in Proceedings
Conference Runtime Verification - 17th International Conference, RV 2017
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-67531-2_14
Field Informatics
Keywords model checking; runtime verification
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.