From Model Checking to Runtime Verification and Back

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F17%3A00095134" target="_blank" >RIV/00216224:14330/17:00095134 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-319-67531-2_14" target="_blank" >http://dx.doi.org/10.1007/978-3-319-67531-2_14</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-319-67531-2_14" target="_blank" >10.1007/978-3-319-67531-2_14</a>

Jazyk výsledku

angličtina

Název v původním jazyce

From Model Checking to Runtime Verification and Back

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

From Model Checking to Runtime Verification and Back

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA15-08772S" target="_blank" >GA15-08772S: Analýza korektnosti vícevláknových programů v C a C++</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2017

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Runtime Verification - 17th International Conference, RV 2017

ISBN

9783319675305

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

16

Strana od-do

225-240

Název nakladatele

Springer

Místo vydání

neuvedeno

Místo konání akce

Seattle

Datum konání akce

13. 9. 2017

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—